feat(category_theory): functions to convert is_lawful_functor and is_… (

leanprover-community#1258)

* feat(category_theory): functions to convert is_lawful_functor and is_lawful_monad to their corresponding category_theory concepts

* Fix typo

* feat(category): add mjoin_map_pure, mjoin_pure to the simpset (and use <$> notation)

src/category/basic.lean

@@ -138,6 +138,29 @@ def list.mmap_accuml (f : β' → α → m' (β' × γ')) : β' → list α →
 
 end monad
 
+section
+variables {m : Type u → Type u} [monad m] [is_lawful_monad m]
+
+lemma mjoin_map_map {α β : Type u} (f : α → β) (a : m (m α)) :
+  mjoin (functor.map f <$> a) = f <$> (mjoin a) :=
+by simp only [mjoin, (∘), id.def,
+  (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, map_bind, pure_bind]
+
+lemma mjoin_map_mjoin {α : Type u} (a : m (m (m α))) :
+  mjoin (mjoin <$> a) = mjoin (mjoin a) :=
+by simp only [mjoin, (∘), id.def,
+  map_bind, (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, pure_bind]
+
+@[simp] lemma mjoin_map_pure {α : Type u} (a : m α) :
+  mjoin (pure <$> a) = a :=
+by simp only [mjoin, (∘), id.def,
+  map_bind, (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, pure_bind, bind_pure]
+
+@[simp] lemma mjoin_pure {α : Type u} (a : m α) : mjoin (pure a) = a :=
+is_lawful_monad.pure_bind a id
+
+end
+
 section alternative
 variables {F : Type → Type v} [alternative F]
 

src/category_theory/monad/default.lean

@@ -1 +1,3 @@
-import category_theory.monad.limits
+import
+  category_theory.monad.limits
+  category_theory.monad.types

src/category_theory/monad/types.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+
+import category_theory.monad.basic
+import category_theory.types
+
+/-!
+
+# Convert from `monad` (i.e. Lean's `Type`-based monads) to `category_theory.monad`
+
+This allows us to use these monads in category theory.
+
+-/
+
+namespace category_theory
+
+section
+universes u
+
+variables (m : Type u → Type u) [_root_.monad m] [is_lawful_monad m]
+
+instance : monad (of_type_functor m) :=
+{ η           := ⟨@pure m _, assume α β f, (is_lawful_applicative.map_comp_pure m f).symm ⟩,
+  μ           := ⟨@mjoin m _, assume α β (f : α → β), funext $ assume a, mjoin_map_map f a ⟩,
+  assoc'      := assume α, funext $ assume a, mjoin_map_mjoin a,
+  left_unit'  := assume α, funext $ assume a, mjoin_pure a,
+  right_unit' := assume α, funext $ assume a, mjoin_map_pure a }
+
+end
+
+end category_theory

src/category_theory/types.lean

@@ -110,6 +110,28 @@ begin
     exact (congr_fun H₂ x : _) }
 end
 
+section
+
+/-- `of_type_functor m` converts from Lean's `Type`-based `category` to `category_theory`. This
+allows us to use these functors in category theory. -/
+def of_type_functor (m : Type u → Type v) [_root_.functor m] [is_lawful_functor m] :
+  Type u ⥤ Type v :=
+{ obj       := m,
+  map       := λα β, _root_.functor.map,
+  map_id'   := assume α, _root_.functor.map_id,
+  map_comp' := assume α β γ f g, funext $ assume a, is_lawful_functor.comp_map f g _ }
+
+variables (m : Type u → Type v) [_root_.functor m] [is_lawful_functor m]
+
+@[simp]
+lemma of_type_functor_obj : (of_type_functor m).obj = m := rfl
+
+@[simp]
+lemma of_type_functor_map {α β} (f : α → β) :
+  (of_type_functor m).map f = (_root_.functor.map f : m α → m β) := rfl
+
+end
+
 end category_theory
 
 -- Isomorphisms in Type and equivalences.