Action Groupoid
Let be a Group Action. The action groupoid is the following Groupoid:
- Objects are elements of
- A morphism is a pair of a group element and a proof that .
In other words, is the Category of Elements of when viewed as a Presheaf.
Note that there is a canonical functor to the Delooping of ; this endows with the structure of a Discrete Cocartesian Fibration.