Definition weq_iso_left_total_of_twosided_disp_cat {y : C₂} (xy₁ xy₂ : left_total_of_twosided_disp_cat y) : (∑ (f : z_iso (pr1 xy₁) (pr1 xy₂)), iso_twosided_disp f (identity_z_iso _) (pr2 xy₁) (pr2 xy₂)) ≃ z_iso_disp (identity_z_iso _) xy₁ xy₂. Proof. use weq_iso. - exact (λ f, make_iso_left_total_of_twosided_disp_cat (pr1 f) (pr2 f)). - exact (λ f, from_iso_left_total_of_twosided_disp_cat_pr1 f ,, from_iso_left_total_of_twosided_disp_cat_pr2 f). - abstract (intro f ; cbn ; use weq_iso_left_total_of_twosided_disp_cat_eq_help ; apply idpath). - abstract (intro f ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; 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.