Lemma cod_disp_axioms : disp_cat_axioms C cod_disp_data. 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.
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.