Definition twosided_disp_cat_product_id_comp : twosided_disp_cat_id_comp twosided_disp_cat_product_ob_mor. Proof. simple refine (_ ,, _). - exact (λ wx yz d, id_two_disp (pr1 d) ,, id_two_disp (pr2 d)). - exact (λ wx₁ wx₂ wx₃ yz₁ yz₂ yz₃ d₁ d₂ d₃ fg₁ fg₂ hk₁ hk₂ φ ψ, pr1 φ ;;2 pr1 ψ ,, pr2 φ ;;2 pr2 ψ). 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.