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. intro p. rewrite ! id_left_disp in p. refine (transportb_transpose_right p @ _). rewrite transport_b_b. use transportf_set. apply homset_property. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core.