Category theory in the Univalent Foundations

Carte non disponible

Date/heure
Date(s) - 18/03/2014
11 h 00 min - 12 h 00 min

Catégories


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.

http://benedikt-ahrens.de“>http://benedikt-ahrens.deBenedikt Ahrens

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange