fact: 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₂.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.CategoryTheory.TwoSidedDisplayedCats.Total