x,x':A, y,y':B. R(x,y) & R(x',y') 
(x = x' 
y = y')A,B:Type, R:(A
BProp). (R is 1-1) 
TypeA,yB. R(x;y)
Def ==
x,x':A, y,y':B. R(x;y) & R(x';y') (x = x' y = y')A,B:Type, R:(ABType). (1-1 xA,yB. R(x;y)) Type| Some definitions of interest. | |
| rel_1_1 | x,x':A, y,y':B. R(x,y) & R(x',y') (x = x' y = y') |
| A,B:Type, R:(ABProp). (R is 1-1) Type | |
| rel_1_1_b | A,yB. R(x;y)
Def == x,x':A, y,y':B. R(x;y) & R(x';y') (x = x' y = y') |
| A,B:Type, R:(ABType). (1-1 xA,yB. R(x;y)) Type |
About:
 |  |  |  |  |  |  |  |  |  |