  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.

Logic in Computer Science