proposition: Proposition essentially_surjective_local_equivalence_mnd_inv_laws : mnd_mor_laws essentially_surjective_local_equivalence_mnd_inv_data.
proof: Proof. split. - cbn -[psfunctor_id psfunctor_comp]. rewrite id2_rwhisker, id2_right. refine (!_). etrans. { rewrite <- lwhisker_vcomp. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite <- psfunctor_lwhisker. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite <- psfunctor_rinvunitor. rewrite <- !psfunctor_vcomp. do 2 apply maponpaths_2. apply maponpaths. exact (!(mnd_mor_unit f)). } cbn -[psfunctor_id psfunctor_comp]. rewrite id2_rwhisker, id2_right. rewrite !vassocl. use vcomp_move_R_Mp ; [ is_iso | ]. cbn -[psfunctor_id psfunctor_comp]. rewrite !vassocr. rewrite <- psfunctor_linvunitor. apply idpath. - cbn -[psfunctor_id psfunctor_comp]. rewrite <- !rwhisker_vcomp. rewrite <- !lwhisker_vcomp. rewrite !vassocl. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite <- psfunctor_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. do 2 apply maponpaths_2. rewrite <- psfunctor_vcomp. apply maponpaths. exact (!(mnd_mor_mu f)). } rewrite !psfunctor_vcomp. etrans. { rewrite !vassocr. do 7 apply maponpaths_2. rewrite psfunctor_lassociator. apply idpath. } rewrite !vassocl. do 2 apply maponpaths. etrans. { rewrite !vassocr. rewrite psfunctor_rwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ]. cbn -[psfunctor_id psfunctor_comp]. etrans. { rewrite !vassocr. rewrite psfunctor_rassociator. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite !vassocr. rewrite psfunctor_lwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. refine (!_). etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } use vcomp_move_R_pM ; [ is_iso | ]. cbn -[psfunctor_id psfunctor_comp]. etrans. { rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite rwhisker_lwhisker. rewrite !vassocr. rewrite <- rwhisker_rwhisker. apply idpath. } refine (!_). etrans. { rewrite !vassocr. rewrite psfunctor_lassociator. rewrite !vassocl. apply idpath. } rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite psfunctor_rwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_rinv. apply id2_left. } rewrite !rwhisker_vcomp. apply maponpaths. use vcomp_move_L_pM ; [ is_iso | ]. cbn -[psfunctor_id psfunctor_comp]. etrans. { rewrite !vassocr. rewrite <- psfunctor_lunitor. apply idpath. } rewrite vcomp_lunitor. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.Monads.Examples.PsfunctorOnMonad UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Properties UniMath.Bicategories.PseudoFunctors.LocalEquivalenceProperties UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion