Reserved Notation "'∀'  x .. y , P"
  (at level 200, x binder, y binder, right associativity).
Reserved Notation "'∃'  x .. y , P"
  (at level 200, x binder, y binder, right associativity).
Reserved Notation "'λ'  x .. y , t"
  (at level 200, x binder, y binder, right associativity).
Identifier 'λ' now a keyword

Reserved Notation "x ∧ y" (at level 80, right associativity).
Reserved Notation "x → y" (at level 99, y at level 200, right associativity).
Reserved Notation "x ↔ y" (at level 95, no associativity).
(*Notation "¬ x" (at level 75, right associativity).*)
(*Notation "x ≠ y" (at level 70).*)

Reserved Infix "∩" (at level 20).
Reserved Infix "⋅" (at level 20).
Reserved Infix "∙" (at level 20).
Reserved Infix "∘" (at level 40, left associativity).
Reserved Infix "∘ˡ" (at level 40, left associativity).
Reserved Infix "∘ʳ" (at level 40, left associativity).
Reserved Infix "⊣" (at level 60, right associativity).
Reserved Infix "≅" (at level 70, no associativity).
Reserved Notation "A 'ᵒᵖ'" (at level 1).
Identifier 'ᵒᵖ' now a keyword
Reserved Notation "A × B" (at level 40, left associativity).
Reserved Notation "a ≤ b" (at level 70, no associativity).
Reserved Notation "A ≃ B" (at level 85).
#[warnings="-postfix-notation-not-level-1"]
Reserved Notation "a ⇓ 'CAT'" (at level 40, left associativity).
#[warnings="-postfix-notation-not-level-1"]
Reserved Notation "a ⇑ 'CAT'" (at level 40, left associativity).
Reserved Notation "a ≤_{ x } b" (at level 70, no associativity).
Reserved Notation "C ↓ a" (at level 70, no associativity).
Reserved Notation "'CAT' ⇓ a" (at level 40, left associativity).
Identifier 'CAT' now a keyword
Reserved Notation "'CAT' ⇑ a" (at level 40, left associativity).
Reserved Notation "C → D" (at level 99, D at level 200, right associativity).
Reserved Notation "f '⁻¹'" (at level 1, format "f '⁻¹'").
(* Reserved Notation "f ×ᴱ g" (at level 40, no associativity). *)
(* Reserved Notation "f *ᴱ g" (at level 40, no associativity). *)
Reserved Notation "f +ᴱ g" (at level 50, left associativity).
Reserved Notation "F ₁ m" (at level 10, no associativity).
Reserved Notation "F ₀ x" (at level 10, no associativity).
Reserved Notation "g ∘ f" (at level 40, left associativity).
Reserved Notation "g ∘ᴱ f" (at level 40, left associativity).
Reserved Notation "m ≤ n" (at level 70, no associativity).
Reserved Notation "p • q" (at level 20).
Reserved Notation "p •' q" (at level 21, left associativity, format "'[v' p '/' '•''  q ']'").
#[warnings="-postfix-notation-not-level-1"]
Reserved Notation "x ₁" (at level 10).
Reserved Notation "x ₂" (at level 1).
Reserved Notation "¬ x" (at level 35, right associativity).
Reserved Notation "x ⇓ F" (at level 40, left associativity).
Reserved Notation "x ⇑ F" (at level 40, left associativity).
Reserved Notation "x ∈ v" (at level 30).
Reserved Notation "x ⊆ y" (at level 30).
Reserved Notation "x ≠ y" (at level 70).
Reserved Notation "x ⇸ y" (at level 99, right associativity, y at level 200).
Reserved Notation "x ↠ y" (at level 99, right associativity, y at level 200).
Reserved Notation "x ↪ y" (at level 99, right associativity, y at level 200).
Reserved Notation "A ⊗ B" (at level 45, left associativity).
(* Reserved Notation "∀  x .. y , P" (at level 200, x binder, y binder, right associativity). *)
Reserved Notation "x ∨ y" (at level 85, right associativity).
(* Reserved Notation "x ⊔ y" (at level 85, right associativity). *)

Reserved Infix "≶" (at level 70, no associativity).
Reserved Infix "⊓" (at level 50, no associativity).
Reserved Infix "⊔" (at level 50, no associativity).
Reserved Infix "∸" (at level 50, left associativity).
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y ≤ z" (at level 70, y at next level).

Reserved Notation "'π'" (at level 0).