\open elements \* [1] 2.1. 2.2. 2.4. *\
- \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop
+ \decl "rule application" App: { [*Obj] [*Obj] [*Obj] } *Prop
- \decl "classification predicate" Cl: *Obj -> *Prop
+ \decl "classification predicate" Cl: [*Obj] *Prop
- \decl "classification membership" Eta: *Obj => *Obj -> *Prop
+ \decl "classification membership" Eta: { [*Obj] [*Obj] } *Prop
\* we must make an explicit coercion from *Obj to *Term *\
- \decl "object-to-term-coercion" T: *Obj -> *Term
+ \decl "object-to-term-coercion" T: [*Obj] *Term
- \decl "term application" At: *Term => *Term -> *Term
+ \decl "term application" At: { [*Term] [*Term] } *Term
- \decl "term-object equivalence" E: *Term => *Obj -> *Prop
+ \decl "term-object equivalence" E: { [*Term] [*Obj] } *Prop
\close
\open logical_abbreviations \* [1] 2.3. 2.5. *\
\def "logical comprehension restricted to classifications"
- CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)
- : (*Obj -> *Prop) -> *Prop
+ CAll = [q:[*Obj]^1 *Prop] All([x:*Obj]^2 Imp(Cl(x), q(x)))
+ : [[*Obj]^1 *Prop] *Prop
\def "logical existence restricted to classifications"
- CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))
- : (*Obj -> *Prop) -> *Prop
+ CEx = [q:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(Cl(x), q(x)))
+ : [[*Obj]^1 *Prop] *Prop
\def "logical comprehension restricted to a classification"
- EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)
- : *Obj => (*Obj -> *Prop) -> *Prop
+ EAll = { [a:*Obj] [q:[*Obj]^1 *Prop] } All([x:*Obj]^2 Imp(Eta(x, a), q(x)))
+ : { [*Obj] [[*Obj]^1 *Prop] } *Prop
\def "logical existence restricted to a classification"
- EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))
- : *Obj => (*Obj -> *Prop) -> *Prop
+ EEx = { [a:*Obj] [q:[*Obj]^1 *Prop] } Ex([x:*Obj]^2 And(Eta(x, a), q(x)))
+ : { [*Obj] [[*Obj]^1 *Prop] } *Prop
\close
\open non_logical_abbreviations \* [1] 2.4. 2.7 *\
\def "object application"
- OAt = [f:*Obj, x:*Obj] At(T(f), T(x)) : *Obj => *Obj -> *Term
+ OAt = { [f:*Obj] [x:*Obj] } At(T(f), T(x)) : { [*Obj] [*Obj] } *Term
\def "convergence of a term to an object"
- Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
+ Conv = [t:*Term] EX([y:*Obj]^2 E(t, y)) : [*Term] *Prop
\def "term-term equivalence"
- Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
- : *Term => *Term -> *Prop
+ Eq = { [t1:*Term] [t2:*Term] } All([y:*Obj]^2 Iff(E(t1, y), E(t2, y)))
+ : { [*Term] [*Term] } *Prop
\def "classification membership of a term"
- TEta = [t:*Term, a:*Obj] EEx(a, [y:*Obj] E(t, y))
- : *Term => *Obj -> *Prop
+ TEta = { [t:*Term] [a:*Obj] } EEx(a, [y:*Obj]^2 E(t, y))
+ : { [*Term] [*Obj] } *Prop
\def "operation (rule with inhabited domain)"
- Op = [f:*Obj] Ex([x:*Obj] Conv(OAt(f, x))) : *Obj -> *Prop
+ Op = [f:*Obj] Ex([x:*Obj]^2 Conv(OAt(f, x))) : [*Obj] *Prop
\def "classification inclusion"
- ESub = [a1:*Obj, a2:*Obj] EAll(a1, [x:*Obj] Eta(x, a2))
- : *Obj => *Obj -> *Prop
+ ESub = { [a1:*Obj] [a2:*Obj] } EAll(a1, [x:*Obj]^2 Eta(x, a2))
+ : { [*Obj] [*Obj] } *Prop
\def "classification morphism"
- ETo = [f:*Obj, a:*Obj, b:*Obj] EAll(a, [x:*Obj] TEta(OAt(f, x), b))
- : *Obj => *Obj => *Obj -> *Prop
+ ETo = { [f:*Obj] [a:*Obj] [ b:*Obj] } EAll(a, [x:*Obj]^2 TEta(OAt(f, x), b))
+ : { [*Obj] [*Obj] [*Obj] } *Prop
\close
\ax e_refl: [y:*Obj] E(T(y), y)
\ax e_at_in: [t1:*Term][t2:*Term][f:*Obj][x:*Obj][y:*Obj]
- E(t1, f) -> E(t2, x) -> App(f, x, y) -> E(At(t1, t2), y)
+ [E(t1, f)] [E(t2, x)] [App(f, x, y)] E(At(t1, t2), y)
\*
- \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y)
+ \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] [E(At(T(f), T(x)), y)] App(f, x, y)
*\
\ax "I (i)" id_dec: [x:*Obj][y:*Obj] Or(Id(x, y), NId(x, y))
\ax "I (ii)" at_mono: [f:*Obj][x:*Obj][y1:*Obj][y2:*Obj]
- E(OAt(f, x), y1) -> E(OAt(f, x), y2) -> Id(y1, y2)
+ [E(OAt(f, x), y1)] [E(OAt(f, x), y2)] Id(y1, y2)
- \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] Eta(x, a) -> Cl(a)
+ \ax "I (iii)" eta_cl: [x:*Obj][a:*Obj] [Eta(x, a)] Cl(a)
\close