Definition from_iso_left_total_of_twosided_disp_cat_pr1 {y : C₂} {xy₁ xy₂ : left_total_of_twosided_disp_cat y} (f : z_iso_disp (identity_z_iso _) xy₁ xy₂) : z_iso (pr1 xy₁) (pr1 xy₂). Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr11 f). - exact (pr112 f). - abstract (refine (maponpaths pr1 (inv_mor_after_z_iso_disp f) @ _) ; unfold mor_disp ; cbn ; rewrite transportb_total2 ; apply idpath). - abstract (refine (maponpaths pr1 (z_iso_disp_after_inv_mor f) @ _) ; unfold mor_disp ; cbn ; rewrite transportb_total2 ; 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.