L1Definition. We define
False to be
∀p : prop, p of type
prop.
L1Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop.
Notation. We use
¬ as a prefix operator with priority 700 corresponding to applying term
not.
L6Definition. We define
and to be
λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type
prop → prop → prop.
Notation. We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and.
L11Definition. We define
or to be
λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type
prop → prop → prop.
Notation. We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or.
Beginning of Section Eq
L19Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
L20Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop.
End of Section Eq
Notation. We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq.
Notation. We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq.
Beginning of Section Ex
L29Definition. We define
ex to be
λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type
(A → prop) → prop.
End of Section Ex
Notation. We use
∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex.
Primitive. The name
In is a term of type
set → set → prop.
Notation. We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In. Furthermore, we may write
∀ x ∈ A, B to mean
∀ x : set, x ∈ A → B.
L36Definition. We define
Subq to be
λA B ⇒ ∀x ∈ A, x ∈ B of type
set → set → prop.
Notation. We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq. Furthermore, we may write
∀ x ⊆ A, B to mean
∀ x : set, x ⊆ A → B.
Notation. We use
∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and.
Primitive. The name
Empty is a term of type
set.
Primitive. The name
ordsucc is a term of type
set → set.
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc.
Primitive. The name
𝒫 is a term of type
set → set.
Primitive. The name
equip is a term of type
set → set → prop.