Definition from_is_iso_twosided_disp_cat_on_disp_cat_id {x : E₁} {y : E₂} {xy₁ xy₂ : twosided_disp_cat_on_disp_cat x y} (fg : xy₁ -->[ identity _ ][ identity _ ] xy₂) (Hfg : is_iso_twosided_disp (identity_is_z_iso x) (identity_is_z_iso y) fg) : is_iso_twosided_disp (identity_is_z_iso (pr1 x)) (identity_is_z_iso (pr1 y)) 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.