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 - Centre National de la Recherche Scientifique : 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 : Monday, October 5, 2015 - 5:01:02 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00786589, version 3

Collections

Citation

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

Export

Share

Metrics

Record views

435

Document downloads

161