Definition is_z_iso_total_twosided_disp_cat_inv : total_twosided_disp_category ⟦ (x₂ ,, y₂ ,, xy₂) , (x₁ ,, y₁ ,, xy₁) ⟧ := inv_from_z_iso f_z_iso ,, inv_from_z_iso g_z_iso ,, iso_inv_twosided_disp Hfg.
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.