Identity type of the total space [00DK]

As a Sigma-Type, the identity type of the total space is given by

, since (by definition), this is

So an element of the identity type is an element together with a proof that , which is exacly what we would expect from a morphism in the action groupoid.