Proposition eq_cod_mor {x y : C} {xx : cod_disp_data x} {yy : cod_disp_data y} {f : x --> y} {ff gg : xx -->[ f ] yy} (p : pr1 ff = pr1 gg) : ff = gg. Proof. use subtypePath. { intro. apply homset_property. } exact p. 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.