| | Some definitions of interest. |
|
| hzero_rep | Def zero_rep == @x: . ( y:.  x = suc_rep(y)  ) |
| | | Thm* zero_rep hind |
|
| hsuc_rep | Def suc_rep ==  x:. (@f:  . (one_one(;;f) & onto(;;f)))(x) |
| | | Thm* suc_rep (hind hind) |
|
| label | Def t ...$L == t |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
| | | Thm* S |
|
| ncompose | Def ncompose(f;n;x) == if n= 0 then x else f(ncompose(f;n-1;x)) fi (recursive) |
| | | Thm* 'a:Type, n:, x:'a, f:('a'a). ncompose(f;n;x) 'a |
|
| not | Def A == A   False |
| | | Thm* A:Prop. (A) Prop |
|
| one_one | Def one_one('a;'b;f) == x,y:'a. f(x) = f(y) 'b x = y |
| | | Thm* 'a,'b:Type, f:('a'b). one_one('a;'b;f) Prop |
|
| onto | Def onto('a;'b;f) == y:'b.  x:'a. y = f(x) |
| | | Thm* 'a,'b:Type, f:('a'b). onto('a;'b;f) Prop |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
