proposition: Proposition faithful_local_equivalence_mnd : faithful local_equivalence_mnd.
proof: Proof. intros f g τ. use invproofirrelevance. intros θ₁ θ₂. induction θ₁ as [ θ₁ p₁ ]. induction θ₂ as [ θ₂ p₂ ]. use subtypePath. { intro. apply cellset_property. } cbn ; cbn in p₁, p₂. use eq_mnd_cell. use (vcomp_lcancel (local_equivalence_counit_inv2cell HF _)). { apply property_from_invertible_2cell. } use (vcomp_rcancel ((local_equivalence_counit_inv2cell HF _)^-1)). { is_iso. } rewrite <- !psfunctor_local_equivalence_inv_twocell. apply maponpaths. exact (maponpaths cell_of_mnd_cell (p₁ @ !p₂)). 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