A,B,C:Type, f:(B
C), g:(AB). f o g 
ACa1,a2:A. f(a1) = f(a2) B 
a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Prop| 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 | |
| inject | Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2 |
| Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop |
About:
 |  |  |  |  |  |  |  |  |