Univalent Double Categories - Formalization and Applications in Category Theory

Explore a 27-minute conference talk from CPP 2024 that delves into the formalization of double categories using the Coq proof assistant. Learn how category theory provides a framework for understanding mathematical structures and how double categories extend this concept with two classes of morphisms. Discover the applications of double categories in mathematics and computer science, including their use in functional programming, lenses, petri nets, and spans. Examine two equivalent formalizations of double categories presented in the talk: an explicit definition and a definition using 2-sided displayed categories. Gain insights into the notion of univalent double categories and the established univalence principle. Understand how this work contributes to the field of formalized mathematics and extends the capabilities of the Coq UniMath library.

[CPP'24] Univalent Double Categories