Definition op2_comma_has_comma_ump_1 : comma_ump_1 op2_comma_cone. Proof. intro q. pose (q' := make_comma_cone _ (comma_cone_pr2 q : B ⟦ _ , _ ⟧) (comma_cone_pr1 q) (comma_cone_cell q)). use make_comma_1cell ; cbn. - exact (comma_ump_mor comma_sqr q'). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (comma_ump_mor_pr2 comma_sqr q')). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (comma_ump_mor_pr1 comma_sqr q')). - abstract (refine (comma_ump_mor_cell comma_sqr q' @ _) ; cbn ; rewrite !vassocl ; apply idpath). 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.