let us describe the salient features of the resulting cocartesian fibration
which it classifies.
(1)
Over an object , the fiber is canonically equivalent to .
(2)
Given a morphism in and an object of the fiber over its source, there is a canonical morphism
in which projects to , called an -cocartesian lift (or simply a cocartesian lift) of relative to , such that the canonical equivalence identifies the object with the object . This is illustrated in FigureΒ 1.
Figure 1. An illustration of a cocartesian morphism.
(3)
An arbitrary morphism in admits a unique factorization as a cocartesian morphism followed by a morphism lying in the fiber β which we will therefore refer to as a fiber morphism β, as illustrated in FigureΒ 2.
Figure 2. An illustration of the factorization system in a cocartesian fibration.
Under the equivalence , the morphism in corresponds to a morphism in . Thus, we have canonical equivalences