proposition: Lemma issig_morphism_helper {T0} `{IsHSet T0} (a b : T0) (pf : a = b) : Contr (b = a).
proof: Proof. destruct pf. apply contr_inhabited_hprop; try reflexivity. typeclasses eauto. Qed.
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types