Initial algebras from constructive ordinals

Benno van den Berg

We show how a standard constructive notion of ordinal supports a useful constructive theory of transfinite recursion. We do this by giving constructive proofs of various initial al…