Convert from Applicative to CategoryTheory.Functor.LaxMonoidal #
This allows us to use Lean's Type-based applicative functors in category theory.
@[implicit_reducible]
instance
CategoryTheory.instLaxMonoidalOfTypeFunctor
(F : Type u_1 → Type u_2)
[Applicative F]
[LawfulApplicative F]
:
A lawful Applicative gives a category theory LaxMonoidal functor
between categories of types.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.μ_def
(F : Type u_1 → Type u_2)
[Applicative F]
[LawfulApplicative F]
(x✝ x✝¹ : Type u_1)
:
Functor.LaxMonoidal.μ (ofTypeFunctor F) x✝ x✝¹ = TypeCat.ofHom fun (p : MonoidalCategoryStruct.tensorObj ((ofTypeFunctor F).obj x✝) ((ofTypeFunctor F).obj x✝¹)) =>
Prod.mk <$> p.1 <*> p.2
@[simp]
theorem
CategoryTheory.ε_def
(F : Type u_1 → Type u_2)
[Applicative F]
[LawfulApplicative F]
:
Functor.LaxMonoidal.ε (ofTypeFunctor F) = TypeCat.ofHom fun (x : MonoidalCategoryStruct.tensorUnit (Type u_2)) => pure PUnit.unit