λ(t : Type) →
λ(base : Type → Type) →
  { cata : ∀(a : Type) → ∀(algebra : base a → a) → ∀(fixed : t) → a }