Explicit Computational Paths

Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira

The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms $a,b$ of a type $A$…