tweak long $== notation

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Apr 24, 2024 · d6426eb · d6426eb
1 parent 85b9377
commit d6426eb
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
@@ -399,8 +399,8 @@ Section TwistConstruction.
   Local Infix "⊗R" := (fmap01 cat_tensor) (at level 40) : monoidal_scope.
   Local Infix "⊗L" := (fmap10 cat_tensor) (at level 40) : monoidal_scope.
   Local Notation "f ∘ g" := (f $o g) (at level 61, left associativity, format "f  '/' '∘'  g") : monoidal_scope.
-  Local Notation "f ~[ A ]~ g" := (GpdHom (A := A) f g)
-    (at level 62, format "'[v' '[v' f ']' '/'  ~[ A ]~ '/'  g ']'")
+  Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
+    (at level 80, format "'[v' '[v' f ']' '/'  $== '/'  '[v' g ']'  '/' :>  '[' A ']' ']'")
     : long_path_scope.
   Local Open Scope monoidal_scope.