Definition is_isotwosided_disp_twosided_disp_cat_product {wx : category_binproduct C₁ C₂} {yz : category_binproduct C₃ C₄} {d₁ d₂ : twosided_disp_cat_product_data wx yz} {fg : pr1 d₁ -->[ identity _ ][ identity _ ] pr1 d₂} (Hfg : is_iso_twosided_disp (identity_is_z_iso (pr1 wx)) (identity_is_z_iso (pr1 yz)) fg) {hk : pr2 d₁ -->[ identity _ ][ identity _ ] pr2 d₂} (Hhk : is_iso_twosided_disp (identity_is_z_iso (pr2 wx)) (identity_is_z_iso (pr2 yz)) hk) : @is_iso_twosided_disp _ _ twosided_disp_cat_product _ _ _ _ _ _ _ _ (identity_is_z_iso wx) (identity_is_z_iso yz) (fg ,, hk). Proof. simple refine (_ ,, _ ,, _). - exact (iso_inv_twosided_disp Hfg ,, iso_inv_twosided_disp Hhk). - abstract (cbn ; rewrite transportb_twosided_disp_cat_product ; use dirprodeq ; cbn ; [ refine (inv_after_iso_twosided_disp Hfg @ _) | refine (inv_after_iso_twosided_disp Hhk @ _) ] ; use transportb_disp_mor2_eq ; apply idpath). - abstract (cbn ; rewrite transportb_twosided_disp_cat_product ; use dirprodeq ; cbn ; [ refine (iso_after_inv_twosided_disp Hfg @ _) | refine (iso_after_inv_twosided_disp Hhk @ _) ] ; 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.