Definition weq_z_iso_total_twosided_disp_cat {x₁ x₂ : C₁} {y₁ y₂ : C₂} (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂) : (∑ (f : z_iso x₁ x₂) (g : z_iso y₁ y₂), iso_twosided_disp f g xy₁ xy₂) ≃ (@z_iso total_twosided_disp_category (x₁ ,, y₁ ,, xy₁) (x₂ ,, y₂ ,, xy₂)). Proof. use weq_iso. - exact (λ fg, make_z_iso_total_twosided_disp_cat (pr22 fg)). - exact from_iso_total_twosided_disp_cat. - abstract (intros f ; use weq_z_iso_total_twosided_disp_cat_help_eq ; apply idpath). - abstract (intros f ; use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ; apply idpath). 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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromIsoTotal. End FromIsoTotal.