Definition disp_cat_to_twosided_disp_cat_id_comp (D : disp_cat (category_binproduct C₁ C₂)) : twosided_disp_cat_id_comp (disp_cat_to_twosided_disp_cat_ob_mor D). Proof. split. - exact (λ x y xy, id_disp _). - refine (λ x₁ x₂ x₃ y₁ y₂ y₃ xy₁ xy₂ xy₃ f₁ f₂ g₁ g₂ fg₁ fg₂, _). cbn in *. exact (fg₁ ;; fg₂)%mor_disp. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.