Right Fibration

A right fibration is a Cartesian Fibration where every morphism is Cartesian. Note that every morphism being cartesian does not suffice: we need the existence of lifts.

Properties

• A fibration is a right fibration if and only if the projection from the Total Category

is Conservative.

• A fibration is a right fibration if and only if every vertical map is invertible. This means that every Fibre Category of a right fibration is a Groupoid.