Well founded coalgebras and their applications

This is part of my work on Induction, recursion, replacement and the ordinals that was begun in the 1990s.

A coalgebra α:A → T A for a functor T:C→C is well founded if, for every mono i:U ↪ A such that the pullback H factors through U in the diagram on the left, the map i must be an isomorphism.

Under conditions that are discussed in the papers below, any well founded coalgebra satisfies the recursion scheme that, for any algebra θ:T θ→Θ, there is a unique map f:A→Θ making the square on the right commute.

Well founded coalgebras and recursion

2019–25 paper currently with a journal referee (PDF).

Sections 2 and 8 have been re-written repeatedly since the November 2022 version.

We define well founded coalgebras and prove the recursion theorem for them: that there is a unique coalgebra-to-algebra homomorphism to any algebra for the same functor. The functor must preserve monos, whereas earlier work also required it to preserve their pullbacks. The argument is based on von Neumann’s recursion theorem for ordinals. Extensional well founded coalgebras are seen as initial segments of the free algebra, even when that does not exist.

The assumptions about the underlying category, originally sets, are examined thoroughly, with a view to ambitious generalisation. In particular, the “monos” used for predicates and extensionality are replaced by a factorisation system. Future work will obtain much more powerful results by using this in a categorical form of Mostowski’s theorem that imposes extensionality.

These proofs exploit Pataraia’s fixed point theorem for dcpos, which Section 2 advocates (independently of the rest of the paper) for much wider deployment as a much prettier (as well as constructive) replacement for the use of the ordinals, the Bourbaki–Witt theorem and Zorn’s Lemma.

Ordinals as Coalgebras

Draft PDF

Slides, 27 June 2024, Category Theory 2024, Santiago de Compostela.

Slides, 23 August 2023, Symposium in honour of Andy Pitts, Cambridge.

This works out the theory from Well Founded Coalgebras and Recursion in the category of posets using both general subsets with the restricted order and lower subsets as the class of “monos”.

This yields the “thin” and “plump” ordinals from Intuitionistic Sets and Ordinals and also another system that we call “slim”, although this is much less well behaved.

The first few plump ordinals are calculated in the topos of presheaves on a single arrow over classical sets, showing that this requires Replacement for ω· 2.

Seminar slides for Ordinals as Coalgebras, Symposium in honour of Andy Pitts, Cambridge, 23 August 2023.

This document was translated from L^AT_EX by H^EV^EA.