The Internal Language of Univalent Categories

Niels van der Weide

In this talk, we study the theorem by Clairambault and Dybjer saying that there is a biequivalence between locally Cartesian closed categories and Martin-Löf type theories in univalent foundations. More specifically, we give an analogue of this theorem using univalent categories, and we extend it to several classes of toposes.I start with an introduction to univalent categories, and I shall discuss some of the challenges when interpreting Martin-Löf type theory in univalent categories. After that, I will give a short introduction to comprehension categories, and explain why they are a suitable structure for the semantics of type theory in univalent foundations. Finally, I shall explain how univalent categories are used in this proof, and how they simplify the technical details.

---

Previous: | Incremental and parallel checking of dependently typed programs
Next: | Verifying weak memory concurrent data structure implementations