chore(category_theory/closed): move one thing to monoidal closed and …

…fix naming (#3090)

Move one of the CCC defs to MCC as an example, and make the naming consistent.

src/category_theory/closed/cartesian.lean

@@ -63,12 +63,9 @@ The terminal object is always exponentiable.
 This isn't an instance because most of the time we'll prove cartesian closed for all objects
 at once, rather than just for this one.
 -/
-def terminal_exponentiable {C : Type u} [category.{v} C] [has_finite_products.{v} C] : exponentiable ⊤_C :=
-{ is_adj :=
-  { right := 𝟭 C,
-    adj := adjunction.mk_of_hom_equiv
-    { hom_equiv := λ X _, have unitor : _, from prod.left_unitor X,
-        ⟨λ a, unitor.inv ≫ a, λ a, unitor.hom ≫ a, by tidy, by tidy⟩ } } }
+def terminal_exponentiable {C : Type u} [category.{v} C] [has_finite_products.{v} C] :
+  exponentiable ⊤_C :=
+unit_closed
 
 /--
 A category `C` is cartesian closed if it has finite products and every object is exponentiable.
@@ -99,7 +96,7 @@ def coev : 𝟭 C ⟶ prod_functor.obj A ⋙ exp A :=
 closed.is_adj.adj.unit
 
 notation A ` ⟹ `:20 B:20 := (exp A).obj B
-notation A ` ^^ `:30 B:30 := (exp A).obj B
+notation B ` ^^ `:30 A:30 := (exp A).obj B
 
 @[simp, reassoc] lemma ev_coev : limits.prod.map (𝟙 A) ((coev A).app B) ≫ (ev A).app (A ⨯ B) = 𝟙 (A ⨯ B) :=
 adjunction.left_triangle_components (exp.adjunction A)
@@ -112,7 +109,7 @@ end exp
 variables {A}
 
 -- Wrap these in a namespace so we don't clash with the core versions.
-namespace is_cartesian_closed
+namespace cartesian_closed
 
 variables [has_finite_products.{v} C] [exponentiable A]
 
@@ -123,9 +120,9 @@ def curry : (A ⨯ Y ⟶ X) → (Y ⟶ A ⟹ X) :=
 def uncurry : (Y ⟶ A ⟹ X) → (A ⨯ Y ⟶ X) :=
 (closed.is_adj.adj.hom_equiv _ _).inv_fun
 
-end is_cartesian_closed
+end cartesian_closed
 
-open is_cartesian_closed
+open cartesian_closed
 
 variables [has_finite_products.{v} C] [exponentiable A]
 

src/category_theory/closed/monoidal.lean

@@ -31,4 +31,21 @@ class monoidal_closed (C : Type u) [category.{v} C] [monoidal_category.{v} C] :=
 
 attribute [instance, priority 100] monoidal_closed.closed
 
+/--
+The unit object is always closed.
+This isn't an instance because most of the time we'll prove closedness for all objects at once,
+rather than just for this one.
+-/
+def unit_closed {C : Type u} [category.{v} C] [monoidal_category.{v} C] : closed (𝟙_ C) :=
+{ is_adj :=
+  { right := 𝟭 C,
+    adj := adjunction.mk_of_hom_equiv
+    { hom_equiv := λ X _,
+      { to_fun := λ a, (left_unitor X).inv ≫ a,
+        inv_fun := λ a, (left_unitor X).hom ≫ a,
+        left_inv := by tidy,
+        right_inv := by tidy },
+      hom_equiv_naturality_left_symm' := λ X' X Y f g,
+      by { dsimp, rw left_unitor_naturality_assoc } } } }
+
 end category_theory

src/category_theory/monoidal/category.lean

@@ -69,8 +69,11 @@ attribute [simp] monoidal_category.tensor_id
 restate_axiom monoidal_category.tensor_comp'
 attribute [simp] monoidal_category.tensor_comp
 restate_axiom monoidal_category.associator_naturality'
+attribute [reassoc] monoidal_category.associator_naturality
 restate_axiom monoidal_category.left_unitor_naturality'
+attribute [reassoc] monoidal_category.left_unitor_naturality
 restate_axiom monoidal_category.right_unitor_naturality'
+attribute [reassoc] monoidal_category.right_unitor_naturality
 restate_axiom monoidal_category.pentagon'
 restate_axiom monoidal_category.triangle'
 attribute [simp] monoidal_category.triangle