A categorical construction of Bachmann–Howard fixed points

Abstract

Peter Aczel has given a categorical construction for fixed points of normal functors, that is, dilators which preserve initial segments. For a general dilator X TX , we cannot expect to obtain a well-founded fixed point, as the order type of TX may always exceed the order type of X. In the present paper, we show how to construct a Bachmann-Howard fixed point of T , that is, an order BH(T ) with an 'almost' order preserving collapse : T BH(T ) BH(T ). Building on previous work, we show that 1 1 -comprehension is equivalent to the assertion that BH(T ) is well-founded for any dilator T .