Transfinite iteration of functors as an extensional reflection
Infinite or transfinite iteration of functors is the principal way in which mainstream mathematics goes outside the logic of an elementary topos. It can be encoded using von Neumann’s class recursion theorem, but in 100 years the set theorists have failed to explain the two main components of this to the wider community. One is Replacement and the other is using impredicative higher order logic to derive recursion from induction.
Category theory is a mature and powerful discipline that should be able to do this in its native language, adopting the ideas without the dogma of other subjects. My proposal is to use extensional reflection of well founded coalgebras, in which “extensionality” is defined using a general factorisation system. This was shown to be consistent with ZF in a recent ItaCa lecture.
As a new axiom this is intended as an addition to those for an elementary topos, or maybe other foundational systems, but also as a new tool in our toolbox. One application is to recover ZF, which first requires the von Neumann hierarchy, i.e. the transfinite iteration of the covariant powerset, but full recovery involves other issues about ZF that distract from the category theory.
Thirty years after renouncing excluded middle and working on ordinals in category theory, I am not going to revert to the classical ones. However, the various constructive ones are not nicely behaved, for example it is not clear what diagram shapes are required to form colimits over them.
Extensional well founded coalgebras for general functors come to the rescue here, because they form (class) preorders rather than categories and behave very like sets under inclusion. Also the iterates of a functor are extensional and well founded, so transfinite colimits behave like set-theoretic unions.
Pullbacks give the -maps of a factorisation system in any arrow category. Applied to (op)fibrations they can express equations. Thus transfinite iteration of functors may be obtained as an extensional reflection in a category of opfibrations of (small) posets.
The papers and lecture slides are at
including a new historical study of Old and new proofs of the order-theoretic fixed point theorem.