nLab Benedikt Ahrens (changes)

Showing changes from revision #13 to #14: Added | Removed | Changed

• webpage

Selected writings

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](https://arxiv.org/abs/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, UniMath: its origins, present, and future (2017) [[pdf](https://unimath.github.io/bham2017/UniMath_origins-present-future.pdf), pdf]

On 2-dimensional type theory:

• 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](https://arxiv.org/abs/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](https://arxiv.org/abs/2102.06275)]

On 2-dimensional type theory:

• 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, 12 (2022) 1–14, [[doi:10.1145/3531130.3533334](https://doi.org/10.1145/3531130.3533334)]

On univalent bicategories in homotopy type theory:

• Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide, Bicategories in Univalent Foundations, Mathematical Structures in Computer Science 31 10 (2022) 1232-1269 [[arXiv:1903.01152](https://arxiv.org/abs/1903.01152), doi:10.1017/S0960129522000032&rbrack

On monoidal univalent categories:

• Kobe Wullaert, Ralph Matthes, Benedikt Ahrens, Univalent Monoidal Categories [[arXiv:2212.03146](https://arxiv.org/abs/2212.03146)]

An internal language for comprehension categories is developed in:

• Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North, A Type Theory for Comprehension Categories with Applications to Subtyping (arXiv:2503.10868)

On the Rzk proof assistant:

• Nikolai Kudasov, Violetta Sim, Benedikt Ahrens: Rzk: a Proof Assistant for Synthetic $\infty$-Categories [[arXiv:2607.12207](https://arxiv.org/abs/2607.12207)]

Related entries

• internal category in homotopy type theory

• UniMath project