Univalence for free

Matthieu Sozeau 1, 2 Nicolas Tabareau 3, 4
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
3 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : We present an internalization of the 2-groupoid interpretation of the calculus of construction that allows to realize the univalence axiom, proof irrelevance and reasoning modulo. As an example, we show that in our setting, the type of Church integers is equal to the inductive type of natural numbers.
Type de document :
Pré-publication, Document de travail
2013
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-00786589
Contributeur : Nicolas Tabareau <>
Soumis le : jeudi 21 mars 2013 - 10:10:24
Dernière modification le : mercredi 12 octobre 2016 - 01:24:49
Document(s) archivé(s) le : dimanche 2 avril 2017 - 16:22:01

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00786589, version 3

Collections

Citation

Matthieu Sozeau, Nicolas Tabareau. Univalence for free. 2013. <hal-00786589v3>

Partager

Métriques

Consultations de
la notice

640

Téléchargements du document

258