From d3f37111cfa52dd74cf9bb013f926ddb116d6916 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 15:50:40 +0100
Subject: [PATCH 1/6] feat: port CategoryTheory.Monoidal.Functorial


From 8b695cd3eccc1b52f08aa8bb065b7d0ee723a82b Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 15:50:40 +0100
Subject: [PATCH 2/6] Initial file copy from mathport

---
 .../CategoryTheory/Monoidal/Functorial.lean   | 133 ++++++++++++++++++
 1 file changed, 133 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Functorial.lean

diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
new file mode 100644
index 0000000000000..7487a6cee24f8
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module category_theory.monoidal.functorial
+! leanprover-community/mathlib commit 73dd4b5411ec8fafb18a9d77c9c826907730af80
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.CategoryTheory.Monoidal.Functor
+import Mathbin.CategoryTheory.Functor.Functorial
+
+/-!
+# Unbundled lax monoidal functors
+
+## Design considerations
+The essential problem I've encountered that requires unbundled functors is
+having an existing (non-monoidal) functor `F : C ⥤ D` between monoidal categories,
+and wanting to assert that it has an extension to a lax monoidal functor.
+
+The two options seem to be
+1. Construct a separate `F' : lax_monoidal_functor C D`,
+   and assert `F'.to_functor ≅ F`.
+2. Introduce unbundled functors and unbundled lax monoidal functors,
+   and construct `lax_monoidal F.obj`, then construct `F' := lax_monoidal_functor.of F.obj`.
+
+Both have costs, but as for option 2. the cost is in library design,
+while in option 1. the cost is users having to carry around additional isomorphisms forever,
+I wanted to introduce unbundled functors.
+
+TODO:
+later, we may want to do this for strong monoidal functors as well,
+but the immediate application, for enriched categories, only requires this notion.
+-/
+
+
+open CategoryTheory
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+open CategoryTheory.Category
+
+open CategoryTheory.Functor
+
+namespace CategoryTheory
+
+open MonoidalCategory
+
+variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  [MonoidalCategory.{v₂} D]
+
+/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`ε] [] -/
+/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`μ] [] -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+-- Perhaps in the future we'll redefine `lax_monoidal_functor` in terms of this,
+-- but that isn't the immediate plan.
+/-- An unbundled description of lax monoidal functors. -/
+class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
+  -- unit morphism
+  ε : 𝟙_ D ⟶ F (𝟙_ C)
+  -- tensorator
+  μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)
+  μ_natural' :
+    ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
+      (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by
+    obviously
+  -- associativity of the tensorator
+  associativity' :
+    ∀ X Y Z : C,
+      (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).Hom =
+        (α_ (F X) (F Y) (F Z)).Hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+    obviously
+  -- unitality
+  left_unitality' : ∀ X : C, (λ_ (F X)).Hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).Hom := by
+    obviously
+  right_unitality' : ∀ X : C, (ρ_ (F X)).Hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).Hom := by
+    obviously
+#align category_theory.lax_monoidal CategoryTheory.LaxMonoidal
+
+restate_axiom lax_monoidal.μ_natural'
+
+attribute [simp] lax_monoidal.μ_natural
+
+restate_axiom lax_monoidal.left_unitality'
+
+restate_axiom lax_monoidal.right_unitality'
+
+-- The unitality axioms cannot be used as simp lemmas because they require
+-- higher-order matching to figure out the `F` and `X` from `F X`.
+restate_axiom lax_monoidal.associativity'
+
+attribute [simp] lax_monoidal.associativity
+
+namespace LaxMonoidalFunctor
+
+/-- Construct a bundled `lax_monoidal_functor` from the object level function
+and `functorial` and `lax_monoidal` typeclasses.
+-/
+@[simps]
+def of (F : C → D) [I₁ : Functorial.{v₁, v₂} F] [I₂ : LaxMonoidal.{v₁, v₂} F] :
+    LaxMonoidalFunctor.{v₁, v₂} C D :=
+  { I₁, I₂ with obj := F }
+#align category_theory.lax_monoidal_functor.of CategoryTheory.LaxMonoidalFunctor.of
+
+end LaxMonoidalFunctor
+
+instance (F : LaxMonoidalFunctor.{v₁, v₂} C D) : LaxMonoidal.{v₁, v₂} F.obj :=
+  { F with }
+
+section
+
+instance laxMonoidalId : LaxMonoidal.{v₁, v₁} (id : C → C)
+    where
+  ε := 𝟙 _
+  μ X Y := 𝟙 _
+#align category_theory.lax_monoidal_id CategoryTheory.laxMonoidalId
+
+end
+
+-- TODO instances for composition, as required
+-- TODO `strong_monoidal`, as well as `lax_monoidal`
+end CategoryTheory
+

From 548f839fafde9477b5896e2255a17b52934a7fee Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 15:50:40 +0100
Subject: [PATCH 3/6] automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
---
 Mathlib.lean                                    | 1 +
 Mathlib/CategoryTheory/Monoidal/Functorial.lean | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 8edf9b49cc0f6..29da970a3dc44 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -274,6 +274,7 @@ import Mathlib.CategoryTheory.Limits.Cones
 import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Functor
+import Mathlib.CategoryTheory.Monoidal.Functorial
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites
diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
index 7487a6cee24f8..4b5d62ff8a47e 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -8,8 +8,8 @@ Authors: Scott Morrison
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.Monoidal.Functor
-import Mathbin.CategoryTheory.Functor.Functorial
+import Mathlib.CategoryTheory.Monoidal.Functor
+import Mathlib.CategoryTheory.Functor.Functorial
 
 /-!
 # Unbundled lax monoidal functors

From eb0e46d9552fc376103578653de207c8cab1d1bd Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 15:58:00 +0100
Subject: [PATCH 4/6] make it build

---
 .../CategoryTheory/Monoidal/Functorial.lean   | 42 +++++++++----------
 1 file changed, 19 insertions(+), 23 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
index 4b5d62ff8a47e..153692e3ccfeb 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -66,40 +66,37 @@ variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Ty
 -- but that isn't the immediate plan.
 /-- An unbundled description of lax monoidal functors. -/
 class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
-  -- unit morphism
+  /-- unit morphism -/
   ε : 𝟙_ D ⟶ F (𝟙_ C)
-  -- tensorator
+  /-- tensorator -/
   μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)
-  μ_natural' :
+  /-- natuality -/
+  μ_natural :
     ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
       (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by
-    obviously
-  -- associativity of the tensorator
-  associativity' :
+   aesop_cat
+  /-- associativity of the tensorator -/
+  associativity :
     ∀ X Y Z : C,
-      (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).Hom =
-        (α_ (F X) (F Y) (F Z)).Hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
-    obviously
-  -- unitality
-  left_unitality' : ∀ X : C, (λ_ (F X)).Hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).Hom := by
-    obviously
-  right_unitality' : ∀ X : C, (ρ_ (F X)).Hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).Hom := by
-    obviously
+      (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom =
+        (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+    aesop_cat
+  /-- left unitality -/
+  left_unitality : ∀ X : C, (λ_ (F X)).hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom := by
+    aesop_cat
+  /-- right unitality -/
+  right_unitality : ∀ X : C, (ρ_ (F X)).hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom := by
+    aesop_cat
 #align category_theory.lax_monoidal CategoryTheory.LaxMonoidal
 
-restate_axiom lax_monoidal.μ_natural'
+attribute [simp] LaxMonoidal.μ_natural
 
-attribute [simp] lax_monoidal.μ_natural
-
-restate_axiom lax_monoidal.left_unitality'
-
-restate_axiom lax_monoidal.right_unitality'
+attribute [simp] LaxMonoidal.μ_natural
 
 -- The unitality axioms cannot be used as simp lemmas because they require
 -- higher-order matching to figure out the `F` and `X` from `F X`.
-restate_axiom lax_monoidal.associativity'
 
-attribute [simp] lax_monoidal.associativity
+attribute [simp] LaxMonoidal.associativity
 
 namespace LaxMonoidalFunctor
 
@@ -130,4 +127,3 @@ end
 -- TODO instances for composition, as required
 -- TODO `strong_monoidal`, as well as `lax_monoidal`
 end CategoryTheory
-

From 12079e24e2465f51cbff12dd8bf269f8beb5a769 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 16:00:22 +0100
Subject: [PATCH 5/6] remove automated port comments, fixing line length lint

---
 Mathlib/CategoryTheory/Monoidal/Functorial.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
index 153692e3ccfeb..cdb5f7e1a0495 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -50,18 +50,6 @@ open MonoidalCategory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Type u₂} [Category.{v₂} D]
   [MonoidalCategory.{v₂} D]
 
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`ε] [] -/
-/- ./././Mathport/Syntax/Translate/Command.lean:388:30: infer kinds are unsupported in Lean 4: #[`μ] [] -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 -- Perhaps in the future we'll redefine `lax_monoidal_functor` in terms of this,
 -- but that isn't the immediate plan.
 /-- An unbundled description of lax monoidal functors. -/

From 8db538d5d714483ac6d21ed1370ee00aa1a5dd05 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 26 Feb 2023 21:55:02 +0100
Subject: [PATCH 6/6] naming

---
 Mathlib/CategoryTheory/Monoidal/Functorial.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
index cdb5f7e1a0495..3a6ff397a2268 100644
--- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean
@@ -20,10 +20,10 @@ having an existing (non-monoidal) functor `F : C ⥤ D` between monoidal categor
 and wanting to assert that it has an extension to a lax monoidal functor.
 
 The two options seem to be
-1. Construct a separate `F' : lax_monoidal_functor C D`,
-   and assert `F'.to_functor ≅ F`.
+1. Construct a separate `F' : LaxMonoidalFunctor C D`,
+   and assert `F'.toFunctor ≅ F`.
 2. Introduce unbundled functors and unbundled lax monoidal functors,
-   and construct `lax_monoidal F.obj`, then construct `F' := lax_monoidal_functor.of F.obj`.
+   and construct `LaxMonoidal F.obj`, then construct `F' := LaxMonoidalFunctor.of F.obj`.
 
 Both have costs, but as for option 2. the cost is in library design,
 while in option 1. the cost is users having to carry around additional isomorphisms forever,
@@ -50,7 +50,7 @@ open MonoidalCategory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] {D : Type u₂} [Category.{v₂} D]
   [MonoidalCategory.{v₂} D]
 
--- Perhaps in the future we'll redefine `lax_monoidal_functor` in terms of this,
+-- Perhaps in the future we'll redefine `LaxMonoidalFunctor` in terms of this,
 -- but that isn't the immediate plan.
 /-- An unbundled description of lax monoidal functors. -/
 class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
@@ -88,8 +88,8 @@ attribute [simp] LaxMonoidal.associativity
 
 namespace LaxMonoidalFunctor
 
-/-- Construct a bundled `lax_monoidal_functor` from the object level function
-and `functorial` and `lax_monoidal` typeclasses.
+/-- Construct a bundled `LaxMonoidalFunctor` from the object level function
+and `Functorial` and `LaxMonoidal` typeclasses.
 -/
 @[simps]
 def of (F : C → D) [I₁ : Functorial.{v₁, v₂} F] [I₂ : LaxMonoidal.{v₁, v₂} F] :
@@ -113,5 +113,5 @@ instance laxMonoidalId : LaxMonoidal.{v₁, v₁} (id : C → C)
 end
 
 -- TODO instances for composition, as required
--- TODO `strong_monoidal`, as well as `lax_monoidal`
+-- TODO `StrongMonoidal`, as well as `LaxMonoidal`
 end CategoryTheory