arXiv subjects

S. C. Steenkamp

Publications and source records attributed to S. C. Steenkamp.

3 recordsLinked to original sources

arXiv2022

Constructing Initial Algebras Using Inflationary Iteration

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 topos.

math.LO↗

arXiv2022

Quotients, inductive types, and quotient inductive types

This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.

cs.LO↗

arXiv2020

Constructing Infinitary Quotient-Inductive Types

This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel's size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.

cs.LO↗