5 \open syntax \* [1] 2.1. *\
7 \decl "logical false" False : *Prop
9 \decl "logical conjunction" And : [p:*Prop, q:*Prop] *Prop
11 \decl "logical disjunction" Or : [p:*Prop, q:*Prop] *Prop
13 \decl "logical implication" Imp : [p:*Prop, q:*Prop] *Prop
15 \decl "logical comprehension" All : [p:[x:*Set]*Prop] *Prop
17 \decl "logical existence" Ex : [p:[x:*Set]*Prop] *Prop
19 \decl "syntactical identity" Id : [x:*Set, y:*Set] *Prop
21 \decl "rule application" App : [f:*Set, x:*Set, y:*Set] *Prop
23 \decl "classification predicate" Cl : [a:*Set] *Prop
25 \decl "classification membership" Eta : [x:*Set, a:*Set] *Prop
27 \decl "object-to-term-coercion" T : [x:*Set] *Term
29 \decl "term application" At : [t:*Term, u:*Term] *Term
31 \decl "term-object equivalence" E : [t:*Term, x:*Set] *Prop
35 \open non_logical_axioms
37 \decl "E: reflexivity" e_refl : [x:*Set] E(T(x), x)