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