Convert from monad (i.e. Lean's Type-based monads) to category_theory.monad
This allows us to use these monads in category theory.
@[instance]
Equations
- category_theory.of_type_functor.monad m = {η := {app := pure applicative.to_has_pure, naturality' := _}, μ := {app := mjoin _inst_1, naturality' := _}, assoc' := _, left_unit' := _, right_unit' := _}
The Kleisli category of a control.monad is equivalent to the kleisli category of its
category-theoretic version, provided the monad is lawful.
Equations
- category_theory.eq m = {functor := {obj := λ (X : category_theory.Kleisli m), X, map := λ (X Y : category_theory.Kleisli m) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}, inverse := {obj := λ (X : category_theory.kleisli (category_theory.of_type_functor m)), X, map := λ (X Y : category_theory.kleisli (category_theory.of_type_functor m)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.Kleisli m), category_theory.iso.refl X) _, counit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.kleisli (category_theory.of_type_functor m)), category_theory.iso.refl X) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.eq_inverse_obj
(m : Type u → Type u)
[monad m]
[is_lawful_monad m]
(X : category_theory.kleisli (category_theory.of_type_functor m)) :
(category_theory.eq m).inverse.obj X = X
@[simp]
@[simp]
theorem
category_theory.eq_functor_obj
(m : Type u → Type u)
[monad m]
[is_lawful_monad m]
(X : category_theory.Kleisli m) :
(category_theory.eq m).functor.obj X = X
@[simp]
theorem
category_theory.eq_inverse_map
(m : Type u → Type u)
[monad m]
[is_lawful_monad m]
(X Y : category_theory.kleisli (category_theory.of_type_functor m))
(f : X ⟶ Y)
(ᾰ : X) :
(category_theory.eq m).inverse.map f ᾰ = f ᾰ
@[simp]
theorem
category_theory.eq_functor_map
(m : Type u → Type u)
[monad m]
[is_lawful_monad m]
(X Y : category_theory.Kleisli m)
(f : X ⟶ Y)
(ᾰ : X) :
(category_theory.eq m).functor.map f ᾰ = f ᾰ
@[simp]