Definition is_univalent_right_total_of_twosided_disp_cat (HC₂ : is_univalent C₂) (HD : is_univalent_twosided_disp_cat D) : is_univalent_disp right_total_of_twosided_disp_cat. Proof. intros y₁ y₂ p xy₁ xy₂. induction p. use weqhomot. - exact (weq_iso_right_total_of_twosided_disp_cat xy₁ xy₂ ∘ weqtotal2 (_ ,, HC₂ _ _) (λ q, (_ ,, HD _ _ _ _ (idpath _) q (pr2 xy₁) (pr2 xy₂))) ∘ total2_paths_equiv _ _ _)%weq. - abstract (intro p ; induction p ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; cbn ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromIsoTotal. End FromIsoTotal.