From 4a795318d6c1f76352cb79af423755a9a0882d94 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 4 Apr 2023 11:45:54 +1000 Subject: [PATCH] chore(category_theory/monad/basic): remove some simp lemmas --- src/category_theory/monad/basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/category_theory/monad/basic.lean b/src/category_theory/monad/basic.lean index 3ed6b2bcf7ec4..69302b5bd815b 100644 --- a/src/category_theory/monad/basic.lean +++ b/src/category_theory/monad/basic.lean @@ -226,7 +226,6 @@ def monad_to_functor : monad C ⥤ (C ⥤ C) := instance : faithful (monad_to_functor C) := {}. -@[simp] lemma monad_to_functor_map_iso_monad_iso_mk {M N : monad C} (f : (M : C ⥤ C) ≅ N) (f_η f_μ) : (monad_to_functor _).map_iso (monad_iso.mk f f_η f_μ) = f := by { ext, refl } @@ -249,7 +248,6 @@ def comonad_to_functor : comonad C ⥤ (C ⥤ C) := instance : faithful (comonad_to_functor C) := {}. -@[simp] lemma comonad_to_functor_map_iso_comonad_iso_mk {M N : comonad C} (f : (M : C ⥤ C) ≅ N) (f_ε f_δ) : (comonad_to_functor _).map_iso (comonad_iso.mk f f_ε f_δ) = f := by { ext, refl }