Unique lifting property of a discrete fibration
= Unique lifting property of a discrete fibration
An incoming <morphism> into the image of a specified object has exactly one lift with that specified codomain. Both its source object and its lifted <morphism> are determined. Applying uniqueness to identity and composite <morphisms> gives the functoriality of lifting.