Definition from_iso_sigma_of_twosided_disp_cat_pr2 : z_iso_disp (make_z_iso_total_twosided_disp_cat D₁ from_iso_sigma_of_twosided_disp_cat_pr1) (pr2 xy₁) (pr2 xy₂). Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr21 f). - exact (pr212 f). - abstract (assert (p := pr222 f @ maponpaths _ (sigma_transportf_left _ _) @ sigma_transportf_right _ _) ; cbn in p ; rewrite transport_f_f in p ; refine (sigma_mor_eq p @ _) ; cbn ; unfold transportb ; rewrite transport_f_f ; apply transportf_hset_eq ; apply (total_twosided_disp_category D₁)). - abstract (assert (p := pr122 f @ maponpaths _ (sigma_transportf_left _ _) @ sigma_transportf_right _ _) ; cbn in p ; rewrite transport_f_f in p ; refine (sigma_mor_eq p @ _) ; cbn ; unfold transportb ; rewrite transport_f_f ; apply transportf_hset_eq ; apply (total_twosided_disp_category D₁)). 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.