Nicolas Tabareau (INRIA, Inventeurs du monde numérique), Univalence for free, not yet ...



We present an internalization of the 2-groupoid (or rather groupoidoid) interpretation of the calculus of construction that allows to realize proof irrelevance, reasoning modulo and a weak form of the univalence axiom. As an example, we show that in our setting, the type of Church integers is equal to the inductive type of natural numbers.

Pièces jointes