proposition: Lemma precomp_disp_id_left_inj {C : category} {D : disp_cat C} {y z : C} {f : C⟦y,z⟧} {yy : D y} {zz : D z} (ff1 ff2 : yy -->[f] zz) : id_disp yy ;; ff1 = id_disp yy ;; ff2 → ff1 = ff2.
proof: Proof. intro p. rewrite ! id_left_disp in p. refine (transportb_transpose_right p @ _). rewrite transport_b_b. use transportf_set. apply homset_property. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core