f:(A
BA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) 
b1 = b2) (a,a':A. Dec(
b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) 
Graph(a,a':A. b:B. a' = f(a,b))f:(AB). Id o f = fg:(AB
C). (Id,Id) o g = g| Rank | Theorem | Name |
| 2 | Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b)) | [fun-graph-rel-graph] |
| cites | ||
| 1 | Thm* f:(AB). Id o f = f | [comp_id_l] |
| 0 | Thm* g:(ABC). (Id,Id) o g = g | [comp2_id_l] |