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.
