proposition: Proposition disp_univalent_disp_codomain : is_univalent_disp (disp_codomain C).
proof: 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.
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