Proposition essentially_surjective_local_equivalence_mnd_inv_laws : mnd_mor_laws essentially_surjective_local_equivalence_mnd_inv_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.PsfunctorOnMonad. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Properties. Require Import UniMath.Bicategories.PseudoFunctors.LocalEquivalenceProperties. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.