Proposition faithful_local_equivalence_mnd : faithful local_equivalence_mnd. 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.
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.