Towards a Unified Treatment of Induction, I: The General Recursion Theorem

Paul Taylor

1995–6

Abstract

The recursive construction of a function f : A → Θ consists, paradigmatically, of finding a functor T and maps α : A → T A and θ : T Θ → Θ such that f = α; T f ; θ. The role of the functor T is to marshall the recursive sub-arguments, and apply the function f to them in parallel. This equation is called partial correctness of the recursive program, because we have also to show that it terminates, i.e. that the recursion (coded by α) is well founded. This may be done by finding another map g : A → N, called a loop variant, where N is some standard well founded srtucture such as the natural numbers or ordinals. In set theory the functor T is the covariant powerset; in the study of the free algebra for a free theory Ω (such as in proof theory) it is the polynomial Σ_{r∈Ω}(−)^{ar(r)}, and it is often something very crude.

We identify the properties of the category of sets needed to prove the general recursion theorem, that these data suffice to define f uniquely. For any pullback-preserving functor T, a structure similar to the von Neumann hierarchy is developed which analyses the free T - algebra if it exists, or deputises for it otherwise. There is considerable latitude in the choice of ambient category, the functor T and the class of predicates admissible in the induction scheme. Free algebras, set theory, the familiar ordinals and novel forms of them which have arisen in theoretical computer science are treated in a uniform fashion.

The central idea in the paper is a categorical definition of well founded coalgebra α : A ▷ T A, namely that any pullback diagram of the form

\begin{aligned}T U & ^{⊂} T i > & T A \\ H & ∧ & ^{⊂} > & U & ^{⊂} i > & A & ^{∧α} \end{aligned}

is degenerate, i.e. U ≅ A.

This paper was available on my web page from 1996 to 2003. The work was presented at

• Category Theory 1995, Cambridge (UK), 7 August 1995;

• Logical Foundations of Mathematics, Computer Science and Physics — Kurt Gödel’s Legacy (Gödel ’96), Brno (CZ), 28 August 1996.

Summaries of the results were published in Sections 2.5, 6.3, 6.7 and 9.5 of my book [Tay99] and in an Extended Abstract that was circulated at the Brno meeting and elsewhere, and also available on my web page.

1 Introduction

The finite ordinals and (though not necessarily by this name) the term algebra for a finitary free theory have been familiar throughout the history of mathematics.

The geometrical form of Euclid’s algorithm was perhaps the first statement of induction: an infinite sequence of numbers is found, each less than the one before, which, as Elements VII 31 says quite clearly, is impossible amongst whole numbers [[check Euclid]]. Jakob Bernoulli (1686) stated an inductive principle in terms of the base case and the induction step in order to verify formulae for ∑_{r=1}^{n} r^{k} etc. Newton, Pascal and Wallis studied similar iterative problems and may have been aware of the logical principle. However Pierre de Fermat had been the first to make non-trivial use of the method of infinite descent to obtain positive results in number theory (1659). Gottlob Frege used his Begriffschrift (1879) to study iterative processes, introducing second order logic, and Bernoulli’s induction principle became the definition of the natural numbers in the work of Richard Dedekind (1888) and Giuseppe Peano (1889).

However it is a commonplace in proof theory that infinitary operations also admit induction and recursion (at least, as long as there are no laws), and Cantor showed how to define transfinite ordinals (1883). Indeed more careful consideration shows that notions of induction are needed to capture finiteness and not vice versa.

In order to study the essence of induction, infinitary term algebras and the ordinals, a naïve metalanguage is therefore inadequate to measure arities. In the symbolic tradition, a set theory with the axiom of choice has been used. However set theory is itself a term algebra, a kind of ordinal, and admits ∈-induction. The Zermelo-Fraenkel axioms, regarded either as a first or second order system, describe a relation called ∈ between entities from a universe which must already have some of the properties we’re trying to axiomatise. Whether the logical circularity about which Poincaré and Gödel warned us is a real threat we do not know, but the conceptual circularity is the subject of this paper.

Set theory as Zermelo formulated it in 1908 dealt with the “algebraic” operations forming new sets from old by powerset, comprehension, etc. Only later did Mirimanoff, Skolem, Zermelo himself and von Neumann consider the rank of a set, the process of recursion used to build it and the solution of the Russell and Burali-Forti paradoxes.

The notion of well-foundedness was originally restricted to ordinals, which are said to be well ordered. According to Cantor’s definition, every non-empty subset has a least element. Progress was hindered by the traditional requirement that order relations be total (or, better, trichotomous: ∀x, y. x < y ∨ x = y ∨ x > y); this was dropped by Montague, replacing least by minimal. However working with this formulation forever relies on excluded middle: what the examples (such as the natural numbers) satisfy is the induction scheme, and this is what is used to prove the theorems.

The break-through in the algebraic structure of sets was made not by set theorists but by analysis of the increasingly complicated algebraic tools employed by topologists and geometers. The exactness properties (relating images, kernels and their duals) of vector spaces were identified in the 1950s, using diagrams [[book]], and then formulated for sets in the 1960s by Giraud, Lawvere and Tierney. Lawvere’s ambition was “to do set theory without elements” and in particular we learnt from him that the quantifiers are the left and right adjoints to substitution. On the basis of Lawvere’s inspiration, Martin-Löf returned to the symbolic tradition and modern type theory was set out in a style originally used by Gentzen. We now have a very thorough understanding of type theory and the relationship between its symbolic and diagrammatic forms.

The inductive properties of sets are more difficult to axiomatise than the algebraic ones. They are needed to construct free algebras, which are the basis of syntax. In writing the chapter on induction in my book Practical Foundations I felt embarrassed how old fashioned the material was in comparison to that on type theory. At the very least, I needed the general recursion theorem for free theories instead of ordinals. Well founded relations reek of set theory. One reason for the difficulty was that the traditional theory of the ordinals depends very heavily on classical logic. Only very recently was this constraint removed, by Joyal and Moerdijk and by myself, to reveal not a single intuitionistic system of ordinals, but a complex family of systems.

The first remark the diagrammatic tradition had to offer about a term algebra was that it is the initial object in the category of all algebras. The very general nature of universal properties — the fact that this mode of description applies to so many other mathematical phenomena, including the quantifiers — means that we no longer have a “hands on” appreciation of the parsing and induction properties of the term algebra. These two features (which, in fact, characterise term algebras) drive the unification algorithm used in logic programming.

In theoretical computer science, idioms of induction have also arisen which cannot be expressed straightforwardly as instances of well founded relations. The fixed point theorem which Tarski proved is demonstrated using closure conditions, whilst the form popular in denotational semantics has been adapted to an idiom known as Scott induction, by specialising to predicates which are ā priori closed under directed joins. My own work on The fixed point property in synthetic domain theory employed a corresponding notion of “finite ordinals” which, unlike Cantor’s, stop at ω, and domains of this kind have been generalised by Crole and Pitts to “FIX objects” in more complicated inductive structures.

In the symbolic tradition, the initiality property (known as recursion) is derived from the induction condition characterising the term algebra, by means of the general recursion theorem, which was originally stated for ordinals. The proof is by pasting together “attempts” (partial solutions). After packaging the data for the free algebraic theory or notion of ordinal under consideration as a functor, we give a categorical proof of this theorem. This is based on a new definition of well founded coalgebra. The style of argument was first used by Osius, although unfortunately this work was not followed up at the time.

With the exception of Osius’ work, categorists seem invariably to have presupposed the existence of the initial algebra. In theoretical computer science, Jo Goguen, J.W. Thatcher, Eric Wagner and J.B. Wright in particular have rightly emphasised adjunctions in the algebraic methodology of programming (and are known as the ADJ group) [[write to them]]. But this is at the cost of the important parsing properties mentioned above.

Here, and also for finitary algebraic theories, the functor T preserves filtered colimits, and iteration over ℕ gives the initial algebra. For infinitary theories, transfinite iteration is needed, raising the question of when to stop. The traditional notion of the “rank” of a functor, which is needed to answer this question, depends on a (hitherto classical) theory of cardinals and ordinals, and so is not available to us. However the general recursion theorem was formulated for the theory based on the covariant powerset functor, which has no rank. The von Neumann hierarchy deputises for the missing initial algebra, and this is what we construct for general functors in this paper. In set theory it collects the admissible (set) approximations to the proper class algebra, and in arithmetic the finite approximations to the infinite algebra of natural numbers. In the approximations, the algebraic operations are not everywhere defined: they may over-flow.

By varying the underlying category we are then able to treat two branches of the intuitionistic multifurcation of the ordinals discovered by Joyal and Moerdijk, and my finite ordinals with a stationary point at ω, in the same framework as the set theory and free algebras resident in the category of sets and functions.

Ordinals, unlike free algebras, support successor, predecessor, union and other arithmetic operations. In fact it was these, rather than the well founded relation, which underlay the work of Joyal and Moerdijk. This extra structure is attributable to the fact that the functor which encodes the notion of ordinal is part of a monad. Although general algebras for the functor need not satisfy the additional laws required of algebras for the monad, on the initial algebra for the functor we may define a new structure which does. Indeed it is the initial such algebra equipped with an endofunction (obeying no more laws). In this way we obtain a notion of ordinal for any monad.

The diagrammatic version of the general recursion theorem identifies just how much of the logic of sets à la Lawvere is needed.

2 Free algebraic theories

In this section and the next we collect some basic symbolic ideas about algebra and set theory and express them in diagrammatic form. Both the notions of algebra and coalgebra for a functor arise, together with their homomorphisms; this seems incongruous at first, but we shall make sense of it in Section 5.

In order to define the structure of an algebra for theory with one sort, two constant-symbols 0 and 1, a unary operation-symbol − and two binary operation-symbols + and ×, we have to provide a set A together with “multiplication tables”

0_{A} : 1 → A 1_{A} : 1 → A −_{A} : A → A +_{A} : A × A → A ×_{A} : A × A → A.

(Be careful not to confuse the cartesian or categorical product A × A with the name of the symbol which might be used for arithmetical multiplication, or the singleton 1 = {⋆} with the name of a constant. We shall also use + for coproduct or disjoint union.)

If this were arithmetic we would then impose laws such as commutativity, associativity and distributivity, but we shall not consider these as we are interested in free (law-less) theories and their free algebras. Such algebras are sometimes called absolutely free. Besides raw formulae, free theories also describe trees, formal proofs and programs. We do not need to consider free algebras with generators, because these may be treated as additional constants (operation-symbols with arity zero) of the theory.

These five operations may be summed up as one using disjoint union (+):

[0_{A}, 1_{A}, −_{A}, +_{A}, ×_{A}] : 1 + 1 + A + A × A + A × A → A

i.e.

∑_{r∈Ω} A^{ar(r)} → A

where Ω = {0, 1, −, +, ×} is the set of operation-symbols and ar(r) is the arity of the operationsymbol r, in these cases 0, 0, 1, 2, 2 respectively.

In order to extract the individual operations from this amalgam, the sum must be stable and disjoint [BW85, Joh77]. This is one of the exactness conditions of the category of sets and functions, first identified (for sheaves) by Jean Giraud; for a slicker re-formulation, under the name of extensive category, see [CLW93, Tay99]. In fact the individual algebraic operations are of no further interest to us, so we do not make extensivity an Assumption (but see 6).

Interpreting A^{ar(r)} as the set of functions ar(r) → A instead of an ar(r)-fold product, the arity of each operation-symbol need not be a number, but can be an arbitrary set. Indeed the set Ω of operation-symbols need not be enumerated either: the arity-assignment is then itself a function defined on Ω and taking a set as its value at each point.

Thus a (possibly infinitary) free algebraic theory can be expressed by the functor

T = ∑_{r∈Ω} (−)^{ar(r)}

and the data for an algebra are encoded as an arbitrary function α : T A → A.

In this formulation, the assumption that there are no laws in the theory may be relaxed to some extent. For example, a commutative binary operation may be expressed by a function whose input is not an ordered pair (a, b) ∈ A^{2} but an unordered pair. We write, suggestively, A^{2}/2! for the set of unordered pairs, where / indicates not numerical division but the set of orbits in A^{2} of the action of the permutation group, so 3^{2}/2! has six elements. Further modifications of the functor, which we leave the reader to describe, may be used to express idempotence in the sense r_{3}(a, a, b) = r_{2}(a, b). These are the algebraic properties of the (finitary) set-forming operation {−, −, ⋯, −}. When programming data-structures, the notions of bag and list are at least as useful as set; algebraically, these are obtained by dropping the idempotence and commutativity requirements. The restriction to finite sets may be weakened: Joyal and Moerdijk [JM95] have provided categorical technology for handling subsets of specifically restricted size.

If (and only if) the function α : T A ↪ A is injective, we can say whether two values in A arose as expressions with the same outermost operation-symbol and sub-arguments. Of course in arithmetic we cannot distinguish between 5×2 and 7+3, but term algebras do have this property. In general we shall call the algebra α : T A ↪ A equationally free if α is mono. Notice that algebras for theories with laws can never be equationally free: indeed this property says that no non-trivial individual instances of equations ever hold (the commutative and idempotent laws give rise to weaker but more complicated notions of equational freedom which we leave the reader to formulate).

In the case where α is a bijection, every value in A arises in a unique way as an expression, i.e. as a particular constant or as a particular operation applied to particular arguments. Recognising it as such is called parsing. Of course, the arguments themselves can be parsed, and so on. We shall characterise the term algebra by the property that parsing is possible, but eventually terminates (at constant-symbols).

A function f : A → B between algebras is a homomorphism if the law

f(r_{A}(a_{→})) = r_{B}(f(a_{→}))

holds for each operation-symbol r and tuple a_{→} ∈ A^{ar(r)} of values. This means that the square on the left commutes for each r ∈ Ω:

a_{→} ∈ A^{ar(r)} \overline{\begin{matrix}f^{ar(r)} \\ > \end{matrix}} B^{ar(r)}  T A = ∑_{r∈Ω} A^{ar(r)} \overline{\begin{matrix}T f \\ > \end{matrix}} ∑_{r∈Ω} B^{ar(r)} = T B

A \begin{aligned}r_{A} \\ & ∨ \end{aligned}  \overline{f >} B \begin{matrix}r_{B} \\ ∨ \end{matrix}  A \begin{matrix}α \\ ∨ \end{matrix}  \overline{f >} B \begin{matrix}β \\ ∨ \end{matrix}

Putting the operation-symbols together, the condition is expressed by commutation of the righthand square, which makes use of the covariant action of the functor T on morphisms.

If B is an equationally free algebra (and the sum over the set of operation-symbols is disjoint) then we can only have

f(r(a_{→})) = f(s(a_{→}′))

if r and s are the same operation-symbol and f(a_{i}) = f(a′_{i}) for each of its arguments. The search for such an f : A → B identifying given pairs of terms in A in some term- (and therefore equationally free) algebra B to be found is called unification and is part of the computation engine of a logic programming language. We see here how the basic step arises — deducing a_{→} = a_{→}′ from r(a_{→}) = r(a_{→}′), which is plainly not valid in arithmetic — together with the clash error, if we try to identify terms with different outermost operation-symbols (r ≠ s). The other type of failure, x = r(x), for which the occurs check is made, is related to the well-foundedness of parsing in the target structure B. See [Tay99] for a more detailed treatment.

These ideas no longer rely on the logic of sets and can be formulated for any category:

Definition 2.1 Let S be any category and T : S → S an endofunctor. Then a T -algebra is an object A ∈ obS together with a morphism α : T A → A in S. It is called equationally free if α is a mono, and parsable if α is an isomorphism. A S-morphism f : A → B is a homomorphism of T -algebras if the square above commutes, i.e. T f ; β = α; f.

Lemma 2.2 If (as we shall later assume) T preserves monos, then any subalgebra of an equationally free algebra is equationally free. Proof

\begin{aligned}T A & ^{⊂} T f> & T B \\ A & \begin{matrix}α \\ ∨ \end{matrix} & ^{⊂} f > & B & ^{\begin{matrix}β \\ ∨ \end{matrix} ∩} \end{aligned}

By the cancellation property of monos, α : T A ↪ A. □

Definition 2.3 The algebra α : T A → A is called initial if for every algebra θ : T Θ → Θ there is a unique homomorphism f : A → Θ. In particular, Bill Lawvere [[ref]] characterised the natural numbers as the initial algebra for the Peano theory (with one constant and one unary operation). Thinking of A as the set of syntactic terms, the unique homomorphism is defined by structural recursion, and interprets the syntax using the semantic operations of Θ. We shall spell this out in Definition 3.6. This idiom is central to giving the definition of models of type theory. As for all universal properties, it is easy to show that the initial algebra, if it exists, is unique up to unique isomorphism.

Proposition 2.4 (Lambek) The initial algebra α : T A → A is parsable. Proof First observe that T α : T^{2}A → T A is a T -algebra and α : T A → A a homomorphism. But since A is initial, there is a unique homomorphism f : A → T A.

\begin{aligned}T A & <\underline{T α} ; ...... T f ..... > & T^{2}A \\ A & \begin{matrix}α \\ ∨ \end{matrix} & < \underline{α} ; ........f...... > & T A & \begin{matrix}T α \\ ∨ \end{matrix} \end{aligned}

Then f ; α : A → A is an endomorphism of the initial algebra, so by uniqueness f ; α = id. But as f is a homomorphism, α; f = T f ; T α = id, so f = α^{−1} [Lam68, Lam70]. □

Parsability is not sufficient to characterise the initial algebra: somehow we have to capture termination as well-foundedness or induction. In the case of the natural numbers, the first two of Giuseppe Peano’s five axioms say that they form an algebra (with one constant and one unary operation), and the next two that this is equationally free. However ℕ + ℤ is also a parsable algebra, but fails the last axiom: the induction scheme. We can state this as follows:

Proposition 2.5 (Lehman,Smyth) The initial algebra has no proper subalgebra.

\begin{aligned}T A & < T i ^{⊃} ; ...... T f ...... > & T U \\ A & \begin{matrix}α \\ ∨ \end{matrix} & < i ^{⊃} ; ........f........ > & U & ∨ \end{aligned}

Proof By a similar argument, f ; i = id_{A}, but i is mono, so U ≅ A [LS81, §5.2]. □

We shall show in Section 9 that a minimal parsable algebra is initial.

Remark 2.6 The categorical description is not particularly helpful in showing that free algebras exist. Since the forgetful functor which extracts the carrier A from an algebra α : T A → A preserves arbitrary limits, some version of the adjoint functor theorem ought to provide free algebras. But the covariant powerset functor P (Definition 3.1) shows that some restriction must be put on T.

One such hypothesis is the solution-set condition of the general adjoint functor theorem [Mac71, §6.6]. In this case we would need to find an admissible set G of algebras such that for any algebra Θ there is some homomorphism A → Θ with A ∈ G. The general adjoint functor theorem is silent on the subject of how to find such a set G of algebras.

The traditional way a categorist might look for the free T -algebra is by iteration. Starting with the unique map e : Z → T Z, where Z is the initial object (such as ∅), we form the sequence

Z ^{e}> T Z ^{T e}> T^{2}Z ^{T^{2}e}> T^{3}Z > ⋯ > colim_{n∈ℕ} T^{n}Z

and its colimit. If T preserves this colimit then it gives the free algebra. Otherwise, we must iterate transfinitely, but this begs several questions:

• We must go outside the diagrammatic idiom to use a set-theoretic and until recently classical theory of ordinals.

• We do not know a priori when to stop iterating. The functor is said to have rank if there is some ordinal κ at which T^{κ}Z is a fixed point; in particular, for a free theory, κ = sup {ar(r) : r ∈ Ω}. On the other hand, the covariant powerset functor (Definition 3.1) does not have rank, and the corresponding process gives the von Neumann hierarchy. When the category is a small ipo, i.e. a poset with least element and arbitrary directed joins, one might expect this process to converge; indeed it does, classically, but the intuitionistic question without additional hypothesis (Tarski’s theorem) remains open [Tay96, §9].

• The formation of infinite colimits involves the axiom of replacement [Tay96, 3.17ff].

The purpose of the present work is to turn these techniques in to respectable category theory. We aim to give an intrinsic description of the diagram, without ā priori indexing: the rank will be obtained from the diagram, and not vice versa.

What we shall use is the special adjoint functor theorem [Mac71, §6.8], which is a diagrammatic manifestation of second order logic. We may form the union or intersection of all subsets satisfying certain properties. In the situation at hand, if there is some equationally free algebra then there is a minimal one, given by the intersection of all subalgebras. In Assumption 1ff we shall similarly form unions. In this paper we do not have very much to add on the subject of the special adjoint functor theorem — we are interested in other aspects of the construction — but see [PS78], particularly Theorem 2.2.2, for an account of the existence of adjoints in terms of indexed category theory. [[Peter Johnstone on Giraud’s theorem.]]

To show that the term algebra exists, it only remains to prove the

Proposition 2.7 Any free theory has an equationally free algebra in Set (or in any topos with a natural numbers object).

Proof In the case of the theory of lists (with the empty list as constant and some “alphabet” X whose elements we treat as unary operation-symbols) the set (X + 1)^{ℕ} of streams provides an equationally free algebra.

For a general free theory with a set Ω of operation-symbols, let A = P(L), where L is the set of lists of the form

[r_{0}, j_{0}, r_{1}, j_{1}, …, r_{n−1}, j_{n−1}, r_{n}]

each r_{i} ∈ Ω being an operation-symbol, and j_{i} ∈ ar(r_{i}) a position in its arity. We write r :: j :: ℓ for the operation (cons) of appending two terms to the front (head) of the list ℓ.

For x_{→} ∈ A^{ar(r)}, define α(r, x_{→}) = {r} ∪ {r :: j :: t | j ∈ ar(r), t ∈ x_{j}}, making α : T A → A an

algebra.

Then r is characterised in this subset as the unique list of length 1 and

x_{j} = {t | r :: j :: t ∈ α(r, x_{→})},

so this algebra is equationally free. □

The idea of this construction is that the terms are (infinitely branching) trees, and are determined by the set of paths through them from the root. Imagine a term being processed by a program; at any moment it is at a certain point in the tree, with the path stored on its stack, i.e. as a list. Corresponding to the root there is an operation symbol, r_{0}, with a co-ordinate j_{0} ∈ ar(r_{0}); the next stage is a similar pair (r_{1}, j_{1}) with j_{1} ∈ ar(r_{1}) and so on. At the last stage (which is the top of the stack or the head of the list) we have only an operation-symbol r_{n} without any specified co-ordinate. Otherwise we would not be able to handle the nullary operations, without which the free algebra would be empty.

For finitary free theories there is an alternative construction, using Jan Łukasiewicz’s (“Polish”) notation, in which operation-symbols precede their lists of arguments. By keeping tally of the number of pending sub-arguments it is easy to identify which lists of these symbols are well formed terms in the free algebra. This notation, in “reversed” form, with the operation-symbols after their arguments, is used by compilers and some pocket calculators to evaluate arithmetic expressions stored on a stack.

3 The ∈ relation as a coalgebra

Here we shall recall some of the basic definitions of set theory and show how they can be expressed in terms of coalgebras for the powerset functor. The idea is that the von Neumann hierarchy is the free algebra. Of course, the hierarchy is a proper class, and this functor has no free algebra in the standard sense.

Many of these ideas are due to Gerhard Osius [Osi74], though unfortunately they were not followed up at the time. The reason for this is that set theory was intended by Zermelo as a type theory, and attention has normally been focused on this aspect. This was especially so in the 1970s, when Osius was writing, as the priority then was to show that toposes could do the same job (but better). Osius himself, who now studies statistics, seems not to have appreciated the value of his own work to induction rather than type theory. See also [Tay96] for an iconoclastic account of the interpretation of type theory in sets and vice versa. Familiarity with these two papers is not essential to follow the present work, but references to the analogous results in them will be given in order to trace the history of the argument.

Definition 3.1 The covariant powerset functor P : Set → Set is defined on a function f : A → B by

P(f)(U) = {f(a) : a ∈ U} = {b ∈ B : ∃a ∈ A. b = f(a) ∧ a ∈ U} ⊂ B

for U ⊂ A. We shall also need to define, for V ⊂ B,

f^{∗}V = {a ∈ A : f(a) ∈ V }
f_{∗}U = {b ∈ B : ∀a ∈ A. f(a) = b ⇒ a ∈ U}.

These also provide the morphism parts of functors Set → Set which are respectively contravariant and covariant, since (g ∘ f)^{∗}W = f^{∗}(g^{∗}W) and (g ∘ f)_{∗}U = g_{∗}(f_{∗}U), but these will not arise in this paper. What is of more interest is to consider the adjunctions

\begin{aligned}U & ^{⊂}  > & X & P(X) \\ V & ^{⊂}  > & Y & \begin{aligned}f \\ & ∨ \end{aligned} & P(Y) & ^{P(f)∧}⊣ \begin{matrix}f^{∗} \\ ∨ \end{matrix} ⊣ f_{∗} ∧ \end{aligned}

order-theoretically. Diagrammatically, P(f) and f^{∗} are given by composition and pullback respectively. Symbolically, P(f)(U) and f_{∗}U are defined by similar formulae, except that one involves an existential and the other a universal quantifier [Law69]. We shall take these up in section 7.

Definition 3.2 A coalgebra for an endofunctor T : S → S of any category is an object A ∈ obS together with a morphism α : A ▷ T A.

\begin{matrix}T A & \overline{T f ▷} & T B \\ A & ^{α△} & \overline{f ▷} & B & ^{△β} \end{matrix}

A homomorphism of coalgebras is a function f : A ▷ B making the square commute. We shall use the triangle arrowhead for maps which are coalgebra homomorphisms, although this fact will not always be proved in sitū. (Beware that this is not the same use of the triangle arrowhead as in [Tay99]. [[⊴ in [Tay96]]]) The structure map α : A ▷ T A is easily seen to be a homomorphism if we equip A and T A with the structures α and T α; this may perhaps overcome any confusion which may arise from considering both algebras and coalgebras, and using similar notational conventions for both. In later parts of the paper, most of the arrows will actually be coalgebra homomorphisms.

Remark 3.3 Any binary relation whatever is a P-coalgebra, and vice versa, where

x ≺ a ⟺ x ∈ α(a) α(a) = {x : x ≺ a}.

We write (≺) ⊂ A×A for the binary relation because we intend it to be well founded (and therefore irreflexive in this case), or in particular to be the set-theoretic membership relation, but we avoid the notation ∈ as a source of confusion. This relation need not be transitive in the order-theoretic sense.

The structure map α : A ↪ P(A) is mono iff the rule

{∀x ∈ A. x ≺ a ⟺ x ≺ b \atop a = b}

holds for all a, b ∈ A, in which case ≺ and α are said to be extensional.

In set theory a carrier A equipped with a well founded extensional relation is called a transitive set: transitive because the elements and elements of elements etc. of the elements are also needed in order to specify the structure fully. This should be thought of as a model of a fragment of set theory, specifically of the axioms of foundation and extensionality. Following [Tay96] we call such a structure an ensemble.

Transitivity in the usual order-theoretic sense provides the simplest notion of ordinal [Tay96, §4]. It is characterised diagrammatically by α; T α; μ ⊂ α, where μ : T^{2}A → T A is union.

Remark 3.4 Before characterising P-coalgebra homomorphisms, consider the situation where α; P(f) ⊂ f ; β.

P(A) \overline{\begin{matrix}P(f) \\ > \end{matrix}} P(B)
⊂
a ∈ A^{α△}  \overline{f >} B^{△β}

This inclusion holds iff

∀a, x ∈ A. x ≺_{A} a ⇒ f(x) ≺_{B} f(a)

i.e. f is “strictly monotone” — it preserves the binary relation.

The reverse inclusion says

∀a ∈ A. ∀y ∈ B. y ≺_{B} f(a) ⇒ ∃x ∈ A. y = f(x) ∧ x ≺_{A} a,

which is a “lifting” property similar to that defining a fibration:

\begin{matrix}∃x & ................ ≺_{A} > & a & A \\ y & ^{\begin{aligned}f \\ & ∨ \end{aligned}. . . . . . . . . . . . . .} & \overline{\begin{matrix}≺_{B} \\ > \end{matrix}} & f(a) & \begin{matrix}f \\ ∨ \end{matrix} & B & f_{▽} \end{matrix}

In process algebra a function f with this property is known as a simulation [Tay96, 2.3].

If f : A > ▷ B is mono then being a simulation says that A is down-closed, i.e. ∀a, b. b ≺ a ∈ A ⇒ b ∈ A. This is the case for the the inclusion of one transitive set as a subset of another (in the set-theoretic sense), so Osius gave the name inclusion to such maps [Osi74, §6].

Indeed if the two coalgebras are extensional and well founded, f is necessarily mono (Proposition 10.2), and embeds A as a ≺-lower subset of B. This gives a purely order-theoretic characterisation of the subset relation of set theory [Tay96, 2.9, §3].

Now we come to the central concept of this paper:

Definition 3.5 A coalgebra α : A ▷ T A is well founded if in any pullback diagram of the form

\begin{aligned}T B & ^{⊂}  T i  > & T A \\ H & ∧ & ^{⊂} j > & B & ^{⊂} i > & A & ^{△α} \end{aligned}

the maps i and j are necessarily isomorphisms.

Let us spell this out in detail in the case T = P. The property says that any subset B ⊂ A satisfying a certain premise (that it gives rise to a diagram of this form) is necessarily the whole of A. Writing B = {x ∈ A : ϕ[x]} for some predicate ϕ[x] defined on A, the induction scheme has this form. We just have to unscramble the premise.

An element (a, V) ∈ H ⊂ A × T B of the pullback consists of a ∈ A and V ⊂ B ⊂ A such that α(a) ≡ {x ∈ A : x ≺ a} = V. Thus V is determined uniquely by a (and the structure α : A → T A), but for such a V to exist, a must satisfy

{x ∈ A : x ≺ a} ⊂ B, i.e. ∀x ∈ A. x ≺ a ⇒ ϕ[x].

For every such a ∈ A, the premise is that a ∈ B, i.e. ϕ[a].

In the case T = P, α : A → T A is therefore a well founded coalgebra iff the rule

∀a. (∀x ∈ A. x ≺ a ⇒ ϕ[x]) ⇒ ϕ[a] ; ∀a. ϕ[a]

is valid. This is the usual induction scheme defining a well founded relation. The bracketed part, H = (∀x ∈ A. x ≺ a ⇒ ϕ[x]), is known as the induction hypothesis, and a “proof by induction” is the implication from this to B = ϕ[a]. We shall call this implication the induction premise. If it happens that it is two-way then we refer to the strict induction premise; this corresponds to being given j : H ≅ B in the Definition, i.e. to the situation of Proposition 2.5. [[It can be shown that the lax and strict induction schemes are equivalent.]]

A diagrammatic “proof by induction” consists in showing that H ⊂ B; the conclusion is then B = A. See Lemma 6.5, Proposition 6.7, Proposition 7.3, Theorem 8.4 and Proposition 10.2 for examples of this style of reasoning.

Osius did not consider induction but recursion [[pick up abstract]]:

Definition 3.6 A coalgebra α : A ▷ T A obeys the recursion scheme if, for every algebra θ : T Θ → Θ, there is a unique map f : A → Θ such that the square

\begin{matrix}T A & \overline{T f>} & T Θ \\ A & ^{α△} & \overline{f >} & Θ & \begin{matrix}θ \\ ∨ \end{matrix} \end{matrix}

commutes. In the case of the covariant powerset functor, this is the law

f(a) = θ({f(x) : x ≺ a}),

which describes a recursive procedure: given the argument a, use α to parse it as a set {x : x ≺ a} of sub-arguments, apply f (recursively) in parallel to these, and finally use θ to form the result f(a) from the sub-results f(x). In general, the functor T handles the “parallel” application of f, allowing for more complicated ways of marshalling the sub-arguments.

An ensemble for a free algebraic theory is a collection of terms which is closed under subarguments, but not necessarily under applying the operation-symbols. We may think of expressions lying outside the collection as having “overflowed.” In the case of the free algebra, the structure map of the coalgebra is the inverse of that of the algebra (Proposition 2.4): it is used to parse a term and feed its sub-terms to the recursive calls T f of the function.

Remark 3.7 As an example of the recursion law, Andrzej Mostowski showed in set-theoretic terms that every extensional well founded relation is isomorphic to the ∈-relation on a unique transitive set. This is defined recursively by

f(a) = {f(x) : x ≺ a}.

Dropping extensionality as a hypothesis in this result, we obtain the extensional quotient of any well founded relation, i.e. the universal way of imposing extensionality on a well founded relation.

Mostowski’s equation may be re-written as

y ∈ f(a) ⟺ ∃x. y = f(x) ∧ x ≺ a,

which says exactly that f is a simulation from the well founded relation to its extensional quotient. [Tay96, 2.11] gave a complicated recursive construction of the equivalence relation needed to perform this construction, without the axiom of replacement (which Mostowski’s result needs). We shall give a simpler construction in Proposition 7.10.

Remark 3.8 Consider the case where Θ = Ω = P(1), the set of truth values (subobject classifier), and the structure map θ = ⋀ is infinitary conjunction or universal quantification. Then

f[a] ⟺ (∀x. x ≺ a ⇒ f[x]),

which is the strict (⇔) version of the induction premise above. On the other hand, it is easy to see that the constant function f : a ↦ ⊤ satisfies the recursion property in this case, so uniqueness of f amounts to the induction scheme.

\begin{aligned}H & \overline{>} & T U & \overline{>} & T 1 & \overline{>} & 1 & \underline{<} & U \\ A & ^{∨ ∩} & \overline{▷} & T A & ^{\begin{matrix}T i \\ ∨ \end{matrix} ∩} & \overline{T f >} & T Ω & ^{\begin{matrix}T ⊤ \\ ∨ \end{matrix} ∩} & \overline{\begin{matrix}θ = χ_{T ⊤} \\ > \end{matrix}} & Ω & ^{\begin{matrix}⊤ \\ ∨ \end{matrix} ∩} & < f & A & ^{\begin{matrix}i \\ ∨ \end{matrix} ∩} \end{aligned}

This argument generalises. Let θ : T Ω → Ω be the characteristic function of the subset T ⊤ : T 1 ↪ T Ω, where ⊤ : 1 ↪ Ω is the element “true”. The induction premise is α; T f ; θ ⇒ f and the strict premise has equality (bi-implication), but this is also satisfied by the constant function with value ⊤.

The conclusion that well foundedness is necessary for a unique solution of the recursion equation should be treated with circumspection. Taking the object of truth values as the target algebra means that we are using higher order logic (this point is obscured classically by the identification of Ω with a discrete two-element set). Induction for the second order predicate ϕ[x] ≡ (x ⊀ x) shows that well founded relations in this sense are irreflexive, and therefore too clumsy to analyse fixed points of iteration. On the other hand, experience shows that we must count ourselves lucky to find a condition for termination of a heavily recursive program which is sufficient for the case at hand: asking for it to be necessary as well is too much.

Idiomatically, we have in mind a particular target structure Θ, and maybe we would like to do recursion in some category which is not a topos. By closer examination of the carrier and structure of the intended target, maybe we can restrict the class of subsets (predicates) which need to be considered, and thereby obtain a weaker notion of well-foundedness which admits more source structures A but remains sufficient to define recursion.

4 Examples

Example 4.1 Euclid’s algorithm. Let T : Set → Set by X ↦ X + ℕ. Put Θ = ℕ and let θ : T Θ = ℕ + ℕ → ℕ be the co-diagonal. Put A = ℕ × ℕ and define α : A ▷ T A = (ℕ × ℕ) + ℕ by

α(n, 0) = n  (in the second component)
α(n, m) = (m, n)  if 0 < m < n
α(n, m) = (n, m − n)  if 0 < n ≤ m

Then α is well founded because g : A → ℕ by (n, m) ↦ 2n + m is strictly monotone. Hence there is a unique solution of the recursion equation, which is the highest common factor. □

Definition 4.2 The situation where T X = X + Θ and θ : T Θ = Θ + Θ → Θ is the co-diagonal is called tail recursion. Without loss of generality Θ = A. Iteration of α : A → A until it’s fixed.

While coequalisers.

Other text book recursion examples, such as fold and quick sort.

Deal with using a sub-result as another sub-argument.

5 Partial algebras

In order to make the ideas of the last two sections fit together, we shall now generalise those of Section 2 by considering partial functions. We shall characterise the “initial segments” of the free algebra, i.e. collections of terms closed under sub-expressions. Section 8 shows how to build up all initial segments, and hence the free algebra. The ambient category will be called S, though you may think of it as sets and functions.

Definition 5.1 A partial map X ⇀ Y is a diagram of the form

\begin{matrix}U & \overline{f >} & Y \\ X & ^{\begin{matrix}i \\ ∨ \end{matrix} ∩} \end{matrix}

where i is injective (a mono) and is called the support. If i is an isomorphism then (i, f) is said to be a total map.

Proposition 5.2 Partial maps form an ordered category, which we call P, and each hom-poset P(X, Y) is an ipo (it has a least element ⊥ and directed joins ^{⋁↑}). Total maps are maximal (if (i, f) ⊑ (j, g) then (i, f) = (j, g)), though the converse need not hold.

• ............ > V  \overline{>} Z  U

U^{∨ \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}}  \overline{>} Y^{∨ ∩}  V \overline{g >}^{.......k....... >}  Y^{f  >}

X^{∨ ∩}  X^{\begin{matrix}j \\ ∨ \end{matrix} ∩}^{⊂  i  >}

Proof Partial maps compose by forming the pullback shown on the left. This composition is associative with identity X <^{id} ^{⊃} X ^{id} > X. We define (i, f) ⊑ (j, g) if there is a map k (necessarily a mono, cf. Lemma 6.2, and unique) such that i = k ; j and f = k ; g, as shown on the right. If (i, f) ⊑ (j, g) and (j, g) ⊑ (i, f) we shall treat them as equal. The least partial map X ⇀ Y has empty support; directed unions of supports, being colimits, provide directed joins of partial maps. □

A generalisation is possible wherein we no longer require supports to be mono, so partial maps become spans. These form a bicategory rather than an ordered category, although in fact this would not make the arguments of this paper significantly more complicated. The reason for restricting to monos is that we have some control over the number of monos into an object, i.e. its subsets (we say that the category is well powered, Assumption 1), but not over arbitrary incoming maps. [[Small complete category.]]

Assumption 5.3 Let T : S → S be an endofunctor which preserves monos and inverse image diagrams, i.e. pullbacks of the form:

\begin{aligned}U & \overline{>} & V \\ X & ^{∨ ∩} & \overline{>} & Y & ^{∨ ∩} \end{aligned}

[[Peter Freyd’s unique existentiation.]]

Notice that in the cases we considered in Sections 2 and 3, T actually preserves arbitrary intersections of monos, and cofiltered limits of arbitrary maps. In fact free algebraic theories and generalisations of them such as semilattices and complete semilattices may be characterised by such properties: see [Joy87, Tay89].

Proposition 5.4 T extends to an order-preserving endofunctor T : P → P on the ordered category of partial maps. □

Definition 5.5 Now we can replace T A → A by T A ⇀ A in the definition of a T -algebra. That is, a partial algebra is a diagram of the form

A \underline{<}  U ^{⊂} > T A.

In fact it is useful to generalise even further to a span A ← U → T A. From spans we restrict back to the special cases in which these two maps are monos or isomorphisms:

U ↪ T A  U ≅ T A
A ← U → T A  partial algebra  algebra

A ↩ U partial coalgebra equationally free partial algebra equationally free algebra

A ≅ U  coalgebra  extensional coalgebra parsable algebra
well founded coalgebra  T -ensemble  initial algebra

In this table, each of the twelve notions is the conjunction of those at the top and left. This is not difficult to see, except in the last two cases. We shall show in Proposition 5.8 that a minimal equationally free partial algebra, i.e. one with no proper subalgebra, is the same thing as a well founded extensional coalgebra. That well-foundedness and parsability imply initiality is one of our main goals.

Definition 5.6 Similarly a partial homomorphism is a map f : A ⇀ Θ such that the square on the left commutes in P:

T A \overline{\begin{matrix}T f \\ ⇀ \end{matrix}} T Θ  T A \overline{\begin{matrix}T f \\ ⇀ \end{matrix}} T Θ
⊑
A \begin{aligned}α \\ & ⇃ \end{aligned} \overline{f ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}  A \begin{aligned}α \\ & ⇃ \end{aligned} \overline{f ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}

This is simply a homomorphism of T -algebras in the category P. However we have no direct way of obtaining homomorphisms: there is at most one homomorphism from a T -ensemble to a partial algebra, and its existence is a principal result of this paper. It is therefore useful to replace this equality with the order relation on partial maps, as on the right. A partial map f : A ⇀ Θ such that α ; f ⊑ T f ; θ is called an attempt. The empty partial function is an attempt, and by applying the functor and forming unions we can generate more of them.

Several symbolic and diagrammatic technologies have been developed for handling partial functions, and in particular to deal with the fact that we may wish to write an expression without asserting ā priori that it denotes a value. Consider the law defining homomorphisms of algebras,

f(r_{A}(a_{→})) = r_{Θ}(f(a_{→})),

interpreted as a strict equation between possibly undefined terms. This says that if one side (together with all of its subformulae) is defined, so is the other (and its subterms), and then they are equal. For an attempt, we allow the right hand side to be defined and the left not, writing

f(r_{A}(a_{→})) ⊑ r_{Θ}(f(a_{→})).

Beware that this does not mean that the left hand side is in any sense arithmetically less than the right: if they are both defined then they are equal.

In this work partial maps are being used as a tool to define total ones, so we want to develop idioms for discussing total maps. In particular we have to explain how coalgebra homomorphisms and the recursion scheme (Definitions 3.2 and 3.6) arise.

The next result is a Pons Assinorum: it is not difficult in itself, but this rearrangement of diagrams is crucial to understanding the rest of the paper.

Remark 5.7 An attempt f : A ⇀ Θ is described by either of the following diagrams in S:

\begin{aligned}P & > & B & \overline{f >} & Θ \\ & 1 & 2 \\ Q & > & ^{............ >} & ^{i ∩} & V & θ > \\ U & ∨ & \overline{g} & \overline{>} & A & ∨ \\ 4 & & 3 \\ T B & ∨ & \overline{T f >} & T Θ & ^{\begin{matrix}j \\ ∨ \end{matrix} ∩} \\ T A & ^{\begin{matrix}α \\ ∨ \end{matrix} ∩} & <T i^{⊃} \end{aligned}  \begin{aligned}A & < g & U & ^{⊂} α > & T A \\ & 1 & & 4 \\ B & ^{i_{∪} ∧} & \underline{<} & P & ^{^{∪} ∧} & ^{⊂} > & T B & ^{T i_{∪} ∧} \\ & 2 & & 3 \\ Θ & \begin{aligned}f \\ & ∨ \end{aligned} & < θ & V & ∨ & ^{⊂} j > & T Θ & \begin{matrix}T f \\ ∨ \end{matrix} \end{aligned}

Similarly a partial homomorphism is given by the same diagram, but with P ≅ Q in the left-hand diagram, and square 3 in the right-hand diagram is a pullback. □

[[Partial homomorphism T A ⇀ A.]]

Just as we generalised T -algebras to spans and then restricted again, so we may replace the monos in these diagrams by general maps or by isomorphisms. The idioms of the previous two sections may be recovered by doing this in various ways.

The next result links Proposition 2.5 (minimal equationally free algebras) to Definition 3.5 (well-foundedness). This explains our interest in coalgebras, even though we aim to find the free algebra. Coalgebra homomorphisms are also very important, and in particular coalgebra monomorphisms A > ▷ B between ensembles are called initial segments.

Proposition 5.8 A minimal equationally free partial algebra (mefpa) is the same thing as an extensional well founded coalgebra. We shall call such a structure a T -ensemble.

Proof First we show that every mefpa A <^{i} ^{⊃} U ^{⊂} ^{α}> T A is a coalgebra, i.e. i : U ≅ A.

U < ................ j V .............. β > T U
2  3
A^{\begin{matrix}i \\ ∨ \end{matrix} ∩} < ^{i ^{⊃}} U^{\begin{aligned}j \\ & ∨ \end{aligned}. . . . . . . . . . . . .} ^{⊂} α > T A^{\begin{matrix}T i \\ ∨ \end{matrix} ∩}

Form the pullback as shown on the right; the left-hand square commutes, trivially. But this describes a subalgebra, i.e. a total homomorphism i : U ↪ A, so i : U ≅ A by minimality.

T U ^{⊂}  T i  > T A  U \underline{<}  H ^{⊂} > T U
2  3
H^{^{∪} ∧} ^{⊂} j > U ^{⊂} i > A^{\begin{matrix}α \\ ∧ \end{matrix} △}  A^{\begin{matrix}i \\ ∨ \end{matrix} ∩} = = = = = = = A^{∨ ∩} > α ▷ T A^{\begin{matrix}T i \\ ∨ \end{matrix} ∩}

Now let α : A > ▷ T A be an extensional coalgebra. The diagram on the left testing wellfoundedness of A may be re-arranged into that on the right for a partial subalgebra, i : U ↪ A. Hence A is well founded quâ coalgebra iff it is minimal quâ equationally free partial algebra. □

In future we shall only be interested in partial attempts whose sources are well founded coalgebras, so i : U ≅ A and square 1 degenerates.

Remark 5.9 Reverting to diagrams of partial maps, consider the (lax) recursion scheme, Definition 3.6:

T A \overline{\begin{matrix}T f \\ ⇀ \end{matrix}} T Θ

⊔∣

A^{α△}  \overline{f ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}

Again drawing out this diagram in full in terms of total maps,

P = B  \overline{f}

2

R  \overline{>}^{.......................... >}  Q  \overline{>} V  \overline{_{θ >}} Θ ∨

3

S^{∨ ∩}  \overline{>} T B^{∨ ∩}  \overline{T f>} T Θ^{\begin{matrix}j \\ ∨ \end{matrix} ∩}

4

i ∩  \overline{▷} A = U^{∨ ∩}  \overline{α ▷} T A^{T i_{▽} ∨}

we obtain the diagram on the right in Remark 5.7, reduced to the case where the source of the partial attempt is a coalgebra:

A = = = = = = = A \overline{α ▷} T A
1  4
B^{\begin{matrix}i \\ ∧ \end{matrix} △} = = = = = = = B^{∧ △}  \overline{β ▷} T B^{\begin{matrix}T i \\ ∧ \end{matrix} △}
2  3
Θ \begin{aligned}f \\ & ∨ \end{aligned} < θ V ∨ ^{⊂} j > T Θ \begin{matrix}T f \\ ∨ \end{matrix}

The lax recursion scheme for A ⇀ Θ is therefore the same as a partial attempt A ⇀ Θ, which is a total attempt B → Θ on an initial segment B > ▷ A. □

Remark 5.10 However the strict recursion scheme (with equality for ⊔∣), where the mediator P ≅ R is an isomorphism, corresponds to the condition that P be the limit of the subdiagram consisting of A ▷ T A ◁ < T B → T Θ ↩ V.

In other words the strict recursion scheme does not characterise partial homomorphisms, but

• if A is extensional (α mono) and f is a homomorphism then f = α; T f ; θ, and

• if A is a parsable algebra (α iso) and f = α; T f ; θ then f is a homomorphism,

since f is a homomorphism iff P ≅ Q in Remark 5.7, and these conditions then make R ≅ Q.. For counterexamples consider two-element Peano coalgebras. □

Lemma 5.11 Let f : A ⇀ Θ be a partial attempt from a well founded coalgebra to a total algebra, such that f = α; T f ; θ. Then f is a total map.

Proof We have g : U ≅ A and j : V ≅ T Θ.

A = U \overline{α ▷} T A

4

B = P^{\begin{matrix}i \\ ∧ \end{matrix} △}  \overline{β ▷} T B^{\begin{matrix}T i \\ ∧ \end{matrix} △}

2/3

Θ \begin{aligned}f \\ & ∨ \end{aligned} < θ V = T Θ \begin{matrix}T f \\ ∨ \end{matrix}

The limit diagram reduces to saying that square 4 is a pullback, so by well-foundedness of A this is degenerate, i.e. i : B ≅ A. □

Remark 5.12 Consider instead the case where Θ is also a coalgebra, so θ : V ≅ Θ and both squares 1 and 2 degenerate. Then a partial attempt is a span A ◁ < B ▷ Θ of coalgebra homomorphisms.

Recall that square 3 is a pullback in the case of a partial homomorphism. This too degenerates if Θ is well founded, so any partial homomorphism of partial algebras A ⇀ Θ is simply a coalgebra homomorphism A ◁ < Θ (sic). Any total homomorphism of partial algebras A → Θ is an isomorphism, since the last square 4 is then also trivial, and we shall also see in the next section that ensembles have no non-trivial automorphisms. □

6 Local completeness assumptions

There is, at least classically, no ambiguity about what might constitute a “subset” of a set on which a partial map might be defined (and it will do no harm to ignore this section and think of M throughout as inclusions of subsets). However we observed in Remark 3.8 that well founded relations in the traditional sense are irreflexive, and that to tune them more finely to applications we need to restrict the class of subsets or predicates to which the induction scheme applies. For posets, topological spaces and other categories there are perhaps several notions of “subspace” which might be candidates for this role. We shall therefore be explicit about what properties we require of the notion of subset.

Definition 6.1 A class of supports (or dominion) M in a category S is a class M ⊂ morS (whose arrows we write ^{⊂} > ) such that

1. all M-maps are monos in S, i.e. if m ∈ M and f ; m = g ; m (• ⇉ • ↪ •) then f = g;

2. all isomorphisms (and in particular all identities) from S are in M;

3. M is closed under composition (so it is a wide or lluf subcategory);

4. such that the pullback f^{∗}m of any M-map m against any S map f exists and is in M.

\begin{matrix}• & ................. > & V \\ X & ^{\begin{matrix}f^{∗}m \\ ∨ \end{matrix} \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}} & \overline{f >} & Y & ^{\begin{matrix}m \\ ∨ \end{matrix} ∩} \end{matrix}

Wherever we talk about “monos” or “subsets” in this paper we mean M-maps. In particular the discussion of partial maps in the previous section remains valid when we put M for monos. If the subsets are defined by predicates, then choosing a class of supports corresponds to restricting the predicates to a certain fragment of logic. In order to provide a notion of well foundedness sufficient to solve the recursion scheme in as many cases as possible, we want to make the class M as small as we can.

Lemma 6.2 Whenever m and f ; m are in M then so is f. If the composite of two M-maps is an isomorphism then so are both maps. Proof Since M-maps are mono, f is the pullback of f ; m against m.

\begin{matrix}• & \overline{f >} & • & \overline{id >} & • \\ • & \begin{matrix}id \\ ∨ \end{matrix} & \overline{f >} & • & \begin{matrix}id \\ ∨ \end{matrix} & \overline{m >} & • & ^{\begin{matrix}m \\ ∨ \end{matrix} ∩} \end{matrix}

The second term of the composite is both mono and split epi, so iso. □

It may help to think of M-subsets as open. This point of view is consistent with the following completeness assumptions, and with some applications, but in other applications the usual topology may be inappropriate for the purposes of induction. For example continuous lattices [GHK^{+}80] carry two useful topologies: a Hausdorff one (the Lawson or patch topology), and the T_{1} Scott topology, from which the order may be recovered.

Definition 6.3 A category S with a class M of supports is called locally complete if, for each object X of S,

1. there is an admissible set Sub(X) of isomorphism classes of M-maps into X;

2. Sub(X) has arbitrary joins (unions);

3. for every map f : Y → X, the pullback functor f^{∗} : Sub(X) → Sub(Y) preserves arbitrary unions (f^{∗} acts on M-maps by Assumption 4 above);

4. S has a strict initial object ∅ and the unique map ∅ → X lies in M, so the initial object is the least subobject of every object (this is a special case of the previous clause, but for historical reasons we shall treat ∅ explicitly);

5. directed unions in Sub(X) are filtered colimits in S (so regarding the system of M-maps U_{i} ↪ X as a cocone for a filtered diagram, the mediator colim U_{i} → X from the colimit is in M);

6. binary unions in Sub(X) are pushouts in S over the intersection, which is a special case of inverse image and is therefore also in M.

U

U ∩ V^{⊂}................. > U ∪ V ^{⊂}................. >^{⊂................. >}  X \frac{⊂}{>}

V \frac{⊂}{>}^{⊂}................. >^{⊂................. >}

The reason why we want unions is to be able to form the largest member of a class of M-subobjects which has previously been shown to be closed under unions, for example in the next Proposition. This is therefore where second order logic enters in to the construction. This idea also features in category theory as the special adjoint functor theorem (Remark 2.6).

These unions are all bounded: we have certain M-subobjects of a given object X, and need to form their union as another M-subobject. In Section 10 we shall need to form such unions without being given a bound X; the pushout property holds in any (pre)topos, and in certain other categories by direct calculation, but the infinitary colimits must be indexed by “small” objects and their existence depends on the axiom of replacement.

Remark 6.4 Being a union bounded by X means that the cocone (U_{i} → U) has the universal property of a colimit from the point of view of X, i.e. there is a unique mediator to the cocone (U_{i} → X). We shall also need this property from the point of view of T X, Θ and T Θ, but not for other other objects such as Ω. In other words, the “union” need not really be the colimit in the standard sense involving the entire category S, and in fact the “real” S-union may be a subset of our union which is “dense” in the sheaf-theoretic sense. This is the way in which well-foundedness can be tuned more finely to the specific problem of solving the recursion equation f = α ; T f ; θ for functions f : A → Θ for a particular target structure Θ.

The symbolic proof of the following uses structural induction and probably dates back to Georg Cantor [[check history]]. In the category of sets and functions, the object E is simply the equaliser of f and g. Under the completeness assumptions above we may construct an object which is sufficiently like the equaliser for our purposes. If we think of M-subsets as open, then E is the interior of the equaliser, whereas if the target is a Hausdorff space then the equaliser itself is closed. [[Define interior and closure/hull.]]

Proposition 6.5 Let A be a well founded coalgebra, Θ a partial algebra and f, g : A ⇉ Θ be total attempts. Then f = g. Proof The two parallel squares on the right commute since f and g are total attempts (Remark 5.9). Let e : E ↪ A ⇉ V be the greatest M-subobject of A on which f and g agree; this exists, being the colimit of all such subobjects, by Assumption 2. (Indeed we make take E to be the greatest such initial segment.) [[Not the same use of f as before.]]

T E ^{⊂}  T e  > T A \overline{T g>} ; \overline{_{T f>}} T V ^{⊂} T θ> T Θ
E

H ∧ ^{⊂}  > ................... >  A^{α∧}  \overline{f  >} ; \overline{_{g  >}}^{⊂ e >}  V^{j_{∪} ∧} \overline{θ >} Θ

Form the pullback H; the composites H ⇉ T Θ are equal by construction, and j is mono by hypothesis, so H ↪ A ⇉ V are equal. Then H ↪ A is member of the class of subobjects of which E was the union, so H ↪ E ↪ A. Hence e : E ≅ A by well-foundedness of A and f = g [Tay96, 2.5] [Osi74, 6.5]. □

It follows in particular that the category of T -ensembles and coalgebra homomorphisms is merely a preorder, under a relation which we may think of as “set-theoretic inclusion”. In fact every such homomorphism is mono, but we need the main Theorem to prove this.

Proposition 6.6 The colimit of any diagram of coalgebras and coalgebra homomorphisms is given by the colimit of the carriers. If the individual coalgebras are well founded then so is the colimit. If they are extensional and the diagram is filtered then the colimit is also extensional.

(The empty case of the last part is trivial; we defer pushouts to Proposition 10.6.) Proof Finding the structure map on a colimit is easy (as illustrated in the diagram on the left), and the last part follows from Assumption 5.

T X  T Y ^{⊂}  > T X

............

T X_{i}  \overline{▷}  \overline{▷} T X_{j}  \overline{▷} T Y_{i} ^{⊂}.................................................... pbk  > ∧  T X_{i}  \overline{▷}

X \begin{matrix}△ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}  W ^{⊂}  > Y \underline{⊂}  \overline{>} X^{△}
[figure: ............; ............]
X_{i}^{△}  \overline{▷}  \overline{▷} X_{j}^{△}  \overline{▷} W_{i} \begin{matrix}∧ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix} ^{⊂}.................... pbk > Y_{i} ^{⊂}........................ pbk > X_{i}^{△}  \overline{▷}

To show that X ▷ T X is well founded, form the pullbacks Y_{i} and W_{i} against the colimiting cocone X_{i} ▷ X. By well foundedness of the X_{i}, these diagrams are degenerate (Y_{i} ≅ X_{i}). Hence Y is the vertex of a cocone over the diagram X_{i}, so has a mediator from X, so Y ≅ X. □

Proposition 6.7 Let N ⊂ M be two classes of supports in S both satisfying the completeness assumptions. Then a coalgebra α : A → T A is well founded with respect to all M-subobjects U ↪ A iff it is well founded with respect to all N -subobjects V ↪ A. Proof Ā fortiori M-well-foundedness implies N -well-foundedness. Conversely let U be an Msubobject satisfying the induction premise. Since N is closed under unions, let V ⊂ U be the largest N-subobject contained in U [[interior]] and form the pullback as shown.

T V ^{⊂} > T U ^{⊂}  > T A

K ∧ ^{⊂}  > H ∧ ^{⊂}  > U ^{⊂}  > A^{△α}

V \frac{⊂}{>}^{.......................... >}

Then K ⊂ A is an N -subobject with K ⊂ H ⊂ U, so K ⊂ V by construction of V. Hence V ≅ U ≅ A by N -well-foundedness. □

Although well-foundedness is independent of M, extensionality is not. Where necessary we must therefore speak of “well founded T -coalgebras” but “(T, M)-ensembles” (understanding that the category S, and therefore the applicable complete classes of supports, are implicit in the functor T).

Remark 6.8 The colimits constructed in these two results are of diagrams consisting only of coalgebra homomorphisms, and in fact we shall only need to consider unions of initial segments. We haven’t yet needed stability of unions under pullbacks, but for this too the map in question will always be a coalgebra homomorphism.

Writing Seg(A) for the poset of initial segments of a (well founded) coalgebra A, what we require is that Seg(A) be a frame (it has arbitrary unions, finite intersections, and binary meet distributes over arbitrary joins, cf. the open set lattice of a topological space), and that f^{∗} restrict to a frame homomorphism whenever f : B ▷ A is a coalgebra homomorphism.

Proposition 7.3 makes use of completeness of Sub(X), but an alternative proof will be given in Proposition 8.7 using only Seg(A). However for this the other assumptions need a little strengthening, in ways which the applications are likely to be able to support very easily.

Since Sub(X) or Seg(A) have arbitrary joins and f^{∗} preserves them, the latter has a right adjoint. This and the left adjoint, which exists if we also ask (not unreasonably) that M be closed under arbitrary intersections, are the subject of the next section.

7 Proving well-foundedness

Three techniques ...

The main result of this section is a fact about well founded relations which everyone knows, but most people don’t know they know: that strictly monotone functions reflect well-foundedness. This is what justifies their use to prove that recursive programs terminate and that recursive definitions are valid. On the domain of definition of a recursively defined function p, we may write y ≺ x if y is one of the immediate sub-arguments used to compute p(x). Usually this relation is not amenable to direct analysis, but if we can assign a number or ordinal f(x) (sometimes called a loop variant) to each argument x such that f(y) < f(x) whenever y ≺ x then we have shown termination.

This lemma is rather obvious if well-foundedness is given either of the classical definitions,

1. every non-empty subset has a ≺-minimal element (and excluded middle holds), or

2. there is no infinite descending sequence ⋯ x_{3} ≺ x_{2} ≺ x_{1} (and dependent choice also holds),

but it becomes more difficult to prove when the induction scheme is used as a definition.

Proposition 7.1 Let f : B → A be a strictly monotone function. Then if (A, ≺) is well founded, so is (B, <). Proof Put V = {b ∈ B : ϕ[b]}, so as in Definition 3.5,

T V = {W ⊂ B : ∀y ∈ W . ϕ[y]} H = {b ∈ B : ∀y ∈ B. y ≺_{B} b ⇒ ϕ[y]}.

In order to use well foundedness of A, we aim to show that K ⊂ f_{∗}V, where

K  = {a ∈ A : ∀x ∈ A. x ≺_{A} a ⇒ ψ[x]}
≡ {a ∈ A : ∀y ∈ B. f(y) ≺ a ⇒ ϕ[y]}
f^{∗}K = {b ∈ B : ∀y ∈ B. f(y) ≺ f(b) ⇒ ϕ[y]}
f_{∗}V = {a ∈ A : ψ[a] ≡ ∀y ∈ B. f(y) = a ⇒ ϕ[y]}

from Definition 3.1. Monotonicity of f says y ≺_{B} b ⇒ fy ≺_{A} fb, so

(∀y ∈ B. fy ≺_{A} fb ⇒ ϕ[y]) ⇒ (∀y ∈ B. y ≺_{B} b ⇒ ϕ[y]) ⇒ ϕ[b],

i.e. f^{∗}K ⊂ W ⊂ V. Since f^{∗} ⊣ f_{∗}, we deduce K ⊂ f_{∗}V (maybe the reader should verify this step symbolically), i.e. for a ∈ A,

(∀x ∈ A. x ≺ a ⇒ ϕ[x]) ⇒ (∀y ∈ B. fy = a ⇒ ϕ[y]) ≡ ψ[a].

Hence ∀a. ψ[a] by induction in A, from which ∀b. ϕ[b] follows. □

The more difficult proof has uncovered something interesting: we need an auxiliary predicate ψ[y] ≡ ∀x. (f(x) = y) ⇒ ϕ[x], which, in particular, involves a universal quantifier.

Proposition 7.2 The pullback functor f^{∗} : Sub(X) → Sub(Y) has a right adjoint f_{∗}. If M is also closed under arbitrary limits (intersections) then f^{∗} has a left adjoint as well. Proof Define f_{!} ⊣ f^{∗} ⊣ f_{∗} by

f_{∗}(V) = ⋃ {U : f^{∗}(U) ⊂ V }
f_{!}(V) = ⋂ {U : V ⊂ f^{∗}(U)}

since f^{∗} preserves unions by Assumption 3, and intersections by the additional hypothesis. □

Compare this result with Definition 3.1. The powerset P(X), if it exists, is an object of the category S, whereas Sub(X) is defined externally as a set of M-maps. The latter exists for most familiar categories, though for example it is a complete modular lattice (not distributive) if X is a module for a ring, whereas the existence of the former is the main part of the definition of a topos (cf. Remark 3.8)

The Assumptions of the previous section are also insufficient to characterise f_{∗} and f_{!} as ∀ and ∃. A quantified formula may in general have free variables, and the result of substituting expressions for these must still obey the logical rules for the quantifiers. Categorically this may be expressed as stability of the universal properties under pullback, or as the Beck-Chevalley condition [Tay99]. However it turns out that this condition is not needed for either of the quantifiers in the present work.

Using the right adjoint f_{∗} (the universal quantifier ∀) we shall now give the diagrammatic form of Proposition 7.1, in the case where f is a coalgebra homomorphism. Comparing with Remark 3.4, this is a simulation; we shall discuss the version for strictly monotone functions (sub-homomorphisms) afterwards.

Proposition 7.3 Let f : (B, β) → (A, α) be a homomorphism of coalgebras with A well founded. Then B is also well founded.

\begin{matrix}T B & \overline{T f ▷} & T A \\ B & ^{β△} & \overline{f ▷} & A & ^{△α} \end{matrix}

Proof Given the diagram marked in thick lines, apply the right adjoint (7.2) to j : V ^{⊂} > B, to get i : f_{∗}V ^{⊂} > A with counit ϵ. Note that the little triangle (∗) commutes. The upper part of the diagram is the T -image of the lower part. Let K = α^{∗}T (f_{∗}V) be the pullback of T i and α.

(T f)^{∗}T (f_{∗}V) = T (f^{∗}f_{∗}V) \overline{_{pbk  >}} T (f_{∗}V)

T V ^{⊂} T j  > \frac{<}{T ϵ} \begin{matrix}∧ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}  T B \overline{T f  ▷} \frac{⊂}{>}  ∧  T A^{_{⊂} T i >}

f^{∗}K . . . . . . . . . . . . . . \overline{pbk}  \overline{>} K pbk

H ∧ ^{⊂}  > < ........................ V ^{⊂} \begin{matrix}j \\ (∗) \end{matrix} > B^{△β} \overline{f  ▷} \frac{⊂}{>}  . . . . . . . . . . . . . .  A^{△α} \frac{⊂}{>}

f^{∗}f_{∗}V^{ϵ∧}  \overline{pbk >} \frac{⊂}{>}  f_{∗}V^{∨. . . . . . . . . . . . . .} ^{⊂}  i >

We have f^{∗}K ↪ B → T B and f^{∗}K → K → T (f_{∗}V) agreeing at T A, so there is a pullback mediator f^{∗}K → T (f^{∗}f_{∗}V). Then f^{∗}K → T (f^{∗}f_{∗}V) → T V agrees with f^{∗}K ↪ B at T B (since the top triangle commutes), so there is also a pullback mediator f^{∗}K → H. Then since f^{∗} ⊣ f_{∗} we have K → f_{∗}V. Since A is well founded, i : f_{∗}V ≅ A and j : V ≅ B. □

These proofs differ in that the diagrammatic one assumed that f is a simulation (β;T f = f;α), whilst the symbolic one only required it to be strictly monotone (β;T f ⊑ f;α, Remark 3.4). This could be accommodated in to the diagrammatic argument by replacing the pullback T (f^{∗}f_{∗}V) by a comma square T B ↓ T (f_{∗}V), but T ϵ would also have to be extended. In fact, in the case of the powerset, the pullback and comma square are actually the same. It is not clear what abstract Assumption to make to generalise this situation.

Proposition 7.4 Let T, P : S → S be functors and κ : T → P a cartesian transformation i.e. a natural transformation whose naturality squares are pullbacks. Then any T -coalgebra α : A ▷ T A is well founded (with respect to T) iff α; κ_{A} : A → P A is well founded with respect to P.

P U ^{⊂}  P i  > P A

T U^{κ_{U}∧} ^{⊂}  T i  > T A^{∧κ_{A}}

H ∧ ^{⊂}  > U ^{⊂} i > A^{△α}

Proof The induction hypothesis H is the same for P and T. □

Proposition 7.5 Let T : Set → Set. Then there is a natural transformation κ : T → P which is cartesian with respect to monos (as above) iff T preserves arbitrary intersections.

Proof For any set X and t ∈ T X, define κ_{X} : T X → P(X) by

κ_{X}(t) = {x ∈ X : ∀U ⊂ X. t ∈ T U ⇒ x ∈ U}.

Now (t, V) ∈ T A × P(U) lies in the pullback iff V = κ_{X}(t) ⊂ U. If T preserves intersections, this happens iff t ∈ T U.

\begin{aligned}P(⋂_{i} U_{i}) & {= \atop =} & ⋂_{i} P(U_{i}) & ^{⊂} > & P(U_{i}) & ^{⊂} > & P(A) \\ T (⋂_{i} U_{i}) & ^{κ_{⋂_{i} U_{i}}∧} & ^{⊂} > & ⋂_{i} T (U_{i}) & ∧ & ^{⊂} > & T (U_{i}) & ^{∧κ_{U_{i}}} & ^{⊂} > & T (A) & ^{∧κ_{A}} \end{aligned}

The condition is necessary because P preserves arbitrary intersections and pullbacks commute with them. □

Definition 7.6 In these circumstances we may define the immediate sub-expression relation on A by x ≺ a ⟺ x ∈ κ_{A}(α(a)). Such T was called an analytic functor in [Joy87] since it has a “power series” representation.

The left adjoint f_{!} (the existential quantifier ∃) can be used to transmit well foundedness forwards along surjective coalgebra homomorphisms, and to construct the extensional (Mostowski) reflection. There is an alternative categorical formulation:

Proposition 7.7 There is a left adjoint f_{!} ⊣ f^{∗} iff M is part of a factorisation system.

\begin{aligned}X & \overline{>>} & Q \\ U & ∨ & ^{⊂} > & < ......................... & Y & ∨ \end{aligned}

The factorisation is used in categorical logic to interpret the existential quantifier:

\begin{matrix}\{⟨x, y⟩ : ϕ[x, y]\} & ....................................... >> & \{x : ∃y. ϕ[x, y]\} \\ X × Y & ^{∨ ∩} & \overline{π_{0} >} & X & ^{∨ \begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}} \end{matrix}

Lemma 7.8 Let f : A ↠ B be a surjective coalgebra homomorphism. Then if A is well founded, so is B.

T (f^{∗}V) >  > T A

T V  \overline{>} >  ∧ T B >

• ∧ pbk  > f^{∗}V ≅ ; pbk > A

H ∧  \overline{>} >  V ^{⊂}i > >  B ∧^{f>>}

Proof Pull the test diagram with i : V ^{⊂} > B for B (at the front) back along f : A ↠ B. By well-foundedness of A, f^{∗}V ≅ A. Then f : A ↠ B factors through i : V ^{⊂} > B, so the latter is an isomorphism [Tay96, 2.7]. □

Definition 7.9 Let α : A ▷ T A and β : B > ▷ T B be T -coalgebras with B extensional. Then a coalgebra homomorphism f : A ▷ B (or, loosely, B) is said to be the extensional reflection of A if it is the universal such, i.e. for any other coalgebra homomorphism g : A ▷ C with C extensional there is a unique coalgebra homomorphism h : B ▷ C with g = f ; h. The similar property for total attempts g : A → Θ and h : B → Θ, where Θ is a partial algebra, may be deduced.

For the usual reasons, the extensional reflection is unique up to unique isomorphism. If M is part of a factorisation system (E, M) in S, then g ∈ E. If A is well founded then by the Lemma so is B, and h ∈ M by Remark 10.3, so the extensional quotient is characterised simply by the existence of a coalgebra E-homomorphism A ↠ B.

Proposition 7.10 Let α : A ▷ T A be a T -coalgebra. Suppose that the object A is co-well-powered, i.e. there is an admissible set of isomorphism classes of E-maps out of A, and that all colimits of such E-maps exist. Then A has an extensional reflection. Proof Let A ↠ B ↪ T A be the image factorisation of the structure map; we make this a coalgebra by the composition B ↪ T A → T B.

A  \overline{f  ▷} Θ

B ∨ ∨ ^{⊂} > ............................................... g  > T A \overline{T f ▷}^{α ▷}  T Θ^{\begin{matrix}θ \\ ∨ \end{matrix} ∩}

T B ∨ .......................... T g >

Given a coalgebra homomorphism f : A ▷ Θ to an extensional coalgebra (or a total attempt A → Θ to a partial algebra T Θ ⇀ Θ), the orthogonality of A ↠ B to Θ > ▷ T Θ gives g : B → Θ making the diagram commute.

The new coalgebra B need not be extensional, so we could try iterating this process, but we don’t know when to stop. Instead, we regard the construction as a monotone endofunction on the poset of quotients of A.

\begin{aligned}T A & \overline{>} & T B & \overline{>} & T C \\ A & △ & \overline{>>} & B & △ & \overline{>>} & C & \frac{<}{⊃} \end{aligned}

Assuming that this is a complete lattice, there is a greatest fixed point, which is the required extensional quotient. If A is well founded then the fixed point is actually unique. □

In the category of sets and functions, outgoing surjective functions correspond bijectively to equivalence relations (we say that Set has effective quotients of equivalence relations), cowell-powered-ness follows from the control we already have on the incoming monos. [Tay96, 2.11] constructed the equivalence relation on a well founded P-coalgebra.

There exists a complete class of supports (lower subsets of posets) which is part of a factorisation system whose E-part (cofinal functions) is neither stable nor co-well-powered. In this case, the extensional reflection (called the plump rank in [Tay96]) of well founded coalgebras may still be found, but, like Mostowski’s original construction, this depends on the axiom of replacement.

We shall find that ensembles, as their name suggests, behave in a very set-theoretic fashion. However practical applications of the general recursion theorem actually employ well founded coalgebras, as we saw at the beginning of this section: extensionality is not a natural requirement.

8 The von Neumann hierarchy

In this section we shall show how all of the T -ensembles (and well founded coalgebras) are generated by the “ZF-axioms” of empty set, application of the functor, unions and subsets. We must show on the one hand that these operations take extensional, well founded coalgebras to extensional, well founded coalgebras, and on the other that all T -ensembles are obtained in this way. This latter part is an induction scheme: any property which is transmitted by these operations is shared by all T -ensembles.

In the case where the functor is the powerset, it is the von Neumann hierarchy which is generated by the empty set, application of the functor, and unions. For arbitrary functors this construction is the one mentioned in Remark 2.6, but both the special and general cases rely on an already given system of ordinals. By closing under subsets as well, we obtain a diagram whose vertices have an intrinsic characterisation, namely being extensional, well founded coalgebras.

Lemma 8.1 The initial object ∅, together with the unique map ∅ > ▷ T ∅, is a T -ensemble. Proof Assumption 4. □

Application of the functor preserves ensembles, but it will be convenient to prove something slightly more general.

Lemma 8.2 Let α : A ▷ T A and β : B ▷ T B be coalgebras with A well founded. Suppose there are coalgebra homomorphisms f : A ▷ B and g : B ▷ T A such that α = f ; g and β = g ; T f. Then B is also well founded. Proof Given a pullback square H testing the well-foundedness of B, form the pullback cube along f : A ▷ B.

T U ^{⊂}  > T B

T V ^{⊂}................................................... ≅  > ............ > ∧  T A T f ▷^{< .......................................}

H ^{⊂}  > U \underline{⊂}  \overline{>} B^{△β} \frac{◁}{g}

K \begin{matrix}∧ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix} ^{⊂}................... > ............ > V ^{⊂}........................ ≅  > ............ >  A^{α△} f ▷^{< ................}

Then V ≅ A by well-foundedness of A, so A → U ↪ B → T A → T U, and H ↪ B is split. □

Lemma 8.3 Let A and B be coalgebras and i : B > ▷ T A. Then there is a pullback of coalgebras and homomorphisms as shown (with i = ℓ; T j):

\begin{aligned}B & > ℓ ▷ & T C & >T j ▷ & T A \\ C & ^{k△} & >  j  ▷ & A & ^{△α} \end{aligned}

There is a similar result for B ▷ T A if A is extensional, and without restriction if S has and T preserves all binary pullbacks of coalgebra homomorphisms. Proof The square which says that i is a coalgebra homomorphism,

\begin{aligned}T B & >T i▷ & T^{2}A \\ B & ^{β△} & > i ▷ & T A & ^{△T α} \end{aligned}

has the same top and right edges as the T -image of the pullback above. Hence there is a mediator ℓ : B → T C with β = ℓ; T k : B → T C → T B and i = ℓ; T j : B → T C → T A.

\begin{matrix}B & \overline{β ▷} & T B & \overline{T β ▷} & T^{2}B \\ C & ^{k△} & \overline{_{γ = k ; ℓ▷}} & T C & ^{T k△} & \overline{_{T γ ▷}} & ^{ℓ  ▷} & T^{2}C & ^{△T^{2}k} & ^{T ℓ  ▷} \end{matrix}

Putting γ = k; ℓ : C → B → T C, the objects in the pullback square are coalgebras and the maps are homomorphisms. □

Propositions 6.6 and 7.3 have already dealt with colimits and initial segments.

Theorem 8.4 Let V be a class of T -coalgebras such that the “Zermelo axioms” hold:

1. ∅ ∈ V;

2. if A ∈ V then also T A ∈ V;

3. if A ∈ V and B > ▷ A is an initial segment (or, in particular, an isomorphism), then also B ∈ V;

4. if A = ⋃_{i} A_{i} as an I-indexed union of coalgebras with A_{i} ∈ V, then A ∈ V.

Then V contains all T -ensembles, and, in particular, the initial algebra is in V if it exists.

If we replace B > ▷ A by B ▷ A in 3 then V contains all well founded T -coalgebras. Proof Let A be any well founded coalgebra, and put U = {B ⊂ A : B ∈ V}. By hypotheses 1, 3 (in the weaker form) and 4, U contains ∅ and is closed under unions and initial segments. Hence, putting U = ⋃ U, we have

B ∈ U ⟺ A ◁ < B ∈ V ⟺ B > ▷ U,

and in particular U ∈ V.

T U > ▷ T H > ▷ T A
U

H^{△} >  ▷ .......................... >  A^{△α} \frac{>}{▷}

Then T A ◁ < T U ∈ V by hypothesis 2, so by Lemma 8.3 the pullback H is a coalgebra. For the result about ensembles, A > ▷ T A and H > ▷ T U are mono, so A ◁ < H ∈ V by hypothesis 3. The stronger form, for general coalgebra homomorphisms, is needed in the case of well founded coalgebras. Hence H > ▷ U by construction of U, and A = U ∈ V by well-foundedness. Finally, recall from Propositions 2.4 and 2.5 that the initial algebra is an ensemble. □

Remark 8.5 This proof made no use of the conditions that unions of M-subobjects be colimits and stable under pullback. Hence it is legitimate to use Zermelo induction to verify these conditions in applications.

By way of an example of this Theorem, we may give an alternative proof of Proposition 7.3 which makes direct use of stable unions instead of the adjunction f^{∗} ⊣ f_{∗}.

Lemma 8.6 Let A = ⋃ A_{i} be a union of coalgebras such that whenever C ▷ A_{i} then C is well founded. Let f : B ▷ A. Then B is also well founded. Proof Form the pullbacks B_{i} = f^{∗}A_{i}.

A_{i} >  ▷ ⋃ A_{i} = = = = A

T A_{i} >  ▷ \overline{▷}  ^{△}  T A^{α ▷}

B_{i} \begin{matrix}△ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix} ^{^{⊂}............} .........▷ ⋃ B_{i} >.... ≅▷ Bf

T B_{i} \begin{matrix}△ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix} >.............................................▷^{............▷}  T B^{△T f}^{β ▷}

Since T preserves pullbacks, the front rectangle is also a pullback and the B_{i} are coalgebras with B_{i} ▷ A_{i}, so the B_{i} are well founded by hypothesis. Since f^{∗} preserves unions, B = ⋃ B_{i}, which is well founded by Proposition 6.6. □

Proposition 8.7 Let f : B > ▷ A be an initial segment of a well founded coalgebra A. The B is also well founded. Proof Conditions 1 and 3 of the Theorem are trivial, whilst the Lemma has shown number 4. For 2, given B > ▷ T A, form C > ▷ A by Lemma 8.3 (which used a pullback) and apply Lemma 8.2 with C in place of A. □

9 The general recursion theorem

We are now ready to prove the general recursion theorem, which says that each T -ensemble obeys the recursion scheme, i.e. a partial form of the universal property of the free algebra. Traditionally this has been proved using by pasting together partial functions, which we regard as total functions defined on its initial segments. These initial segments range over the class of T -ensembles. We shall instead show that there is a greatest attempt A ⇀ Θ by induction on A, using Theorem 8.4.

Throughout let θ : T Θ ⇀ Θ be a fixed total or partial algebra.

Lemma 9.1 There is a unique attempt ∅ ⇀ Θ. □

Lemma 9.2 Let α : A ▷ T A be a coalgebra and f : A ⇀ Θ an attempt. Then (T f ; θ) : T A ⇀ Θ and (α; T f ; θ) : A ⇀ Θ are also attempts, with f ⊑ (α; T f ; θ).

T^{2}A \overline{\begin{matrix}T^{2}f \\ ⇀ \end{matrix}} T^{2}Θ
⊔∣
T A^{T α△}  \overline{\begin{matrix}T f \\ ⇀ \end{matrix}} T Θ \begin{aligned}& T θ \\ ⇃ \end{aligned}
⊔∣
A^{α△}  \overline{f ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}

Note that this is diagram a diagram of partial functions. Remark 5.9 characterised partial attempts in this way, and by Proposition 5.4 T acts on partial maps and preserves the order between them.

□

Let us pause for a moment to consider the corresponding symbolic result. In set theory, given

f(a) ⊑ θ({f(x) : x ≺ a}) ≡ g(a) ≡ u,

consider also

θ({g(x) : x ≺ a}) = θ({θ({f(y) : y ≺ x}) : x ≺ a}) ≡ v.

If u is defined then so is each f(x), for x ≺ a, and hence θ({f(y) : y ≺ x}) is also defined and equal to f(x). Then u and v are the same expression.

In algebra we have similarly

f(r(s_{i}(y_{ij}))) ⊑ r(f(s_{i}(y_{ij}))) ⊑ r(s_{i}(f(y_{ij})))

in an informal notation. It was to eliminate such manipulation of multiple suffices etc. in algebraic topology that functors first became an established part of the mathematical vocabulary.

Lemma 9.3 Suppose f : A ⇀ Θ is the greatest attempt from A. Then T f ; θ : T A ⇀ Θ is the greatest attempt from T A. Proof We already know that T f ; θ is an attempt on T A, so let g be another.

T A \overline{\begin{matrix}T f \\ ⇀ \end{matrix}} T Θ  T A \overline{T α▷} T^{2}A \overline{\begin{matrix}T g \\ ⇀ \end{matrix}} T Θ
⊔∣  ⊔∣
A^{α△}  \overline{f ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}  A^{α△} > α ▷ T A^{T α△}  \overline{g ⇀} Θ \begin{aligned}& θ \\ ⇃ \end{aligned}

Then α; g is an attempt on A, so α; g ⊑ f since f is the greatest such. Hence g ⊑ T α; T g ; θ ⊑ T f ; θ. □

Lemma 9.4 Let i : B > ▷ A and suppose C ◁ < A →^{f} Θ is the greatest attempt on A. Then B ◁ < C ∩_{A} B > ▷ C → Θ is the greatest attempt on B. Proof It is an attempt; let B ◁ < D → Θ be another. Then A ◁ < B ◁ < D → Θ is also an attempt on A, so D > ▷ B ∩_{A} C. □

A similar argument (with f^{∗}C instead of B ∩ C) works for an arbitrary coalgebra homomorphism f : B ▷ A if f_{!} ⊣ f^{∗} exists (Proposition 7.2): we deduce D > ▷ f^{∗}C from f_{!}D > ▷ C. Otherwise there is a difficulty with the application of the proof of Theorem 8.4; this can easily be mended, but we shall return to this point later.

We have to divide consideration of unions into the empty, binary and directed cases, but the empty case has been done.

Lemma 9.5 Let A = ^{⋃↑}A_{i} be a directed union of well founded coalgebras. Suppose that on each A_{i} there is a greatest attempt f_{i} : A_{i} ⇀ Θ. Then there is also a greatest attempt f = ^{⋁↑}f_{i} : A ⇀ Θ. Proof Let B_{i} > ▷ A_{i} > ▷ A be the supports of the f_{i} and put B = ^{⋃↑}B_{i} > ▷ A. Since B is the filtered colimit, there is a mediator f : B → Θ to the cocone f_{i} : B_{i} → Θ. It is an attempt because β ; T f ; θ : B ⇀ Θ is also a mediator.

Now let g : C → Θ with C > ▷ A be another attempt. Put C_{i} = A_{i} ∩C > ▷ A, so C = ^{⋃↑}C_{i}. Then g_{i} : A_{i} ◁ < C_{i} > Θ is an attempt on A_{i}, so g_{i} ⊑ f_{i} : A_{i} ⇀ Θ. That is, C_{i} ⊂ B_{i}, and g agrees with f_{i} on C_{i}. Hence by uniqueness of colimit mediators g agrees with f on C, i.e. g ⊑ f on A. □

Lemma 9.6 Let A be a coalgebra with A = B ∪ C, the union of two initial segments. Suppose that f : B ⇀ Θ and g : C ⇀ Θ are the greatest attempts. Then there is a greatest attempt f ∪ g : A ⇀ Θ. [[Incorporate 10.4.]] Proof Let B′ > ▷ B > ▷ A and C′ > ▷ C > ▷ A be the supports of f and g respectively.

B′ ∩_{A} C > ▷ B′ >  ▷ B

B′ ∪_{A} C′ > ▷ \frac{>}{▷}  A \frac{>}{▷}

B ∩_{A} C′^{∧ \begin{matrix}△ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}} ^{^{▽} \begin{matrix}∨ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}} > ▷ \frac{>}{▷} C′ >  ▷ \frac{>}{▷}C \frac{>}{▷} \frac{>}{▷}

As in Lemma 9.4, B ◁ < B ∩ C′ > ▷ C′ →^{g} Θ is a partial attempt on B, so B ∩ C′ > ▷ B′. Similarly B′ ∩ C > ▷ C′, so B′ ∩ C = B ∩ C′ = B′ ∩ C′. Moreover the two restricted attempts agree here. Hence by Assumption 6, there is a pushout mediator B′ ∪_{A} C′ → Θ.

Now let h : A ⇀ Θ be another attempt, with support D. Then B ∩ D ⊂ B′ and C ∩ D ⊂ C′, so D = (B ∩ D) ∪ (C ∩ D) ⊂ (B′ ∪ C′) and h agrees with f ∪ g on them, i.e. h ⊑ f ∪ g. □

A simpler version of this argument, but still using Assumption 6, shows that the attempts A ⇀ Θ on any well founded coalgebra form a directed set, so there is a greatest one since this homposet also has directed joins. To show that any two attempts A ◁ < B → Θ and A ◁ < C → Θ agree on B ∩_{A} C we use Lemma 6.5 instead of relying on being given greatest attempts. Unlike Lemma 9.4, this method extends from ensembles to well founded coalgebras without the need for f_{!} ⊣ f^{∗}.

We have now verified the conditions of Theorem 8.4 needed to prove the General Recursion Theorem for ensembles, and proved it another way for well founded coalgebras.

Theorem 9.7 Let A be a well founded coalgebra and Θ a partial algebra. Then there is a greatest attempt f : A ⇀ Θ, and this satisfies the strict recursion scheme, f = α; T f ; θ. If Θ is total then so is f. Proof Let f : A ⇀ Θ be the greatest attempt. Since α;T f;θ is also an attempt, by Lemma 9.2, we must have f = α; T f ; θ. (This is playing the roles of T U and H in Theorem 8.4.) If Θ is total then so is f by Lemma 5.11. □

From this we may describe the initial algebra (if it exists).

Proposition 9.8 In the category of well founded coalgebras and coalgebra homomorphisms, an object θ : Θ ▷ T Θ is terminal iff it is parsable, i.e. θ is an isomorphism.

Moreover for any other well founded coalgebra A ▷ T A, the greatest attempt f : A ⇀ Θ is total and is the unique coalgebra homomorphism. Proof The terminal coalgebra is parsable by the dual of Proposition 2.4; this argument restricts to well founded coalgebras by Lemma 8.2.

Conversely, let Θ be a parsable well founded algebra. By the Theorem, from any other well founded algebra A there is a greatest attempt f : A ⇀ Θ; this satisfies f = α; T f ; θ and is total. It is a homomorphism by Remark 5.10 and unique either by Lemma 6.5 or because there is only one maximal attempt. □

Corollary 9.9 The terminal T -ensemble or well founded coalgebra is the initial algebra. □

10 Set-theoretic union and intersection

To anyone from any other mathematical discipline, one of the most bizarre features of set theory is its notion of union. [[Merging crowds.]] (The Wiener-Kuratowski formula {{a}, {a, b}} for an ordered pair, on which the set-theoretic interpretation of type theory and thereby of mathematics depend, is perhaps rather more bizarre, and seems to have no analogue in this work.)

In this section we shall investigate set-theoretic union and intersection by specialising Theorem 9.7 to the case where Θ is another T -ensemble.

Remark 10.1 The next result shows, amongst other things, that every coalgebra homomorphism f : A → B between T -ensembles is mono [Tay96, 2.5] [Osi74, 6.5]. The proof would be much simpler if we knew this in advance. One way of showing it would be to make the further Assumption that the kernel pair of f exists in S, i.e. the pullback of f against itself; by Lemma 6.5 the pair would be equal, so f is mono. Although this assumption is valid in Set, we might wish to apply our techniques to some category (of topological spaces, maybe) which does not have arbitrary pullbacks. □

Proposition 10.2 Let A and B be T -ensembles. The greatest attempts A ⇀ B and B ⇀ A are given by the same span (which, in particular, consists of two mono coalgebra homomorphisms) A ↩ P ↪ B. Moreover this is the meet in the preorder of T -ensembles. Proof Let A ◁ < U ▷ B and B ◁ < V ▷ A be the greatest attempts, as given by Theorem 9.7; all four of these maps are coalgebra homomorphisms. Consider the composite A ⇀ B ⇀ A, with support P; this is an attempt. The identity is also an attempt, which is total and so maximal, hence by Theorem 9.7 A ⇀ B ⇀ A is less than id, so P ⊂ A.

A
P  \overline{>} V
P  >^{< ..........................}  V  \overline{_{g ▷}} A^{id  ▷}
U^{∨ ∩}  \overline{f ▷} B^{j_{▽} ∨}
U ∨ \overline{f ▷} B^{j_{▽} ∨}
A^{g  ▷}^{>  i  ▷}
A^{i_{▽} ∨} ^{id  ▷}

The diagram on the left says this verbatim, and that on the right is a re-arrangement. Note that P is the pullback rooted at B, but the kite P ⇉ A also commutes.

Forming a similar diagram from B ⇀ A ⇀ B, with pullback Q, the mediators P ⇆ Q between the pullbacks and commutative squares make P ≅ Q. Hence in the diagram shown on the right above, P is also the pullback rooted at A, and P ↪ V.

Remark 10.3 (Continuing the proof, by induction on P ⊂ U.) The composite H ↪ T P ↪ T V ↪ T B is mono, and factors through the mono β : B > ▷ T B, so H → U → B is also mono. Hence it is the support of an attempt B ⇀ A, whose effect is H → U → A. But V is the support of the greatest such attempt, so there is a mediator H → V making the diagram commute, and H → P is the mediator to the pullback.

P ^{⊂}  > V

H ^{⊂}  > .............................................. > .......................... > U^{∨ ∩} > i ▷ A g_{▽}

T P^{∨ ∩} > ▷ T U^{^{▽} ∨}  B^{>  j  ▷}^{f  ▷}

T V^{∨ ∩} >  T j  ▷ T B^{β_{▽} ∨}^{T f  ▷}

By well-foundedness of U, we now have P ≅ U, and by a similar argument we may also show that P ≅ V.

To show that A ◁ < P > ▷ B is the intersection, consider any pair of inclusions A ◁ < D > ▷ B; these define an attempt A ⇀ B, so D > ▷ P. □

Proposition 10.4 Let A > ▷ C ◁ < B be coalgebra homomorphisms between T -ensembles. Then the intersection A ∩ B is the pullback in S.

Proof Form the pullback P, which consists of monos and so is preserved by T. Hence P is a coalgebra; it is extensional by by the cancellation property of monos and well founded by Proposition 7.3, and A ↩ P ↪ B are coalgebra homomorphisms.

T P >  ▷ T A

P >  ▷^{◁..............<}  ^{∩}  A \frac{◁}{<}

T B^{^{▽} ∨} \underline{⊂}  \overline{▷} T C^{▽}

B^{^{▽} ∨} >  ▷ \frac{◁}{<}  C^{^{▽} ∨} \frac{◁}{<}

The intersection A∩B also provides a commutative cube, so there is a pullback mediator A∩B → P. But A ↩ P ↪ B is an attempt, so there is a mediator to the greatest such, P → A ∩ B. Hence P ≅ A ∩ B. □

Assumption 10.5 Pushouts over intersections.

any two M-maps W ↪ U and W ↪ V have a pushout, P, where U ↪ P and V ↪ P are also in M; moreover if U, V ^{⊂} > X such that the square from W to X is a pullback, then P ↪ X is also in M.

Proposition 10.6 The preorder of T -ensembles and total attempts has binary unions. Proof Let A ∪ B be the pushout of A and B over A ∩ B. This is a well founded coalgebra by Proposition 6.6: we have to show that its structure map is in M.

A >  ▷ T A

A ∩ B\frac{>}{▷}  A ∪ B  \overline{▷} \overline{>}  T (A ∪ B) \frac{⊂}{>}

B >  ▷ \overline{>} \frac{>}{▷}  T B  \overline{>}

Let C = T (A ∪ B) in the previous result, so A ∩ B is the pullback of A > ▷ T (A ∪ B) ◁ < B. By Assumption 6 the pushout mediator A ∪ B > ▷ T (A ∪ B) is in M. □

Definition 10.7 Axiom of replacement [Tay96, 2.13c] and [Osi74, 6.6]

Theorem 10.8 Existence of extensional reflections of well founded coalgebras, using replacement and factorisation.

Theorem 10.9 Suppose that S has set-indexed colimits. Then the functor T has an initial algebra iff, up to isomorphism, there is a set rather than a proper class of T -ensembles. Proof [⇒] A T -ensemble is an initial segment of the initial algebra, and by Assumption 1 there is a set of these. [⇐] Form their colimit, using Assumption 5. □

The “size” words used in this result are not intended to let set theory in by the back door: we’re simply asking that S have colimits indexed by the intrinsically defined category (quâ diagram) of ensembles.

[[Some thoughts on what the definition of rank might be.]]

Finally, we can use the idea of Proposition 5.8 to prove a more general result, although this will not be used in this paper.

Proposition 10.10 Suppose that the ambient category S has and the functor T preserves limits of chains as shown. Then [[coreflection]] for any partial algebra T A ⇀ A there is an extensional coalgebra L > ▷ T L and a total homomorphism of partial algebras L → A with the co-universal property that any total attempt Γ → A factors uniquely as Γ → L → A. Proof Form the pullback of B ↪ T A against T B → T A as shown, to give a partial algebra T B ⇀ B. Repeating the process, the chains along the middle and bottom are the same (but for a shift), so their limits agree.

T L  \overline{>} ⋯  > T C  > T B  \overline{>} T A

L^{^{∪} ∧}  \overline{>} ⋯  > D^{^{∪} \begin{matrix}∧ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}}  > C^{^{∪} \begin{matrix}∧ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}}  > B^{^{∪} ∧}

L ≅ ; ∨  \overline{>} ⋯  > C ∨  > B ∨  \overline{>} A ∨

Assuming that T preserves this limit, so T L is the limit of the chain at the top, the structure map T L ↪ L is the mediator from the middle chain, and is mono because a limit of monos like this is mono. The universal property required follows from that of the limit. □

T Γ
T B  \overline{>}^{................ >}  T A \overline{>}
Γ^{^{∪} ∧}
C^{^{∪} ∧} ^{⊂}  >^{................... >}  B^{^{∪} ∧} >
Γ ‖
B ∨  \overline{>}^{................... >}  A ∨ >

11 Recursion in other categories

Recursion in arbitrary categories, by embedding in a suitable sheaf topos. The recursion equation (for particular A, T and Θ) is the same, but the induction scheme becomes more complicated: instead of subobjects we must consider sieves.

12 Additional material

One or more of the following may be added to this paper; the rest will be in Part II.

• Interpretation of ΠΘ.(T Θ → Θ) → Θ.

References

[Acz88] Peter Aczel. Non-well-founded sets. CSLI Lecture Notes 14. Center for the Study of Language and Information, 1988.

[BF97] Cesare Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo matematico di Palermo, 11:154–164, 1897. English translation in [vH67], pages 104– 111.

[BW85] Michael Barr and Charles F. Wells. Toposes, Triples, and Theories. Springer-Verlag, Berlin, Germany, Heidelberg, Germany, London, UK etc., 1985.

[Can83] Georg Cantor. Über unendliche, lineare Punktmannichfaltigkeiten. Mathematische Annalen, 21:545–591, 1883.

[CLW93] Aurelio Carboni, Steve Lack, and Robert F.C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84:145–158, 1993.

[Ded94] J. W. Richard Dedekind. The nature and meaning of numbers. In Essays on the Theory of Numbers. 1894. Dover (1960).

[FA66] Gottlob Frege and Ignacio Angelelli. Begriffschrift und Andere Aufsätze. Olms, Hildesheim, 1966.

[Fre79] Gottlob Frege. Begriffschrift, eine der Arithmetischen Nachgebildete Formalsprache des Reinen Denkens. 1879. Reprinted in [FA66]; English translation in [vH67], pages 1–82.

[Fre91] Peter J. Freyd. Algebraically complete categories. In A. Carboni et al., editors, Proc. 1990 Como Category Theory Conference, pages 95–104, Berlin, 1991. Springer-Verlag. Lecture Notes in Mathematics Vol. 1488.

[Fre92] Peter J. Freyd. Remarks on algebraically compact categories. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science: Proceedings of the LMS Symposium, Durham, 1991, number 177 in LMS Lecture Notes. Cambridge University Press, 1992.

[GHK^{+}80] Gerhard K. Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Lawson Jimmie D., Michael W. Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, 1980.

[Hei86] Gerhard Heinzmann, editor. Poincaé, Russell, Zermelo at Peano: Textes de la Discussion (1906–1912) sur les Fondements des Mathématiques: des Antinomies à la Prédicativité. Bibliothèque Scientifique. Albert Blanchard, 9 Rue de Médicis, Paris, 1986.

[JM95] André Joyal and Ieke Moerdijk. Algebraic Set Theory. Number 220 in London Mathematical Society Lecture Notes in Mathematics. Cambridge University Press, 1995.

[Joh77] Peter T. Johnstone. Topos Theory. Academic Press, London, 1977.

[Joy87] André Joyal. Foncteurs analytiques et espèces de structures. In Combinatoire énumerative, volume 1234 of Lecture Notes in Mathematics, pages 126–159. Springer Verlag, 1987.

[Lam68] Joachim Lambek. A fixed point theorem for complete categories. Mathematische Zeitung, 103:151–161, 1968.

[Lam70] Joachim Lambek. Subequalisers. Canadian Bulletin of Mathematics, 13:337–349, 1970.

[Law64] F. William Lawvere. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences of the United States of America, 52:1506–1511, 1964.

[Law69] F. William Lawvere. Adjointness in foundations. Dialectica, 23:281–296, 1969.

[LS81] Daniel J. Lehmann and Michael B. Smyth. Algebraic specifications of data types: a synthetic approach. Mathematical Systems Theory, 14:97–139, 1981.

[LS86] Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics Vol. 7. Cambridge University Press, 1986.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.

[Mir17a] Dimitry Mirimanoff. Les antinomies de Russell et de Burali-Forti, et le problème fondemental de la théorie des ensembles. Enseignement Mathématique, 19:37–52, 1917.

[Mir17b] Dimitry Mirimanoff. Remarques sur la théorie des ensembles et les antinomies cantoriennes, I. Enseignement Mathématique, 19:209–217, 1917.

[Mog91] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[Mon55] Richard Montague. Well founded relations; generalisations of principles of induction and recursion. Bull. AMS, 61, 1955.

[Mos49] Andrzej Mostowski. An undecidable arithmetical statement. Fundamenta Mathematica, 36:143–164, 1949.

[Osi74] Gerhard Osius. Categorical set theory: a characterisation of the category of sets. Journal of Pure and Applied Algebra, 4:79–119, 1974.

[Pea89] Giuseppe Peano. The principles of arithmetic, presented by a new method. In Jean van Heijenoort, editor, From Frege to Gödel, pages 20–55. 1889.

[Pit94] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994. (A preliminary version of this work appeared as Cambridge Univ. Computer Laboratory Tech. Rept. No. 252, April 1992.).

[Poi09] Henri Poincaré. La logique de l’infini (I). Rev. mét. et mor., 17:461–482, July 1909. Reprinted in [Hei86], pages 235–256.

[Poi12] Henri Poincaré. La logique de l’infini (II). Scientia, 12:1–11, 1912. Reprinted in [Hei86], pages 305–316.

[PS78] Robert Paré and Dietmar Schumacher. Abstract families and the adjoint functor theorem. In Peter T. Johnstone and Robert Paré, editors, Indexed Categories and their Applications, volume 661 of Lecture Notes in Mathematics, pages 1–125. Springer-Verlag, 1978.

[Tar55] Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific J Math, 5:285–309, 1955.

[Tay89] Paul Taylor. Quantitative domains, groupoids and linear logic. In David Pitt, editor, Category Theory and Computer Science 3, volume 389 of Lecture Notes in Computer Science, pages 155–181. Springer Verlag, 1989.

[Tay91] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay96] Paul Taylor. Intuitionistic sets and ordinals. Journal of Symbolic Logic, page 45, September 1996.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[vH67] Jan van Heijenoort. From Frege to Gödel: a Source Book in Mathematical Logic, 1879–1931. Harvard University Press, Cambridge, MA, 1967.

[vN23] John von Neumann. Zur Einführung der transfiniten Zahlen. Acta litterarum ac scientiarum Regiae Universitatis Hungaricae Franscisco-Josephinae, Section scientiarum mathematicarum, 1:199–208, 1923. English translation in Jean van Heijenoort, ed., From Frege to Gödel, Harvard University Press, 1967, pp 346–354.

[Zer08] Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 59:261–281, 1908. Translation by van Heijenoort in From Frege to Gödel.

[Zer30] Ernst Zermelo. Über Grenzzahlen und Mengenbereiche. Fundamenta Mathematicae, 16:29–47, 1930.

Bernoulli, Euclid, Fermat, Giraud, Dana Scott, Skolem, Tierney From Wilfrid Hodges:

• Montague, Scott and Tarski: On Set Theory and Well Founded Sets, circa 1960, unpublished.

• Zermelo, 1930, Über Grenzzahlen und Mengenbereiche, Fundamenta Mathematicae 16 (1930) 29–47.