Iteration and Primitive Recursion in Categorical Terms

Abstract

We study various well-known schemes for defining inductive
and co-inductive types from a categorical perspective. Categorically, an inductive
type is just an initial algebra and a coinductive type is just a terminal co-algebra.
However, in category theory these notions are quite strong, requiring the existence
of a certain map and its uniqueness. In a

formal system like type theory one usually only enforces the existence, because
uniqueness complicates the computational model. (Equality becomes undecidable.)
It is then more difficult to show the existence of maps defined by primitive
recursion, so one introduces separate notions e.g. primitive recursive types,
etc. The interdefinability of these various notions has been studied by various
authors.

It is well-known that also the categorical notions can be weakened, removing the uniqueness requirement. In the present paper we study various weakened versions of the notion of initial algebra (and its dual, terminal co-algebra), and we show in categorical terms how these notions relate to each other. In that sense, this paper can be seen as a categorical recast of type theoretic constructions of [4].

Full text