Definition sigma_iso_to_iso {x y} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y} (f : z_iso x y) (fff : z_iso_disp f xxx yyy) : ∑ ff, z_iso_disp (total_z_iso f ff (xx := (_ ,, _)) (yy := (_ ,, _))) (pr2 xxx) (pr2 yyy). Proof. use tpair. - repeat use tpair. + exact (pr1 (mor_disp_from_z_iso fff)). + exact (pr1 (inv_mor_disp_from_z_iso fff)). + abstract exact (maponpaths _ (z_iso_disp_after_inv_mor fff) @ pr1_transportf_sigma_disp _ _). + abstract exact (maponpaths _ (inv_mor_after_z_iso_disp fff) @ pr1_transportf_sigma_disp _ _). - repeat use tpair. + exact (pr2 (mor_disp_from_z_iso fff)). + exact (pr2 (inv_mor_disp_from_z_iso fff)). + exact (E_mor_eq (z_iso_inv f) (z_iso_disp_after_inv_mor fff)). + exact (E_mor_eq f (inv_mor_after_z_iso_disp fff)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Limits.