Definition disp_dirprod_binprod {B : bicat} (HB : has_binprod B) (D₁ D₂ : disp_bicat B) (HD₁ : disp_has_binprod D₁ HB) (HD₂ : disp_has_binprod D₂ HB) : disp_has_binprod (disp_dirprod_bicat D₁ D₂) HB. Proof. simple refine (λ x y, _ ,, _ ,, _ ,, λ z f g, _). - simple refine (_ ,, _). + exact (pr1 (HD₁ (pr1 x ,, pr12 x) (pr1 y ,, pr12 y))). + exact (pr1 (HD₂ (pr1 x ,, pr22 x) (pr1 y ,, pr22 y))). - simple refine (_ ,, _). + exact (pr12 (HD₁ (pr1 x ,, pr12 x) (pr1 y ,, pr12 y))). + exact (pr12 (HD₂ (pr1 x ,, pr22 x) (pr1 y ,, pr22 y))). - simple refine (_ ,, _). + exact (pr122 (HD₁ (pr1 x ,, pr12 x) (pr1 y ,, pr12 y))). + exact (pr122 (HD₂ (pr1 x ,, pr22 x) (pr1 y ,, pr22 y))). - simple refine (_ ,, _). + exact (pr222 (HD₁ (pr1 x ,, pr12 x) (pr1 y ,, pr12 y)) (pr1 z ,, pr12 z) (pr1 f ,, pr12 f) (pr1 g ,, pr12 g)). + exact (pr222 (HD₂ (pr1 x ,, pr22 x) (pr1 y ,, pr22 y)) (pr1 z ,, pr22 z) (pr1 f ,, pr22 f) (pr1 g ,, pr22 g)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Limits.Examples.TotalBicategoryLimits. Require Import UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.