  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).
