remove notations from Preamble that come from coq-categories

diff --git a/src/Preamble.v b/src/Preamble.v
index 453027a..d10c592 100644 (file)
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -13,6 +13,9 @@ Export Coq.Classes.RelationClasses.
 Export Coq.Classes.Morphisms.
 Export Coq.Setoids.Setoid.
 
+Require Import Notations.
+Export Notations.
+
 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
 Generalizable All Variables.
 
@@ -26,58 +29,21 @@ Reserved Notation "a ,, b"                      (at level 50).
 Reserved Notation "!! f"                        (at level 3).
 Reserved Notation "!` x"                        (at level 2).
 Reserved Notation "`! x"                        (at level 2).
-Reserved Notation "a  ~=>  b"                   (at level 70, right associativity).
-Reserved Notation "H ===> C"                    (at level 100).
-Reserved Notation "f >>=>> g"                   (at level 45).
-Reserved Notation "a ~~{ C }~~> b"              (at level 100).
-Reserved Notation "f <--> g"                    (at level 20).
-Reserved Notation "! f"                         (at level 2).
-Reserved Notation "? f"                         (at level 2).
-Reserved Notation "# f"                         (at level 2).
-Reserved Notation "f '⁻¹'"                      (at level 1).
-Reserved Notation "a ≅ b"                       (at level 70, right associativity).
-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 54).
-Reserved Notation "a ~> b"                      (at level 70, right associativity).
-Reserved Notation "a ≃ b"                       (at level 70, right associativity).
-Reserved Notation "a ≃≃ b"                      (at level 70, right associativity).
-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 "a ⊗ b"                       (at level 40).
-Reserved Notation "a ⊗⊗ b"                      (at level 40).
-Reserved Notation "a ⊕  b"                      (at level 40).
-Reserved Notation "a ⊕⊕ b"                      (at level 40).
-Reserved Notation "f ⋉ A"                       (at level 40).
-Reserved Notation "A ⋊ f"                       (at level 40).
-Reserved Notation "- ⋉ A"                       (at level 40).
-Reserved Notation "A ⋊ -"                       (at level 40).
-Reserved Notation "a *** b"                     (at level 40).
 Reserved Notation "[# f #]"                     (at level 2).
 Reserved Notation "a ---> b"                    (at level 11, right associativity).
 Reserved Notation "a <- b"                      (at level 100, only parsing).
 Reserved Notation "G |= S"                      (at level 75).
-Reserved Notation "F -| G"                      (at level 75).
 Reserved Notation "a :: b"                      (at level 60, right associativity).
 Reserved Notation "a ++ b"                      (at level 60, right associativity).
 Reserved Notation "<[ t @]>"                    (at level 30).
 Reserved Notation "<[ t @ n ]>"                 (at level 30).
 Reserved Notation "<[ e ]>"                     (at level 30).
-Reserved Notation "'Λ' x : t :-> e"             (at level 9, right associativity, x ident).
 Reserved Notation "R ==> R' "                   (at level 55, right associativity).
-Reserved Notation "f ○ g"                       (at level 100).
 Reserved Notation "a ==[ n ]==> b"              (at level 20).
 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
 Reserved Notation "a |== b @@ c"                (at level 100).
-Reserved Notation "f >>>> g"                    (at level 45).
 Reserved Notation "a >>[ n ]<< b"               (at level 100).
-Reserved Notation "f **** g"                    (at level 40).
-Reserved Notation "C × D"                       (at level 40).
-Reserved Notation "C ×× D"                      (at level 45).
-Reserved Notation "C ⁽ºᑭ⁾"                      (at level 1).
 
 Reserved Notation "'<[' a '|-' t ']>'"          (at level 35).
 
@@ -94,11 +60,11 @@ Reserved Notation "Γ '+'    x : c"              (at level 50, x at level 99).
 Reserved Notation "Γ '++'   x : a ∼ b"          (at level 50, x at level 99).
 Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"               (at level 11, φ₂ at level 99, right associativity).
 
+Notation "?? T" := (option T).
 Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
    (at level 52, past at level 99, present at level 50, succedent at level 50).
 
 Reserved Notation "'η'".
-Reserved Notation "'ε'".
 Reserved Notation "'★'".
 
 Close Scope nat_scope.  (* so I can redefine '1' *)
@@ -107,38 +73,3 @@ Delimit Scope arrow_scope   with arrow.
 Delimit Scope biarrow_scope with biarrow.
 Delimit Scope garrow_scope  with garrow.
 
-Notation "f ○ g"    := (fun x => f(g(x))).
-Notation "?? T"     := (option T).
-Notation "a && b"   := (if a then b else false).
-Notation "a || b"   := (if a then true else b).
-
-(* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
-Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
-Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
-Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
-    (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100).
-Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
-    (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100).
-
-Notation "∀ x y z u q , P" := (forall x y z u q , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
-  : type_scope.
-Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
-  (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,
-    right associativity)
-  : type_scope.