fact: 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).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence