X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FNotations.v;h=26c3ac16c999e5156c9ac19c65e9decafab2e363;hp=3ea525ba24a4aac9e7333c8b8e9abc85c26ac50b;hb=469c709f122da80a207769aab3cd038fd1c3d509;hpb=90844bf411c7cddcd92d48c0b020e5775ace0849

diff --git a/src/Notations.v b/src/Notations.v
index 3ea525b..26c3ac1 100644
--- a/src/Notations.v
+++ b/src/Notations.v
@@ -28,6 +28,7 @@ Reserved Notation "a ≅ b"                       (at level 70, right associativ
 Reserved Notation "C 'ᵒᴾ'"                      (at level 1).
 Reserved Notation "F \ a"                       (at level 20).
 Reserved Notation "f >>> g"                     (at level 45).
+Reserved Notation "a >>≅>> b"                   (at level 45).
 Reserved Notation "a ~~ b"                      (at level 54).
 Reserved Notation "a ~> b"                      (at level 70, right associativity).
 Reserved Notation "a ≃ b"                       (at level 70, right associativity).
@@ -35,6 +36,7 @@ Reserved Notation "a ≃≃ b"                      (at level 70, right associat
 Reserved Notation "a ~~> b"                     (at level 70, right associativity).
 Reserved Notation "F  ~~~> G"                   (at level 70, right associativity).
 Reserved Notation "F <~~~> G"                   (at level 70, right associativity).
+Reserved Notation "F <~~⊗~~> G"                 (at level 70, right associativity).
 Reserved Notation "a ⊗ b"                       (at level 40).
 Reserved Notation "a ⊗⊗ b"                      (at level 40).
 Reserved Notation "a ⊕  b"                      (at level 40).
@@ -50,6 +52,7 @@ Reserved Notation "a :: b"                      (at level 60, right associativit
 Reserved Notation "a ++ b"                      (at level 60, right associativity).
 Reserved Notation "f ○ g"                       (at level 100).
 Reserved Notation "f >>>> g"                    (at level 45).
+Reserved Notation "a >>⊗>> b"                   (at level 20).
 Reserved Notation "f **** g"                    (at level 40).
 Reserved Notation "C × D"                       (at level 40).
 Reserved Notation "C ×× D"                      (at level 45).