3 papers
math.LO2026
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…
cs.LO2026
Constructing (Co)inductive Types via Large Sizes
Bastiaan Laarakker, Daniël Otten, Benno van den Berg
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof ass…
math.CT2025
A constructive approach to the double-categorical small object argument
Benno van den Berg, John Bourke, Paul Seip
Bourke and Garner described how to cofibrantly generate algebraic weak factorisation systems by a small double category of morphisms. However they did not give an explicit construc…