Definition weq_iso_sigma_of_twosided_disp_cat_help_eq {x : C₁} {y : C₂} {xy₁ : sigma_twosided_disp_cat x y} {xy₂ : sigma_twosided_disp_cat x y} (h₁ h₂ : ∑ (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₂)) (p : pr11 h₁ = pr11 h₂) (q : pr12 h₁ = transportb (λ z, pr2 xy₁ -->[ z ] pr2 xy₂) (maponpaths (λ (z : pr1 xy₁ -->[ identity _ ][ identity _ ] pr1 xy₂), _ ,, _ ,, z) p) (pr12 h₂)) : h₁ = h₂.
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.