x:T. P(x) == 
(x:T. 
P(x))T:Type, P:(T
). (x:T. P(x)) 
b == if b
True else False fib:. b Prop y == (x = y T)T:Type, x,y:T. (x = y) 
x:T. True } Type{2}
x:T. b(x))(x) == b(x)| Some definitions of interest. | |
| ball | x:T. P(x) == (x:T. P(x)) |
| T:Type, P:(T). (x:T. P(x)) | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| bequal | y == (x = y T) |
| T:Type, x,y:T. (x = y) | |
| stype | x:T. True } |
| Type{2} | |
| tlambda | x:T. b(x))(x) == b(x) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |