id (X:*) (x:X) : X = x

const (X:*) (Y:*) (x:X) (y:Y) : X = x

o
 (X:*) (Y:*) (Z:*)
 (f:Y -> Z)
 (g:X -> Y)
 : X -> Z
 = λ(x:X) -> f (g x)