Definition weq_iso_sigma_of_twosided_disp_cat {x : C₁} {y : C₂} (xy₁ : sigma_twosided_disp_cat x y) (xy₂ : sigma_twosided_disp_cat x y) : (∑ (f : iso_twosided_disp (identity_z_iso x) (identity_z_iso y) (pr1 xy₁) (pr1 xy₂)), z_iso_disp (make_z_iso_total_twosided_disp_cat _ f) (pr2 xy₁) (pr2 xy₂)) ≃ @iso_twosided_disp _ _ sigma_twosided_disp_cat _ _ _ _ (identity_z_iso x) (identity_z_iso y) xy₁ xy₂. Proof. use weq_iso. - exact (λ f, to_iso_sigma_of_twosided_disp_cat (pr1 f) (pr2 f)). - intro f. simple refine (_ ,, _). + exact (from_iso_sigma_of_twosided_disp_cat_pr1 f). + exact (from_iso_sigma_of_twosided_disp_cat_pr2 f). - intro f. use weq_iso_sigma_of_twosided_disp_cat_help_eq ; apply idpath. - abstract (intro f ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; 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.