A,B,C,B',C':Type, g:(A
B
C), f1:(BB'), f2:(CC'). (f1,f2) o g 
AB'C'A:Type. Id AA| Some definitions of interest. | |
| 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' | |
| tidentity | Def Id == Id |
| Thm* A:Type. Id AA |
About:
 |  |  |  |  |  |  |  |  |