3 \* Feferman's system T0 *\
5 \open elements \* [1] 2.1. 2.2. 2.4. *\
7 \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
9 \decl "classification predicate" Cl: *Obj -> *Prop
11 \decl "classification membership" Eta: *Obj => *Obj -> *Prop
13 \* we must make an explicit coercion from *Obj to *Term *\
14 \decl "object-to-term-coercion" T: *Obj -> *Term
16 \decl "term application" At: *Term => *Term -> *Term
18 \decl "term-object equivalence" E: *Term => *Obj -> *Prop
22 \open logical_abbreviations \* [1] 2.3. *\
26 \open non_logical_axioms \* [1] 2.4. *\
28 \* we axiomatize E because *Term is not inductively generated *\
29 \ax e_refl: [y:*Obj] E(T(y), y)
31 \ax e_at_in: [f:*Obj][x:*Obj][y:*Obj] App(f,x,y) -> E(At(T(f), T(x)), y)
33 \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y)