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