Univalence for free

Matthieu Sozeau 1, 2 Nicolas Tabareau 3, 4
1 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria Paris-Rocquencourt, PPS - Preuves, Programmes et Systèmes, CNRS - Centre National de la Recherche Scientifique : UMR7126, UP7 - Université Paris Diderot - Paris 7
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


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

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>

Exporter

Partager

Métriques

Consultations de
la notice

513

Téléchargements du document

215