Definition to_iso_ver_op_twosided_disp_cat {x : C₁} {y : C₂} {xy₁ xy₂ : D x y} (fg : xy₁ -->[ identity _ ][ identity _ ] xy₂) (Hfg : is_iso_twosided_disp (D := D) (identity_is_z_iso _) (identity_is_z_iso _) fg) : is_iso_twosided_disp (D := ver_op_twosided_disp_cat) (identity_is_z_iso _) (identity_is_z_iso _) fg. Proof. simple refine (_ ,, _ ,, _). - exact (iso_inv_twosided_disp Hfg). - abstract (refine (iso_after_inv_twosided_disp Hfg @ _) ; use transportb_disp_mor2_eq ; apply idpath). - abstract (refine (inv_after_iso_twosided_disp Hfg @ _) ; 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.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.