On the identity type as the type of computational paths
Arthur Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira · Logic Journal of IGPL · 2017
We present a way of formalizing the intensional identity type based on the notion of computational paths which will be taken to be proofs of propositional equality, and thus terms of the identity type. This approach results in an elimination rule which constructs some relevant basic types of Martin-Löf’s Intensional Type Theory in a simpler way. To make this point clear we construct terms of these types using our proposed elimination rule. We also show that one of the properties of Martin-Löf’s original identity type is present on our formulation of the identity type of computational paths. We are referring to the fact that the identity type induces a groupoid structure, as proposed by Hofmann and Streicher in 1994. Using categorical semantics, we show that computational paths induce a groupoid structure too. It is further shown that computational paths induce higher categorical structures. Using our groupoid structure, we also show that our approach refutes the uniqueness of identity proofs. This is on par with the same result obtained by Hofmann and Streicher in 1995 for the original identity type.