Definition op2_comma_has_comma_ump_2 : comma_ump_2 op2_comma_cone. Proof. intros q φ ψ α β p. use iscontraprop1. - abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; refine (comma_ump_eq comma_sqr _ _ β α _ _ _ (pr22 ζ₁) (pr12 ζ₁) (pr22 ζ₂) (pr12 ζ₂)) ; cbn ; cbn in p ; rewrite !vassocl ; exact (!p)). - simple refine (_ ,, _ ,, _). + use (comma_ump_cell comma_sqr _ _ β α). abstract (cbn ; cbn in p ; rewrite !vassocl ; exact (!p)). + abstract (apply (comma_ump_cell_pr2 comma_sqr)). + abstract (apply (comma_ump_cell_pr1 comma_sqr)). 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.