Definition mirror_has_pb_ump : has_pb_ump (mirror_cone cone). Proof. split. - intros q. use make_pb_1cell. + exact (pb_ump_mor pb_sqr (mirror_cone q)). + exact (pb_ump_mor_pr2 pb_sqr (mirror_cone q)). + exact (pb_ump_mor_pr1 pb_sqr (mirror_cone q)). + abstract (pose (r := pb_ump_mor_cell pb_sqr (mirror_cone q)) ; cbn in r ; cbn ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; do 2 (use vcomp_move_L_pM ; [ is_iso | ] ; cbn) ; rewrite !vassocl in r ; exact (!r)). - intros w φ ψ α β q. use iscontraprop1. + abstract (use invproofirrelevance ; intros ζ₁ ζ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; refine (pb_ump_eq pb_sqr φ ψ β α _ _ _ (pr22 ζ₁) (pr12 ζ₁) (pr22 ζ₂) (pr12 ζ₂)) ; rewrite !vassocl ; cbn in q ; use vcomp_move_R_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocr ; rewrite q ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_right ; apply idpath). + simple refine (_ ,, _ ,, _). * use (pb_ump_cell pb_sqr φ ψ β α). abstract (rewrite !vassocl ; cbn in q ; use vcomp_move_R_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; rewrite !vassocr ; rewrite q ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_right ; apply idpath). * exact (pb_ump_cell_pr2 pb_sqr φ ψ β α _). * exact (pb_ump_cell_pr1 pb_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.