Definition to_op2_pb_ump_2 : pb_ump_2 (to_op2_pb_cone γ). Proof. intros w φ ψ α β p ; cbn in p. use iscontraprop1. - abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; use (pb_ump_eq H _ _ α β _ _ _ (pr12 ζ₁) (pr22 ζ₁) (pr12 ζ₂) (pr22 ζ₂)) ; cbn ; cbn in p ; rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocr ; use vcomp_move_L_Mp ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocl ; exact p). - simple refine (_ ,, _). + use (pb_ump_cell H ψ φ α β). abstract (cbn ; cbn in p ; rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocr ; use vcomp_move_L_Mp ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocl ; exact p). + split. * apply (pb_ump_cell_pr1 H ψ φ α β). * apply (pb_ump_cell_pr2 H ψ φ α β). 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.