Definition twosided_disp_cat_product_iso_weq {wx : category_binproduct C₁ C₂} {yz : category_binproduct C₃ C₄} (d₁ d₂ : twosided_disp_cat_product_data wx yz) : iso_twosided_disp (identity_z_iso (pr1 wx)) (identity_z_iso (pr1 yz)) (pr1 d₁) (pr1 d₂) × iso_twosided_disp (identity_z_iso (pr2 wx)) (identity_z_iso (pr2 yz)) (pr2 d₁) (pr2 d₂) ≃ @iso_twosided_disp _ _ twosided_disp_cat_product _ _ _ _ (identity_z_iso wx) (identity_z_iso yz) d₁ d₂. Proof. use weq_iso. - exact (λ fghk, twosided_disp_cat_product_iso_weq_map (pr1 fghk) (pr2 fghk)). - exact (λ φ, twosided_disp_cat_product_iso_weq_inv_pr1 φ ,, twosided_disp_cat_product_iso_weq_inv_pr2 φ). - abstract (intros fghk ; use dirprodeq ; (use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ]) ; apply idpath). - abstract (intros φ ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; 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.