Univalent categories and Rezk completion

Krzysztof Kapulkin
Thursday, July 25, 2013 - from 14:00 to 14:40
The Univalent Foundations Program is a new approach to the foundations of mathematics, proposed by Vladimir Voevodsky (IAS, Princeton), inspired by the homotopy-theoretic models of constructive type theory. It builds on the existing language of Martin-Lof Type Theory (which is the underlying language of many interactive proof assistants, such as Coq and AGDA), to which it adds a new axiom, called the Univalence Axiom. This axiom is not valid in the types-as-sets interpretation of type theory, but it holds in (and was, in fact, inspired by) the model of type theory in Kan complexes. The language of the Univalent Foundations is particularly suitable for developing homotopy theory synthetically, allowing only constructions and proofs that are homotopy-invariant. Recent advances in this approach include calculations of some homotopy groups of spheres and a synthetic proof of Blakers{Massey Theorem. Working in Voevodskys program we begin to systematically develop category theory. We rst de ne precategories which have an arbitrary type as its type of objects, but the type of morphism is required to satisfy the principle of Uniqueness of Identity Proofs, allowing one to talk about equality of morphisms. Categories (or univalent categories) are required to satisfy an additional condition, which is a version of the Univalence Axiom. For such (univalent) categories we start developing the theory: we de ne adjunctions, equivalences, the Yoneda embedding (showing that it is full and faithful). We moreover prove that for categories, the notion of equality is the same as the notion of categorical equivalence and thus, in our system, every property of categories is automatically invariant under equivalence. Finally, we show that the inclusion of categories into precategories admits a left adjoint (in the bicategorical sense) and the components of the unit of this adjunction are categorical equivalences. In the homotopytheoretic models of type theory, this can be seen as a truncated version of the Rezk completion of a Segal space or the stack completion of a prestack. (Joint work with Benedikt Ahrens and Michael Shulman.)