Categorical Structures for Type Theory in Univalent Foundations

Benedikt Ahrens 1 Peter Lefanu Lumsdaine 2 Vladimir Voevodsky 3
1 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions. We then analyze how these structures transfer along (weak and strong) equivalences of categories , and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
Type de document :
Communication dans un congrès
Valentin Goranko and Mads Dam. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. LIPIcs, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 82, pp.8:1 - 8:16, 2017, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). 〈10.4230/LIPIcs.CSL.2017.8〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01579271
Contributeur : Benedikt Ahrens <>
Soumis le : mercredi 30 août 2017 - 18:12:15
Dernière modification le : jeudi 19 avril 2018 - 11:46:06

Fichier

LIPIcs-CSL-2017-8.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Benedikt Ahrens, Peter Lefanu Lumsdaine, Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations . Valentin Goranko and Mads Dam. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. LIPIcs, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), 82, pp.8:1 - 8:16, 2017, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). 〈10.4230/LIPIcs.CSL.2017.8〉. 〈hal-01579271〉

Partager

Métriques

Consultations de la notice

173

Téléchargements de fichiers

59