Séminaire Logique et Interactions

The Univalent Foundations is an extension of Intensional Martin-Löf Type Theory (MLTT) recently proposed by V. Voevodsky. Its novelty is the Univalence Axiom which implements the idea that indistinguishable types should be equal by identifying equality of types with isomorphism of types. When formalizing category theory in traditional, set-theoretic foundations, a significant discrepancy between the foundational notion of "sameness" - equality - and its categorical notion arises: most category-theoretic concepts are invariant under weaker notions of sameness than equality, namely isomorphism in a category or equivalence of categories. We show that this discrepancy can be avoided when formalizing category theory in Univalent Foundations. In this talk I first give an introduction to Voevodsky's Univalent Foundations. Afterwards I define categories and univalent categories within Univalent Foundations, and develop basic category theory. The two main results of our work are the following:

1. Two univalent categories are equivalent (in the category-theoretic sense) if and only if they are equal (in the type-theoretic sense).

2. Any category can be turned into a univalent category via a universal construction, which we call the Rezk completion.

We defined a typed lambda-calculus where the isomorphisms between types are raised to the level of an equality relation. To this end, an equivalence relation is settled at the term level. We provide a proof of strong normalisation modulo such an equivalence, which is a non-trivial adaptation of the reducibility method. This work opens several paths for future work, which I will try to detail in this talk.