On the Groupoid Model of Computational Paths

TL;DR

This paper explores the mathematical structure of computational paths within type theory, demonstrating that they form a groupoid and can induce higher categorical structures, thus enriching the understanding of identity types.

Contribution

It proves that computational paths induce a groupoid structure and can generate higher categorical structures using categorical semantics.

Findings

Computational paths form a groupoid structure.

Computational paths can induce higher categorical structures.

Categorical semantics supports these structural properties.

Abstract

The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computational paths are taken to be terms of the identity type of Martin L\"of's Intensional Type Theory, since these paths can be seen as the grounds on which the propositional equality between two computational objects stand. From this perspective, this work aims to show that one of the properties of the identity type is present on computational paths. We are referring to the fact that that the identity type induces a groupoid structure, as proposed by Hofmann \& Streicher (1994). Using categorical semantics, we show that computational paths induce a groupoid structure. We also show that computational paths are capable of inducing higher categorical structures.