On univalent categories in homotopy type theory:
Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Univalent categories and the Rezk completion, Mathematical Structures in Computer Science 25 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics), (2015) 1010-1039 [arXiv:1303.0584, doi:10.1007/978-3-319-21284-5_14]
Benedikt Ahrens, Univalent categories and Rezk completion, talk at IRIT (2013) [pdf]
On the UniMath project:
Benedikt Ahrens, Paige Randall North, Niels van der Weide, Semantics for two-dimensional type theory, LICS ‘22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, August 2022, No. 12, Pages 1–14, (doi:10.1145/3531130.3533334)
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle (arXiv:2102.06275)
On univalence and the structure identity principle:
Benedikt Ahrens, Paige Randall North, Univalent foundations and the equivalence principle, in: Reflections on the Foundations of Mathematics, Synthese Library 407 Springer (2019) [arXiv:2202.01892, doi:10.1007/978-3-030-15655-8]
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle [abs:2102.06275]
On univalent bicategories in homotopy type theory:
On monoidal univalent categories:
An internal language for comprehension categories is developed in:
Last revised on June 14, 2025 at 18:29:21. See the history of this page for a list of all contributions to it.