feat: add LaxMonoidal instance for Applicative functors (leanprover-community#30407)

Since similar conversions exist for `Functor`s and `Monad`s.

Author: viliml

Mathlib.lean

@@ -2616,6 +2616,7 @@ import Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
 import Mathlib.CategoryTheory.Monoidal.Free.Basic
 import Mathlib.CategoryTheory.Monoidal.Free.Coherence
 import Mathlib.CategoryTheory.Monoidal.Functor
+import Mathlib.CategoryTheory.Monoidal.Functor.Types
 import Mathlib.CategoryTheory.Monoidal.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Grp_
 import Mathlib.CategoryTheory.Monoidal.Hopf_

Mathlib/CategoryTheory/Monoidal/Functor/Types.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Vilim Lendvaj. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vilim Lendvaj
+-/
+import Mathlib.CategoryTheory.Monoidal.Functor
+import Mathlib.CategoryTheory.Monoidal.Types.Basic
+import Mathlib.CategoryTheory.Types.Basic
+import Mathlib.Tactic.Simps.Basic
+
+/-!
+# Convert from `Applicative` to `CategoryTheory.Functor.LaxMonoidal`
+
+This allows us to use Lean's `Type`-based applicative functors in category theory.
+
+-/
+
+namespace CategoryTheory
+
+section
+
+variable (F : Type* → Type*) [Applicative F] [LawfulApplicative F]
+
+attribute [local simp] map_seq seq_map_assoc
+  LawfulApplicative.pure_seq LawfulApplicative.seq_assoc in
+/-- A lawful `Applicative` gives a category theory `LaxMonoidal` functor
+between categories of types. -/
+@[simps]
+instance : (ofTypeFunctor F).LaxMonoidal where
+  ε _ : F _ := pure PUnit.unit
+  μ _ _ p : F _ := Prod.mk <$> p.1 <*> p.2
+
+end
+
+end CategoryTheory