{fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
{ fmor := fun a b f => fmor F f }.
intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
{fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
{ fmor := fun a b f => fmor F f }.
intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).