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. refine (pr1_transportf (A := C⟦_,_⟧) _ _ @ _). rewrite transportf_const ; cbn. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.