Univalence For Free
Matthieu Sozeau, Nicolas Tabareau, Ascola Teams · 2013
Abstract. We present an internalization of the 2-groupoid interpreta-tion 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. 1