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, UP7 - Université Paris Diderot - Paris 7, CNRS : UMR7126
3 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN
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.
Document type :
Preprints, Working Papers, ...
2013


https://hal.archives-ouvertes.fr/hal-00786589
Contributor : Nicolas Tabareau <>
Submitted on : Thursday, March 21, 2013 - 10:10:24 AM
Last modification on : Thursday, March 21, 2013 - 10:32:01 AM

File

main.pdf
fileSource_public_author

Identifiers

  • HAL Id : hal-00786589, version 3

Collections

Citation

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

Export

Share

Metrics

Consultation de
la notice

391

Téléchargement du document

128