Definition from_iso_total_twosided_disp_cat_pr12 : z_iso y₁ y₂. Proof. use make_z_iso. - exact (pr121 f). - exact (pr12 (inv_from_z_iso f)). - split. + exact (maponpaths (λ z, pr12 z) (z_iso_inv_after_z_iso f)). + exact (maponpaths (λ z, pr12 z) (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.