Category theory in the Univalent Foundations
Benedikt Ahrens
CIMI, University Paul Sabatier, Toulouse
https://benediktahrens.net/
Date(s) : 18/03/2014 iCal
11h00 - 12h00
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:
-# Two univalent categories are equivalent (in the category-theoretic sense) if and only if they are equal (in the type-theoretic sense).
-# Any category can be turned into a univalent category via a universal construction, which we call the Rezk completion.
Catégories
