Total space is action groupoid [00DJ]

Given for a fix , the total space is by definition what we call the action type . Its objects are pairs of the form , with

See also definition 5.4.1 in the symmetry book. The action type corresponds to what we call the action groupoid or weak quotient in category theory. We will see in a second that paths in the identity type of the action type correspond precisely to the morphisms in the the action groupoid