j == if i=j
true ; false fi
i,j:
. (i=j) 
a1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(A
B). Inj(A; B; f) Prop| i
k & kj }i,j:. {i...j} Type
b T == 
a = b TA:Type, x,y:A. (x y) Prop| Some definitions of interest. | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| inject | a1,a2:A. f(a1) = f(a2) B a1 = a2 |
| A,B:Type, f:(AB). Inj(A; B; f) Prop | |
| int_iseg | | ik & kj } |
| i,j:. {i...j} Type | |
| nequal | b T == a = b T |
| A:Type, x,y:A. (x y) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |