Repository logo
 

Constructing Initial Algebras Using Inflationary Iteration

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Steenkamp, Shaun 

Abstract

An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using “inflationary” iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor’s constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of elementary topos.

Description

Keywords

Journal Title

Electronic Proceedings in Theoretical Computer Science

Conference Name

4th International Conference on Applied Category Theory

Journal ISSN

2075-2180

Volume Title

Publisher

Open Publishing Association
Sponsorship
EPSRC (2119809)
UK EPSRC PhD studentship 2119809
Relationships
Is supplemented by:
Is source of: