Definition disp_dirprod_prebicat_ops : disp_prebicat_ops disp_dirprod_prebicat_1_id_comp_cells. Proof. repeat (use tpair). - cbn. intros. apply (make_dirprod (disp_id2 _ ) (disp_id2 _)). - cbn. intros. apply (make_dirprod (disp_lunitor _ ) (disp_lunitor _)). - cbn. intros. apply (make_dirprod (disp_runitor _ ) (disp_runitor _)). - cbn. intros. apply (make_dirprod (disp_linvunitor _ ) (disp_linvunitor _)). - cbn. intros. apply (make_dirprod (disp_rinvunitor _ ) (disp_rinvunitor _)). - cbn. intros. apply (make_dirprod (disp_rassociator _ _ _ ) (disp_rassociator _ _ _)). - cbn. intros. apply (make_dirprod (disp_lassociator _ _ _ ) (disp_lassociator _ _ _)). - cbn. intros. apply (make_dirprod (disp_vcomp2 (pr1 X) (pr1 X0)) (disp_vcomp2 (pr2 X) (pr2 X0))). - cbn. intros. apply (make_dirprod (disp_lwhisker (pr1 ff) (pr1 X)) (disp_lwhisker (pr2 ff) (pr2 X))). - cbn. intros. apply (make_dirprod (disp_rwhisker (pr1 gg) (pr1 X)) (disp_rwhisker (pr2 gg) (pr2 X))). 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.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.Initial. Require Import UniMath.Bicategories.Core.Examples.Final. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.