proposition: Lemma path_morphism : forall xa yb (fh gi : morphism xa yb), f fh = f gi -> fh = gi.
proof: Proof. intros ? ? [? ?] [? ?] H; simpl in *; path_induction; apply ap. apply path_ishprop. Defined.
imports: Category.Core HoTT.Basics HoTT.Types HSet