  In Martin-L\"of's Intensional Type Theory, identity type is a heavily used
and studied concept. The reason for that is the fact that it's responsible for
the recently discovered connection between Type Theory and Homotopy Theory. The
main problem with identity types, as originally formulated, is that they are
complex to understand and use. Using that fact as motivation, a much simpler
formulation for the identity type was proposed by Queiroz & Gabbay (1994) and
further developed by de Queiroz & de Oliveira (2013). In this formulation, an
element of an identity type is seen as a sequence of rewrites (or computational
paths). Together with the logical rules of this new entity, there exists a
system of reduction rules between sequence of rewrites called LND_{EQS}-RWS.
This system is constructed using the labelled natural deduction (i.e. Prawitz'
Natural Deduction plus derivations-as-terms) and is responsible for
establishing how a sequence of rewrites can be rewritten, resulting in a new
sequence of rewrites. In this context, we propose a categorical interpretation
for this new entity, using the types as objects and the rules of rewrites as
morphisms. Moreover, we show that our interpretation is in accordance with some
known results, like that types have a groupoidal structure. We also interpret
more complicated structures, like the one formed by a rewrite of a sequence of
rewrites.
