This file defines the category of elements, also known as (a special case of) the Grothendieck construction.
Given a functor F : C ⥤ Type, an object of F.elements is a pair (X : C, x : F.obj X). A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
This construction is equivalent to a special case of a comma construction, so this is mostly just a more convenient API. We prove the equivalence in category_theory.category_of_elements.comma_equivalence.
category of elements, Grothendieck construction, comma category
The type of objects for the category of elements of a functor F : C ⥤ Type is a pair (X : C, x : F.obj X).
The category structure on F.elements, for F : C ⥤ Type. A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
The functor out of the category of elements which forgets the element.
The forward direction of the equivalence F.elements ≅ (*, F).
The reverse direction of the equivalence F.elements ≅ (*, F).
The equivalence between the category of elements F.elements and the comma category (*, F).