Definition to_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₂)) (g : 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. simple refine (_ ,, _ ,, _ ,, _). - exact (pr1 f ,, pr1 g). - exact (pr12 f ,, inv_mor_disp_from_z_iso g). - abstract (unfold transportb_disp_mor2, transportf_disp_mor2 ; rewrite sigma_transportf_left ; rewrite sigma_transportf_right ; use sigma_twosided_disp_cat_mor_eq ; [ exact (pr122 f) | ] ; etrans ; [ apply maponpaths ; exact (inv_mor_after_z_iso_disp g) | ] ; unfold transportb ; cbn ; rewrite !transport_f_f ; apply transportf_hset_eq ; apply (total_twosided_disp_category D₁)). - abstract (unfold transportb_disp_mor2, transportf_disp_mor2 ; rewrite sigma_transportf_left ; rewrite sigma_transportf_right ; use sigma_twosided_disp_cat_mor_eq ; [ exact (pr222 f) | ] ; etrans ; [ apply maponpaths ; exact (z_iso_disp_after_inv_mor g) | ] ; unfold transportb ; cbn ; 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.