chore(category_theory/monoidal): some arguments that need to be made …

…explicit in 3.8
leanprover-community · Apr 19, 2020 · d344310 · d344310
1 parent 11d89a2
commit d344310
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/category_theory/monoidal/functorial.lean b/src/category_theory/monoidal/functorial.lean
@@ -49,9 +49,9 @@ include 𝒞 𝒟
 -- but that isn't the immediate plan.
 class lax_monoidal (F : C → D) [functorial.{v₁ v₂} F] :=
 -- unit morphism
-(ε               : 𝟙_ D ⟶ F (𝟙_ C))
+(ε              [] : 𝟙_ D ⟶ F (𝟙_ C))
 -- tensorator
-(μ                : Π X Y : C, (F X) ⊗ (F Y) ⟶ F (X ⊗ Y))
+(μ              []  : Π 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)