proposition: Lemma issig_morphism' abf a'b'f' : (morphism_sig_T' abf a'b'f') <~> morphism abf a'b'f'.
proof: Proof. issig. Defined.
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types