forall xa yb (H : x xa = x yb), transport P H (a xa) = a yb -> xa = yb. Proof. intros [? ?] [? ?] H H'; simpl in *; path_induction; reflexivity. Defined.
Require Import Category.Core. Require Import HoTT.Basics HoTT.Types HSet. Import PreCategoryOfStructures.