proposition: Proposition transportf_cod_disp {x y : C} {xx : cod_disp_data x} {yy : cod_disp_data y} {f g : x --> y} (p : f = g) (ff : xx -->[ f] yy) : pr1 (transportf (mor_disp xx yy) p ff) = pr1 ff.
proof: Proof. refine (pr1_transportf (A := C⟦_,_⟧) _ _ @ _). rewrite transportf_const ; cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations