Definition is_twosided_disp_cat_iso_pr1 {wx : category_binproduct C₁ C₂} {yz : category_binproduct C₃ C₄} {d₁ d₂ : twosided_disp_cat_product_data wx yz} (φ : d₁ -->[ identity _ ][ identity _ ] d₂) (Hφ : @is_iso_twosided_disp _ _ twosided_disp_cat_product _ _ _ _ _ _ _ _ (identity_is_z_iso _) (identity_is_z_iso _) φ) : is_iso_twosided_disp (identity_is_z_iso _) (identity_is_z_iso _) (pr1 φ). Proof. simple refine (_ ,, _ ,, _). - exact (pr1 (iso_inv_twosided_disp Hφ)). - abstract (refine (maponpaths pr1 (inv_after_iso_twosided_disp Hφ) @ _) ; rewrite transportb_twosided_disp_cat_product ; cbn ; use transportb_disp_mor2_eq ; apply idpath). - abstract (refine (maponpaths pr1 (iso_after_inv_twosided_disp Hφ) @ _) ; rewrite transportb_twosided_disp_cat_product ; cbn ; use transportb_disp_mor2_eq ; apply idpath). Defined.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.