On the Identity Type as the Type of Computational Paths

TL;DR

This paper proposes a new formalization of the intensional identity type using computational paths, resulting in a more understandable elimination rule and demonstrating that it induces a groupoid structure similar to traditional approaches.

Contribution

It introduces a novel approach to formalizing the identity type via computational paths, simplifying the elimination rule and establishing its groupoid structure.

Findings

The new formalization yields an easier-to-understand elimination rule.

The identity type induces a groupoid structure under this approach.

The approach aligns with traditional models like Hofmann & Streicher's.

Abstract

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. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity type, as defined by our approach, induces a groupoid structure. This result is on par with the fact that the traditional identity type induces a groupoid, as exposed by Hofmann \& Streicher (1994).