1  
2    λ(t : Type → Type)
3  → { fold :
4        ∀(a : Type) → ∀(ts : t a) → ∀(b : Type) → ∀(f : a → b → b) → ∀(z : b) → b
5    }