2 papers
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…