T
x,y:T. x = y 
(eq(x,y))T:Type. EqDecider(T) 
Typex dom(f) 
P(x;f(x))b == 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))| Some definitions of interest. | |
| deq | Tx,y:T. x = y (eq(x,y)) |
| T:Type. EqDecider(T) Type | |
| fpf-val | x dom(f) P(x;f(x)) |
| 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)) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |