Definition twosided_disp_cat_product_ob_mor : twosided_disp_cat_ob_mor (category_binproduct C₁ C₂) (category_binproduct C₃ C₄). Proof. simple refine (_ ,, _). - exact (λ wx yz, D₁ (pr1 wx) (pr1 yz) × D₂ (pr2 wx) (pr2 yz)). - exact (λ wx₁ wx₂ yz₁ yz₂ d₁ d₂ fg hk, pr1 d₁ -->[ pr1 fg ][ pr1 hk ] pr1 d₂ × pr2 d₁ -->[ pr2 fg ][ pr2 hk ] pr2 d₂). 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.