Definition from_is_iso_twosided_disp_cat_on_disp_cat {x₁ x₂ : E₁} {f : x₁ --> x₂} (Hf : is_z_isomorphism f) {y₁ y₂ : E₂} {g : y₁ --> y₂} (Hg : is_z_isomorphism g) {xy₁ : twosided_disp_cat_on_disp_cat x₁ y₁} {xy₂ : twosided_disp_cat_on_disp_cat x₂ y₂} (fg : xy₁ -->[ f ][ g ] xy₂) (Hfg : is_iso_twosided_disp Hf Hg fg) : is_iso_twosided_disp (is_z_iso_base_from_total Hf) (is_z_iso_base_from_total Hg) fg. Proof. simple refine (_ ,, _ ,, _). - exact (iso_inv_twosided_disp Hfg). - abstract (refine (inv_after_iso_twosided_disp Hfg @ _) ; rewrite transportb_disp_mor2_twosided_disp_cat_on_disp_cat ; cbn ; use transportb_disp_mor2_eq ; apply idpath). - abstract (refine (iso_after_inv_twosided_disp Hfg @ _) ; rewrite transportb_disp_mor2_twosided_disp_cat_on_disp_cat ; cbn ; use transportb_disp_mor2_eq ; apply idpath). 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.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total.