A categorical construction of Bachmann–Howard fixed points

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 ϑ:TBH(T)→BH(T). Building on previous work, we show that Π11‐comprehension is equivalent to the assertion that BH(T) is well‐founded for any dilator T