Library HoTT.Basics.Notations
To reserve this notation, we must first bootstrap, and preserve the underlying ∀ notation
Notation "'forall' x .. y , P" := (∀ x , .. (∀ y, P) ..) (at level 200, x binder, y binder, right associativity).
Reserved Notation "'exists' x .. y , p"
(at level 200, x binder, right associativity,
format "'[' 'exists' '/ ' x .. y , '/ ' p ']'").
Reserved Notation "'exists' x .. y , p"
(at level 200, x binder, right associativity,
format "'[' 'exists' '/ ' x .. y , '/ ' p ']'").
Work around bug 5569, https://coq.inria.fr/bugs/show_bug.cgi?id=5569, Warning skip-spaces-curly,parsing seems bogus
Local Set Warnings Append "-skip-spaces-curly".
These are the notations whose level and associativity are imposed by Coq
Notations for propositional connectives
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x <-> y" (at level 95, no associativity).
Reserved Notation "x /\ y" (at level 80, right associativity).
Reserved Notation "x \/ y" (at level 85, right associativity).
Reserved Notation "x |_| y" (at level 85, right associativity).
Reserved Notation "~ x" (at level 35, right associativity).
Notations for equality and inequalities
Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x = y" (at level 70, no associativity).
Reserved Notation "x = y = z"
(at level 70, no associativity, y at next level).
Reserved Notation "x <> y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x <> y" (at level 70, no associativity).
Reserved Notation "x <= y" (at level 70, no associativity).
Reserved Notation "x < y" (at level 70, no associativity).
Reserved Notation "x >= y" (at level 70, no associativity).
Reserved Notation "x > y" (at level 70, no 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 "x < y <= z" (at level 70, y at next level).
Arithmetical notations (also used for type constructors)
Reserved Notation "x + y" (at level 50, left associativity).
Reserved Notation "x - y" (at level 50, left associativity).
Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "x / y" (at level 40, left associativity).
Reserved Notation "- x" (at level 35, right associativity).
Reserved Notation "/ x" (at level 35, right associativity).
Reserved Notation "x ^ y" (at level 30, right associativity).
Notations for booleans
Reserved Notation "x || y" (at level 50, left associativity).
Reserved Notation "x && y" (at level 40, left associativity).
Notations for pairs
Reserved Notation "( x , y , .. , z )" (at level 0).
Notation "{ x }" is reserved and has a special status as component
of other notations such as "{ A } + { B }" and "A + { B }" (which
are at the same level as "x + y");
"{ x }" is at level 0 to factor with "{ x : A | P }"
Reserved Notation "{ x }" (at level 0, x at level 99).
Notations for sigma-types or subsets
Reserved Notation "{ x | P }" (at level 0, x at level 99).
Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
Numeric
Reserved Notation "n .+1" (at level 2, left associativity, format "n .+1").
Reserved Notation "n .+2" (at level 2, left associativity, format "n .+2").
Reserved Notation "n .+3" (at level 2, left associativity, format "n .+3").
Reserved Notation "n .+4" (at level 2, left associativity, format "n .+4").
Reserved Notation "n .+5" (at level 2, left associativity, format "n .+5").
Reserved Notation "n '.-1'" (at level 2, left associativity, format "n .-1").
Reserved Notation "n '.-2'" (at level 2, left associativity, format "n .-2").
Reserved Notation "m +2+ n" (at level 50, left associativity).
Reserved Infix "mod" (at level 40, no associativity).
Reserved Notation "p ~ 1" (at level 7, left associativity, format "p '~' '1'").
Reserved Notation "p ~ 0" (at level 7, left associativity, format "p '~' '0'").
Reserved Notation "n .+2" (at level 2, left associativity, format "n .+2").
Reserved Notation "n .+3" (at level 2, left associativity, format "n .+3").
Reserved Notation "n .+4" (at level 2, left associativity, format "n .+4").
Reserved Notation "n .+5" (at level 2, left associativity, format "n .+5").
Reserved Notation "n '.-1'" (at level 2, left associativity, format "n .-1").
Reserved Notation "n '.-2'" (at level 2, left associativity, format "n .-2").
Reserved Notation "m +2+ n" (at level 50, left associativity).
Reserved Infix "mod" (at level 40, no associativity).
Reserved Notation "p ~ 1" (at level 7, left associativity, format "p '~' '1'").
Reserved Notation "p ~ 0" (at level 7, left associativity, format "p '~' '0'").
Pointed
Reserved Infix "@*" (at level 30).
Reserved Infix "@@*" (at level 30).
Reserved Infix "<~>*" (at level 85).
Reserved Infix "->*" (at level 99).
Reserved Infix "->**" (at level 99).
Reserved Infix "o*" (at level 40, left associativity).
Reserved Infix "==*" (at level 70, no associativity).
Reserved Notation "g ^*'" (at level 20).
Reserved Notation "f ^*" (at level 3, format "f '^*'").
Reserved Notation "f ^-1*" (at level 3, format "f '^-1*'").
Reserved Notation "g o*E f" (at level 40, left associativity).
Reserved Notation "'ppforall' x .. y , P"
(at level 200, x binder, y binder, right associativity).
Reserved Infix "@@*" (at level 30).
Reserved Infix "<~>*" (at level 85).
Reserved Infix "->*" (at level 99).
Reserved Infix "->**" (at level 99).
Reserved Infix "o*" (at level 40, left associativity).
Reserved Infix "==*" (at level 70, no associativity).
Reserved Notation "g ^*'" (at level 20).
Reserved Notation "f ^*" (at level 3, format "f '^*'").
Reserved Notation "f ^-1*" (at level 3, format "f '^-1*'").
Reserved Notation "g o*E f" (at level 40, left associativity).
Reserved Notation "'ppforall' x .. y , P"
(at level 200, x binder, y binder, right associativity).
Sigma type
Reserved Notation "x .1" (at level 3, format "x '.1'").
Reserved Notation "x .2" (at level 3, format "x '.2'").
Reserved Notation "x .2" (at level 3, format "x '.2'").
Paths
Reserved Notation "p ^" (at level 3, format "p '^'").
Reserved Notation "p @ q" (at level 20).
Reserved Notation "p # x" (right associativity, at level 65).
Reserved Notation "p # x" (right associativity, at level 65).
Reserved Notation "p @@ q" (at level 20).
Reserved Notation "p @' q" (at level 21, left associativity,
format "'[v' p '/' '@'' q ']'").
Reserved Notation "f == g" (at level 70, no associativity).
Reserved Notation "p @ q" (at level 20).
Reserved Notation "p # x" (right associativity, at level 65).
Reserved Notation "p # x" (right associativity, at level 65).
Reserved Notation "p @@ q" (at level 20).
Reserved Notation "p @' q" (at level 21, left associativity,
format "'[v' p '/' '@'' q ']'").
Reserved Notation "f == g" (at level 70, no associativity).
Equivalences
Reserved Notation "A <~> B" (at level 85).
Reserved Notation "f ^-1" (at level 3, format "f '^-1'").
Reserved Notation "m ^-1" (at level 3, format "m '^-1'").
Reserved Notation "g 'oE' f" (at level 40, left associativity).
Reserved Notation "f *E g" (at level 40, left associativity).
Reserved Notation "f +E g" (at level 50, left associativity).
Reserved Notation "f ^-1" (at level 3, format "f '^-1'").
Reserved Notation "m ^-1" (at level 3, format "m '^-1'").
Reserved Notation "g 'oE' f" (at level 40, left associativity).
Reserved Notation "f *E g" (at level 40, left associativity).
Reserved Notation "f +E g" (at level 50, left associativity).
Categories
Reserved Infix "-|" (at level 60, right associativity).
Reserved Infix "<~=~>" (at level 70, no associativity).
Reserved Notation "a // 'CAT'" (at level 40, left associativity).
Reserved Notation "a \\ 'CAT'" (at level 40, left associativity).
Reserved Notation "'CAT' // a" (at level 40, left associativity).
Reserved Notation "'CAT' \\ a" (at level 40, left associativity).
Reserved Notation "C ^op" (at level 3, format "C '^op'").
Reserved Infix "<~=~>" (at level 70, no associativity).
Reserved Notation "a // 'CAT'" (at level 40, left associativity).
Reserved Notation "a \\ 'CAT'" (at level 40, left associativity).
Reserved Notation "'CAT' // a" (at level 40, left associativity).
Reserved Notation "'CAT' \\ a" (at level 40, left associativity).
Reserved Notation "C ^op" (at level 3, format "C '^op'").
Universal algebra
Reserved Notation "u .# A" (at level 3, format "u '.#' A").
Natural numbers
Reserved Infix "=n" (at level 70, no associativity).
Wild cat
Reserved Infix "$->" (at level 99).
Reserved Infix "$<~>" (at level 85).
Reserved Infix "$o" (at level 40, left associativity).
Reserved Infix "$oE" (at level 40, left associativity).
Reserved Infix "$==" (at level 70).
Reserved Infix "$o@" (at level 30).
Reserved Infix "$@" (at level 30).
Reserved Infix "$@L" (at level 30).
Reserved Infix "$@R" (at level 30).
Reserved Infix "$@@" (at level 30).
Reserved Infix "$=>" (at level 99).
Reserved Notation "T ^op" (at level 3, format "T ^op").
Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").
Reserved Notation "f ^$" (at level 3, format "f '^$'").
Reserved Infix "$@h" (at level 35).
Reserved Infix "$@v" (at level 35).
Reserved Infix "$@hR" (at level 34).
Reserved Infix "$@hL" (at level 34).
Reserved Infix "$@vR" (at level 34).
Reserved Infix "$@vL" (at level 34).
Reserved Notation "s ^h$" (at level 20).
Reserved Notation "s ^v$" (at level 20).
Reserved Infix "$<~>" (at level 85).
Reserved Infix "$o" (at level 40, left associativity).
Reserved Infix "$oE" (at level 40, left associativity).
Reserved Infix "$==" (at level 70).
Reserved Infix "$o@" (at level 30).
Reserved Infix "$@" (at level 30).
Reserved Infix "$@L" (at level 30).
Reserved Infix "$@R" (at level 30).
Reserved Infix "$@@" (at level 30).
Reserved Infix "$=>" (at level 99).
Reserved Notation "T ^op" (at level 3, format "T ^op").
Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").
Reserved Notation "f ^$" (at level 3, format "f '^$'").
Reserved Infix "$@h" (at level 35).
Reserved Infix "$@v" (at level 35).
Reserved Infix "$@hR" (at level 34).
Reserved Infix "$@hL" (at level 34).
Reserved Infix "$@vR" (at level 34).
Reserved Infix "$@vL" (at level 34).
Reserved Notation "s ^h$" (at level 20).
Reserved Notation "s ^v$" (at level 20).
Displayed wild cat
Reserved Infix "$o'" (at level 40, left associativity).
Reserved Infix "$@'" (at level 30).
Reserved Infix "$@L'" (at level 30).
Reserved Infix "$@R'" (at level 30).
Reserved Infix "$@@'" (at level 30).
Reserved Infix "$oE'" (at level 40, left associativity).
Reserved Notation "f ^$'" (at level 3, format "f '^$''").
Reserved Notation "f ^-1$'" (at level 3, format "f '^-1$''").
Reserved Infix "$@'" (at level 30).
Reserved Infix "$@L'" (at level 30).
Reserved Infix "$@R'" (at level 30).
Reserved Infix "$@@'" (at level 30).
Reserved Infix "$oE'" (at level 40, left associativity).
Reserved Notation "f ^$'" (at level 3, format "f '^$''").
Reserved Notation "f ^-1$'" (at level 3, format "f '^-1$''").
Cubical
Reserved Infix "@@h" (at level 30).
Reserved Infix "@@v" (at level 30).
Reserved Infix "@lr" (at level 30).
Reserved Notation "x '@Dp' y" (at level 20).
Reserved Notation "x '@Dr' y" (at level 20).
Reserved Notation "x '@Dl' y" (at level 20).
Reserved Notation "x '^D'" (at level 3).
Reserved Infix "@@v" (at level 30).
Reserved Infix "@lr" (at level 30).
Reserved Notation "x '@Dp' y" (at level 20).
Reserved Notation "x '@Dr' y" (at level 20).
Reserved Notation "x '@Dl' y" (at level 20).
Reserved Notation "x '^D'" (at level 3).
Lists
Reserved Infix "::" (at level 60, right associativity).
Reserved Infix "++" (right associativity, at level 60).
Reserved Infix "++" (right associativity, at level 60).
Other / Not sorted yet
Reserved Infix "<=>" (at level 70).
Reserved Infix "<<" (at level 70).
Reserved Infix "<<<" (at level 70).
Reserved Infix "oL" (at level 40, left associativity).
Reserved Infix "oR" (at level 40, left associativity).
Reserved Notation "~~ A" (at level 35, right associativity).
Reserved Notation "a \ C" (at level 40, left associativity).
Reserved Notation "a <=_{ x } b" (at level 70, no associativity).
Reserved Notation "D1 ~d~ D2" (at level 65).
Reserved Notation "D '_f' g" (at level 10).
Reserved Notation "F '_0' x" (at level 10, no associativity).
Reserved Notation "F '_0' x" (at level 10, no associativity).
Reserved Notation "F '_1' m" (at level 10, no associativity).
Reserved Notation "F ^op" (at level 3, format "F ^op").
Reserved Notation "'forall' x .. y , P" (at level 200, x binder, y binder, right associativity).
Reserved Notation "g 'oD' f" (at level 40, left associativity).
Reserved Notation "g 'o' f" (at level 40, left associativity).
Reserved Notation "m <= n" (at level 70, no associativity).
Reserved Notation "n -Type" (at level 1).
Reserved Notation "p ..1" (at level 3).
Reserved Notation "p ..2" (at level 3).
Reserved Notation "!! P" (at level 35, right associativity).
Reserved Notation "[ u ]" (at level 9).
Reserved Notation "u ~~ v" (at level 30).
Reserved Notation " [ u , v ] " (at level 9).
Reserved Notation "! x" (at level 3, format "'!' x").
Reserved Notation "x \\ F" (at level 40, left associativity).
Reserved Notation "x // F" (at level 40, left associativity).
Reserved Notation "{ { xL | xR // xcut } }" (at level 0, xR at level 39, format "{ { xL | xR // xcut } }").
Reserved Notation "x \ F" (at level 40, left associativity).
Reserved Notation "x <> y" (at level 70, no associativity).
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 55, right associativity, y at level 55).
Reserved Notation "x (-> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x <> y :> T" (at level 70, y at next level, no associativity).
Reserved Notation "Z ** W" (at level 30, right associativity).
Reserved Notation "'+N'" (at level 55).
Reserved Notation "'+Z'" (at level 55).
Reserved Notation "'N3'" (at level 55).
Reserved Notation "'Z3'" (at level 55).
Reserved Notation "a ^+" (at level 0).
Reserved Notation "a ^+ k" (at level 0).
Reserved Notation "x ^++" (at level 0).
Reserved Notation "x ^++ k" (at level 0).
Reserved Notation "b ^+f" (at level 0).
Mathclasses
Reserved Notation "' x" (at level 20).
Reserved Notation "// x" (at level 40, no associativity).
Reserved Infix "?=" (at level 70, no associativity).
Reserved Infix "=?" (at level 70, no associativity).
Reserved Infix "<?" (at level 70, no associativity).
Reserved Infix "<=?" (at level 70, no associativity).
Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Infix "=N=" (at level 70, no associativity).
Reserved Infix ":::" (at level 60, right associativity).
Reserved Notation "// x" (at level 40, no associativity).
Reserved Infix "?=" (at level 70, no associativity).
Reserved Infix "=?" (at level 70, no associativity).
Reserved Infix "<?" (at level 70, no associativity).
Reserved Infix "<=?" (at level 70, no associativity).
Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Infix "=N=" (at level 70, no associativity).
Reserved Infix ":::" (at level 60, right associativity).
TODO: move?
We define various scopes and open them in the order we expect to use them.
Notation scopes
Declare Scope core_scope.
Declare Scope function_scope.
Declare Scope type_scope.
Declare Scope equiv_scope.
Declare Scope path_scope.
Declare Scope fibration_scope.
Declare Scope trunc_scope.
Declare Scope long_path_scope.
Delimit Scope core_scope with core.
Delimit Scope function_scope with function.
Delimit Scope type_scope with type.
Delimit Scope equiv_scope with equiv.
Delimit Scope function_scope with function.
Delimit Scope path_scope with path.
Delimit Scope fibration_scope with fibration.
Delimit Scope trunc_scope with trunc.
Global Open Scope trunc_scope.
Global Open Scope equiv_scope.
Global Open Scope path_scope.
Global Open Scope fibration_scope.
Global Open Scope function_scope.
Global Open Scope type_scope.
Global Open Scope core_scope.
Bind Scope function_scope with Funclass.
Bind Scope type_scope with Sortclass.
Declare Scope function_scope.
Declare Scope type_scope.
Declare Scope equiv_scope.
Declare Scope path_scope.
Declare Scope fibration_scope.
Declare Scope trunc_scope.
Declare Scope long_path_scope.
Delimit Scope core_scope with core.
Delimit Scope function_scope with function.
Delimit Scope type_scope with type.
Delimit Scope equiv_scope with equiv.
Delimit Scope function_scope with function.
Delimit Scope path_scope with path.
Delimit Scope fibration_scope with fibration.
Delimit Scope trunc_scope with trunc.
Global Open Scope trunc_scope.
Global Open Scope equiv_scope.
Global Open Scope path_scope.
Global Open Scope fibration_scope.
Global Open Scope function_scope.
Global Open Scope type_scope.
Global Open Scope core_scope.
Bind Scope function_scope with Funclass.
Bind Scope type_scope with Sortclass.