A,B,C,B',C':Type, g:(A
B
C), f1:(BB'), f2:(CC'). (f1,f2) o g 
AB'C'| Who Cites compose2? | |
| 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' |
| Syntax: | (f1,f2) o g | has structure: | compose2(f1; f2; g) |
About:
 |  |  |  |  |  |  |  |  |