T
x,y:T. x = y 
(eq(x,y))T:Type. EqDecider(T) 
Typeb == if b
True else False fib:. b Propa:{a:A| (a d) }B(a)A:Type, B:(AType). a:A fp-> B(a) Type dom(f) == deq-member(eq;x;1of(f))
1. b(1))(1) == b(1) Type| Some definitions of interest. | |
| deq | Tx,y:T. x = y (eq(x,y)) |
| T:Type. EqDecider(T) Type | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| fpf | a:{a:A| (a d) }B(a) |
| A:Type, B:(AType). a:A fp-> B(a) Type | |
| fpf-dom | dom(f) == deq-member(eq;x;1of(f)) |
| so_lambda1 | 1. b(1))(1) == b(1) |
| top | |
| Type |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |  |