Definition dirprod_disp_cat_id_comp {C : precategory_data} (D1 D2 : disp_cat_data C) : disp_cat_id_comp _ (dirprod_disp_cat_ob_mor D1 D2). Proof. apply tpair. - intros x (x1, x2). exact (id_disp x1,, id_disp x2). - intros x y z f g xx yy zz ff gg. exact ((pr1 ff ;; pr1 gg),, (pr2 ff ;; pr2 gg)). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.