A,B,C:Type, f:(B
C), g:(AB). f o g 
ACA,B,C,B',C':Type, g:(AB
C), f1:(BB'), f2:(CC'). (f1,f2) o g AB'C'| Some definitions of interest. | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| compose2 | Def (f1,f2) o g(x) == g(x)/x,y. < f1(x),f2(y) > |
| Thm* A,B,C,B',C':Type, g:(ABC), f1:(BB'), f2:(CC'). (f1,f2) o g AB'C' |
About:
 |  |  |  |  |  |  |  |  |