1    λ(f : Type → Type → Type)
2  → { compose : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → f b c → f a b → f a c }