From d6426ebc428605aafbd6e0d7ca9b0c1184557a21 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 24 Apr 2024 02:02:57 +0100 Subject: [PATCH] tweak long $== notation Signed-off-by: Ali Caglayan --- theories/WildCat/Monoidal.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index 93405a8e0b6..e2e81366f07 100644 --- 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.