Definition has_binprod_ump_1_op_cell (q : @binprod_cone (op2_bicat B) x y) : binprod_1cell q op2_binprod_cone. Proof. pose (k₁ := binprod_cone_pr1 q). pose (k₂ := binprod_cone_pr2 q). use make_binprod_1cell. - exact (binprod_ump_1cell ump k₁ k₂). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (binprod_ump_1cell_pr1 ump _ k₁ k₂)). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (binprod_ump_1cell_pr2 ump _ k₁ k₂)). 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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Limits.EilenbergMooreComonad. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.