On the Identity Type as the Type of Computational Paths

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

We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. O…