Left Fibration

A Cocartesian Fibration $\mathcal{E}\rightarrowtriangle\mathcal{B}$ is a left fibration if every morphism is Cocartesian.

Note that every morphism being Cocartesian does not suffice, we need the existence of cocartesian lifts!

Properties

• A cocartesian fibration is a left fibration if and only if the projection from the Total Category is Conservative.
• A cocartesian fibration is a left fibration if and only if every vertical map is invertible. This means that every Fibre Category of a left fibration is a Groupoid.