Definition to_op2_pb_ump_1 : pb_ump_1 (to_op2_pb_cone γ). Proof. intro q. use make_pb_1cell ; cbn. - exact (pb_ump_mor H (from_op2_pb_cone q)). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (pb_ump_mor_pr1 H (from_op2_pb_cone q))). - apply weq_op2_invertible_2cell. exact (inv_of_invertible_2cell (pb_ump_mor_pr2 H (from_op2_pb_cone q))). - abstract (cbn ; pose (pb_ump_mor_cell H (from_op2_pb_cone q)) as p ; cbn in p ; use vcomp_move_L_pM ; [ is_iso | ] ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; use vcomp_move_L_pM ; [ apply from_op2_is_invertible_2cell ; apply property_from_invertible_2cell | ] ; cbn ; use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; refine (_ @ !p) ; 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.