Definition is_univalent_sigma_of_twosided_disp_cat (HD₁ : is_univalent_twosided_disp_cat D₁) (HD₂ : is_univalent_disp D₂) : is_univalent_twosided_disp_cat sigma_twosided_disp_cat. Proof. intros x₁ x₂ y₁ y₂ p₁ p₂ xy₁ xy₂. induction p₁, p₂. use weqhomot. - exact (weq_iso_sigma_of_twosided_disp_cat _ _ ∘ weqtotal2 (make_weq _ (HD₁ x₁ x₁ y₁ y₁ (idpath _) (idpath _) (pr1 xy₁) (pr1 xy₂))) (is_univalent_sigma_of_twosided_disp_cat_help HD₂ xy₁ xy₂) ∘ total2_paths_equiv _ _ _)%weq. - intro p. induction p. use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_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.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromSigmaIso. End FromSigmaIso.