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

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

https://hal.archives-ouvertes.fr/hal-00786589
Contributeur : Nicolas Tabareau <>
Soumis le : jeudi 21 mars 2013 - 10:10:24
Dernière modification le : jeudi 7 décembre 2017 - 01:22:15
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

692

Téléchargements de fichiers

268