Definition from_iso_total_twosided_disp_cat_pr22 : iso_twosided_disp from_iso_total_twosided_disp_cat_pr1 from_iso_total_twosided_disp_cat_pr12 xy₁ xy₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr221 f). - exact (pr22 (inv_from_z_iso f)). - exact (from_eq_total (z_iso_inv_after_z_iso f)). - exact (from_eq_total (z_iso_after_z_iso_inv f)). 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.