Update theories/Categories/Monoidal/MonoidalCategory.v

Co-authored-by: Jason Gross <jasongross9@gmail.com>
HoTT · May 16, 2022 · b0cacec · b0cacec
1 parent 9b8f062
commit b0cacec
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Categories/Monoidal/MonoidalCategory.v b/theories/Categories/Monoidal/MonoidalCategory.v
@@ -25,7 +25,7 @@ Section MonoidalCategoryConcepts.
   Variable tensor : ((C * C) -> C)%category.
   Variable I : C.
 
-  Local Notation "A ⊗ B" := (tensor (Datatypes.pair A B)) (at level 45, left associativity).
+  Local Notation "A ⊗ B" := (tensor (Datatypes.pair A B)).
 
   Local Open Scope functor_scope.
   Definition right_assoc := (tensor ∘ (Functor.Prod.pair 1 tensor) )%functor.