Initial algebras from constructive ordinals

Benno van den Berg

Initial algebras from constructive ordinals

Logic 2026-07-28 v1

Authors: Benno van den Berg

Abstract

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 algebra theorems, like Adamek's theorem, and a version of Quillen's small object argument for constructing cofibrantly generated algebraic weak factorisation systems.

Cite

@article{arxiv.2607.25460,
  title  = {Initial algebras from constructive ordinals},
  author = {Benno van den Berg},
  journal= {arXiv preprint arXiv:2607.25460},
  year   = {2026}
}