λ(f : Type → Type) →
    { ana =
        λ(a : Type) →
        λ(coalg : a → f a) →
        λ(s : a) →
        λ(r : Type) →
        λ(fn : ∀(b : Type) → { coalgebra : b → f b, seed : b } → r) →
          fn a { coalgebra = coalg, seed = s }
    }
  : ../Corecursive/Type (./Type f) f