proposition: Proposition fully_faithful_local_equivalence_mnd : fully_faithful local_equivalence_mnd.
proof: Proof. use full_and_faithful_implies_fully_faithful. split. - exact full_local_equivalence_mnd. - exact faithful_local_equivalence_mnd. 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