Definition sigma_disp_z_iso_equiv {x y} {xxx : sigma_disp_cat x} {yyy : sigma_disp_cat y} (f : z_iso x y) : z_iso_disp f xxx yyy ≃ ∑ ff, z_iso_disp (total_z_iso f ff (xx := (_ ,, _)) (yy := (_ ,, _))) (pr2 xxx) (pr2 yyy). Proof. use weq_iso. - exact (sigma_iso_to_iso f). - exact (iso_to_sigma_iso f). - abstract ( intro; apply eq_z_iso_disp; now use total2_paths_f ). - abstract ( intro; use total2_paths_f; [now apply eq_z_iso_disp | apply eq_z_iso_disp]; refine (pr1_transportf (B := λ ff, (pr2 xxx) -->[_ ,, pr1 ff] _) _ _ @ _); refine (functtransportf _ _ _ _ @ _); exact (transportf_set _ _ _ (homset_property _ _ _)) ). 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.