Definition make_z_iso_total_twosided_disp_cat {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D x₁ y₁} {xy₂ : D x₂ y₂} {f : z_iso x₁ x₂} {g : z_iso y₁ y₂} (fg : iso_twosided_disp f g xy₁ xy₂) : @z_iso total_twosided_disp_category (x₁ ,, y₁ ,, xy₁) (x₂ ,, y₂ ,, xy₂). Proof. simple refine (_ ,, _). - exact (pr1 f ,, pr1 g ,, pr1 fg). - use is_z_iso_total_twosided_disp_cat. + exact (pr2 f). + exact (pr2 g). + exact (pr2 fg). 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.