Proposition full_local_equivalence_mnd_cell_laws : is_mnd_cell full_local_equivalence_mnd_cell_data. Proof. unfold is_mnd_cell ; cbn. pose (maponpaths (λ z, z • lunitor _) (mnd_cell_endo τ)) as p. cbn in p. rewrite !vassocl in p. rewrite linvunitor_lunitor in p. rewrite id2_right in p. rewrite vcomp_lunitor in p. rewrite !(maponpaths (λ z, _ • (_ • (_ • z))) (vassocr _ _ _)) in p. rewrite linvunitor_lunitor in p. rewrite id2_left in p. rewrite !vassocr in p. rewrite vcomp_whisker in p. rewrite !vassocl in p. pose (maponpaths (λ z, (_ ◃ (local_equivalence_unit_inv2cell HF (endo_of_mnd m))^-1) • z) p) as q. cbn in q. rewrite !vassocr in q. clear p. rewrite !lwhisker_vcomp in q. rewrite !vcomp_linv in q. rewrite !lwhisker_id2 in q. rewrite !id2_left in q. rewrite !vassocl in q. use (vcomp_rcancel (lunitor _)). { is_iso. } rewrite !vassocl. rewrite vcomp_lunitor. rewrite !vassocr. etrans. { do 2 apply maponpaths_2. rewrite <- local_equivalence_counit_natural_alt. apply idpath. } rewrite !vassocl. pose (maponpaths (λ z, local_equivalence_inv_onecell_comp _ _ _ • z) q) as r. cbn in r. rewrite !vassocr in r. rewrite vcomp_rinv in r. rewrite id2_left in r. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- psfunctor_vcomp. rewrite r. apply idpath. } clear q r. rewrite !vassocr. etrans. { rewrite !psfunctor_vcomp. rewrite !vassocl. rewrite local_equivalence_counit_natural. apply idpath. } rewrite !vassocr. do 2 apply maponpaths_2. rewrite <- !rwhisker_vcomp. rewrite !vassocl. etrans. { do 3 apply maponpaths. Transparent local_equivalence_inv_onecell_comp. cbn -[psfunctor_comp]. rewrite psfunctor_vcomp. rewrite !vassocl. rewrite local_equivalence_counit_natural. rewrite !vassocr. rewrite local_equivalence_triangle1. rewrite id2_left. apply idpath. } etrans. { rewrite !vassocr. do 3 apply maponpaths_2. cbn -[psfunctor_comp]. rewrite !psfunctor_vcomp. rewrite !vassocr. rewrite local_equivalence_counit_natural_alt. rewrite !vassocl. etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite local_equivalence_triangle1_inv. apply id2_left. } rewrite psfunctor_rwhisker. apply idpath. } rewrite !vassocl. apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite vcomp_rinv. rewrite id2_left. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite <- vcomp_whisker. rewrite !vassocl. rewrite lwhisker_vcomp. rewrite vcomp_linv. rewrite lwhisker_id2. apply id2_right. 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.