proposition: Lemma issig_morphism abf a'b'f' : (morphism_sig_T abf a'b'f') <~> morphism abf a'b'f'.
proof: Proof. etransitivity; [ | exact (issig_morphism' abf a'b'f') ]. repeat (apply equiv_functor_sigma_id; intro). symmetry; apply equiv_sigma_contr; intro. apply issig_morphism_helper; assumption. Defined.
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types