Univalent Double Categories
summary
Formalization builds two equivalent definitions of double categories: an unfolded explicit version and a structured version using two-sided displayed categories, implemented in Coq UniMath. The work defines a notion of univalent double category and proves a univalence principle so that equivalences = identities for those double categories. Most of the library is complete and reuses existing category-theory code; current encodings force strictness in one direction and fully weak double categories remain future work.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:11Univalent foundations
- 3:20Categories as math
- 6:32From categories to double
- 9:03Formalization in univalent type theory
- 13:15Challenges in formalizing
- 16:01Two-sided display categories
- 18:54Translating invariances
- 20:39Summary
- 21:42Q&A
related talks
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
26m2-Functoriality of Initial Semantics, and Applications
23mImplementing a category-theoretic framework for typed abstract syntax
02h 24mCategory Theory Track
24mA Computational Interpretation of Compact Closed Categories
25mCubical Synthetic Homotopy Theory
37mEquivalence Hypergraphs: E-Graphs for Monoidal Theories
21mUndecidability of Higher-Order Unification Formalised in Coq