Definition make_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₂)) (fg : iso_twosided_disp f (identity_z_iso _) (pr2 xy₁) (pr2 xy₂)) : z_iso_disp (identity_z_iso _) xy₁ xy₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr1 f ,, pr1 fg). - exact (pr12 f ,, pr12 fg). - abstract (unfold mor_disp ; cbn ; rewrite transportb_total2 ; cbn ; use total2_paths_f ; [ apply z_iso_after_z_iso_inv | ] ; cbn ; etrans ; [ apply maponpaths ; apply (iso_after_inv_twosided_disp (pr2 fg)) | ] ; apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _)). - abstract (unfold mor_disp ; cbn ; rewrite transportb_total2 ; cbn ; use total2_paths_f ; [ apply z_iso_inv_after_z_iso | ] ; cbn ; etrans ; [ apply maponpaths ; apply (inv_after_iso_twosided_disp (pr2 fg)) | ] ; apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _)). 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.