Proposition disp_univalent_disp_codomain : is_univalent_disp (disp_codomain C). Proof. use is_univalent_disp_from_fibers. intros x fy gz. use weqhomot. - refine (disp_iso_weq_iso _ _ ∘ weqtotal2 (make_weq _ (univalent_category_is_univalent C _ _)) _ ∘ total2_paths_equiv _ _ _)%weq. abstract (induction fy as [ y f ] ; induction gz as [ z g ] ; cbn ; intro p ; induction p ; cbn ; rewrite id_left ; exact (idweq _)). - intro p. induction p. use subtypePath. { intro. apply isaprop_is_z_iso_disp. } use eq_cod_mor. 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.