proposition: Lemma cod_disp_axioms : disp_cat_axioms C cod_disp_data.
proof: Proof. repeat apply tpair; intros; try apply homset_property. - use eq_cod_mor. rewrite transportb_cod_disp. cbn. apply id_left. - use eq_cod_mor. rewrite transportb_cod_disp. cbn. apply id_right. - use eq_cod_mor. rewrite transportb_cod_disp. cbn. apply assoc. - apply (isofhleveltotal2 2). + apply homset_property. + intro. apply isasetaprop. apply homset_property. 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