An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor’s constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of topos.
If i_\alpha is an isomorphism for some \alpha\in\mathsf{Ord}, then (F^\alpha 0, i_\alpha^{-1}) is an initial algebra for F:\mathcal{C}\rightarrow\mathcal{C}. So in particular, if F preserves colimits of shape \lambda for some limit ordinal \lambda, then (by the definition of “preserves colimits”) i_\lambda is an isomorphism and F^\lambda 0 is an initial F-algebra.
Recall that a semi-category is like a category, but lacks identity morphisms. A semi-category is thin if there is at most one morphism between any pair of objects. Thus a small thin semi-category is the same thing as a set \kappa (the set of objects) equipped with a transitive relation \_<\_ \subseteq \kappa\times\kappa (the existence-of-a-morphism relation). Given such a (\kappa,{<}), a diagram D:\kappa\rightarrow\mathcal{C} in a category \mathcal{C} is by definition a semi-functor from \kappa to \mathcal{C}: thus D maps each i\in\kappa to a \mathcal{C}-object D_i, each pair (j,i) with j<i to a \mathcal{C}-morphism D_{j,i}: D_j\rightarrow D_i, and these morphisms satisfy D_{j,i}\circ D_{k,j} = D_{k,i} for all k<j<i in \kappa.
A size is a small thin semi-category (\kappa,{<}) that is
directed: every finite subset of \kappa has an upper bound with respect to <; specifically, we assume we are given a distinguished element 0^s\in\kappa and a binary operation \_\mathbin{\sqcup^s}\_:\kappa\times\kappa\rightarrow\kappa satisfying \forall i,j\in\kappa.\; i< {i \mathbin{\sqcup^s} j} \;\wedge\; j < {i\mathbin{\sqcup^s} j}
well-founded: for all K\subseteq \kappa, if \forall i\in\kappa.(\forall j< i.\; j \in K) \Rightarrow i\in K, then K = \kappa.
Note that the directedness property in particular gives a successor operation \mathop{\uparrow^s} : \kappa\rightarrow\kappa on the elements of a size, defined by \mathop{\uparrow^s} i \triangleq i\mathbin{\sqcup^s} i and satisfying \forall i\in\kappa.\; i < \mathop{\uparrow^s} i. (We do not need a successor that also preserves <, although the sizes constructed in the next section have one that does so.)
In the next section we will define a rich class of sizes derived from algebraic signatures (see Proposition 4.2). For now, we note that the natural numbers \mathbb{N} with their usual strict order is a size.\mathbb{N} will be the smallest size once one has developed a comparison relation between sizes. To do that one probably has to restrict to sizes that are extensional, that is, satisfy \forall i,j\in\kappa.\;\{k\in\kappa\mid k<i\} = \{k\in\kappa\mid k<j\} \Rightarrow i = j. However, we have no need of that property for the results in this paper. In classical logic, an ordinal is a size iff its usual strict total order is directed, which happens iff it is a limit ordinal.
Since we are working constructively, the well-foundedness property of a size is stated in a suitably positive form; classically, it is equivalent to the non-existence of infinite descending chains for <. Well-foundedness of < allows one to define size-indexed families by well-founded recursion [TaylorP:prafm, section 6.3]: given a size \kappa and a \kappa-indexed family of sets (A_i)_{i\in\kappa}, from each family of functions (f_i:(\prod_{j<i}A_j)\rightarrow A_i)_{i\in\kappa} we get a family of elements (a_i\in A_i)_{i\in\kappa}, uniquely defined by the requirement \forall i\in\kappa.\; a_i= f_i((a_j)_{j<i}).
Let \kappa be a size. Given an endofunctor F:\mathcal{C}\rightarrow\mathcal{C} on a cocomplete category \mathcal{C}, a diagram D:\kappa\rightarrow\mathcal{C} is an inflationary iteration of F over \kappa if for all i\in\kappa
Given an endofunctor F:\mathcal{C}\rightarrow\mathcal{C} on a cocomplete category \mathcal{C}, for each size \kappa an inflationary iteration of F over \kappa exists (and is unique).
Given i\in\kappa, say that a diagram D:{\downarrow}(i)\rightarrow\mathcal{C} is an inflationary iteration of F up to i if for all j<i, D_j = \operatorname{\mathrm{colim}}_{k<j}F(D_k) and \forall k<j.\; D_{k,j}= \mathrm{c}^{F\circ D}_{k,j}. Note that given such a diagram, for any j<i we have that D|_j:{\downarrow}(j)\rightarrow\mathcal{C} is an inflationary iteration of F up to j. Using well-founded induction for <, one can prove that
Then one can use well-founded recursion for < (Remark 3.4) to define for each i\in\kappa an inflationary iteration of F up to i, D^{(i)}:{\downarrow}(i)\rightarrow\mathcal{C}. If j<i, then D^{(j)} and D^{(i)}|_j are both inflationary iterations of F up to j and so are equal by (Proof). From this it follows that
defines an inflationary iteration of F. (Furthermore, since any such restricts to an up-to-i inflationary iteration, uniqueness follows from (Proof).)
We record some simple properties of inflationary iteration that we need in the proof of the theorem below. Let D:\kappa\rightarrow\mathcal{C} be the inflationary iteration of F:\mathcal{C}\rightarrow\mathcal{C} over \kappa. Note that for all j<i in \kappa, the components of the colimit cocone \mathrm{inc}^{F\circ D|_i}_j: F(D_j) \rightarrow \operatorname{\mathrm{colim}}_{j<i}F(D_j) are morphisms \iota_{j,i}: F(D_j) \rightarrow D_i satisfying
The first equation follows from the fact that D_{j,i} = \mathrm{c}^{F\circ D}_{j,i} and the second from the definition of \iota_{j,i} as a component of a cocone. Since that cocone is colimiting, one also has for all i\in\kappa and all \mathcal{C}-morphisms f,g:D_i\rightarrow X that
Suppose \mathcal{C} is a cocomplete category, F:\mathcal{C}\rightarrow\mathcal{C} is an endofunctor and there is a size \kappa such that F preserves colimits of diagrams \kappa\rightarrow\mathcal{C}. Then F has an initial algebra whose underlying \mathcal{C}-object is the colimit \mu F = \operatorname{\mathrm{colim}}_{i\in\kappa}\mu_i F of the inflationary iteration \mu_i F (Definition 3.5) of F over \kappa.
By Lemma 3.6 there is an inflationary iteration of F:\mathcal{C}\rightarrow\mathcal{C} over \kappa; call it D:\kappa\rightarrow\mathcal{C} and define \mu F \triangleq \operatorname{\mathrm{colim}}_{i\in\kappa}D_i. For each i\in\kappa, as in Definition 3.2 we have \mathop{\uparrow^s} i\in\kappa with i < \mathop{\uparrow^s} i and hence a \mathcal{C}-morphism
By (3.7), (\iota_i)_{i\in\kappa} is a cocone under the diagram F\circ D : \kappa\rightarrow\mathcal{C} and so induces \hat{\iota}: \operatorname{\mathrm{colim}}_{i\in\kappa}F(D_i) \rightarrow \mu F. Then since F preserves the colimit of D, we get a morphism
Therefore \mu F has the structure of an F-algebra. To see that it is initial, suppose we are given a:F(A)\rightarrow A. We have to show that there is a unique F-algebra morphism (\mu F, \iota)\rightarrow (A,a).
If h:\mu F \rightarrow A is such an algebra morphism, that is h\circ\iota = a\circ F(h), then by definition of \iota in (Proof) it follows that the associated cocone (h_i \triangleq h \circ \mathrm{inc}^D_i:D_i\rightarrow A)_{i\in\kappa} satisfies h_{\mathop{\uparrow^s} i}\circ \iota_{i,\mathop{\uparrow^s} i}= a\circ F(h_i). From this, using the directedness property of sizes, we get
So if h and h' are both F-algebra morphisms (\mu F, \iota)\rightarrow (A,a), one can prove by well-founded induction for <, using (3.7) and (?), that \forall i\in\kappa.\; h\circ \mathrm{inc}^D_i = h'\circ\mathrm{inc}^D_i and hence that h=h'.
So it just remains to prove that there is such an h. It suffices to construct a cocone (h_i:D_i\rightarrow A)_{i\in\kappa} satisfying (?) and then take h to be the morphism given by the universal property of the colimit; for then we have \forall i\in\kappa.\; h_{\mathop{\uparrow^s} i}\circ \iota_{i,\mathop{\uparrow^s} i} = a\circ F(h_i) and hence h\circ\iota = a\circ F(h), as required.
For each i\in\kappa, say that a morphism h':D_i\rightarrow A is an up-to-i algebra morphism if \forall j<i.\;h'\circ\iota_{j,i} = a\circ F(h'\circ D_{j,i}) (cf. (?)). Given such a morphism, then for any j<i, h'\circ D_{j,i}:D_j\rightarrow A is an up-to-j algebra morphism. From this it follows by well-founded induction for < that any two up-to-i algebra morphisms are equal. A well-founded recursion for < allows one to construct an up-to-i algebra morphism h_i:D_i\rightarrow A for each i\in\kappa; and the uniqueness of up-to algebra morphisms implies that h_j=h_i\circ D_{j,i} when j<i. Thus (h_i)_{i\in\kappa} is the required cocone satisfying (?).
With the same assumptions on \mathcal{C}, F and \kappa as in Theorem 3.8, then free F-algebras exist, that is, the forgetful functor from the category of F-algebras to \mathcal{C} has a left adjoint.
The free F-algebra on an object X\in\mathcal{C} is the same thing as an initial algebra for the endofunctor F(\_)+X. So by the theorem, it suffices to check that F(\_)+X preserves colimits of diagrams \kappa\rightarrow\mathcal{C}. It does so because F does by assumption and because \kappa is directed (cf. Proposition 4.7(?) below).
A signature (also known as a container [abbott2005containers, GambinoN:welftd]) is specified by a set A\in\ensuremath{\mathbf{Set}} and an A-indexed family of sets B\in\ensuremath{\mathbf{Set}}^A. We write \ensuremath{\mathbf{Sig}} \in \ensuremath{\mathbf{Set}}_1 for the large set of all such signatures. Given \Sigma=(A,B)\in\ensuremath{\mathbf{Sig}}, we say that a size (\kappa,{<}) is \Sigma-filtered if for all a\in A and every function f:B(a) \rightarrow \kappa, there exists i\in\kappa with \forall x\in B(a).\; f(x) < i.
There is a \Sigma-filtered size (\kappa_\Sigma , {<}) for every signature \Sigma.
Given a signature \Sigma=(A,B), we extend it to a signature (A',B') by adding fresh nullary and binary operation symbols. Thus A' \triangleq A\uplus\{n,b\} and B'\in\ensuremath{\mathbf{Set}}^{A'} satisfies B'(a) \triangleq B(a) for a\in A, B'(n)\triangleq \emptyset and B'(b)\triangleq \{0,1\}. Let set \kappa_\Sigma be the W-type W_{(A',B')} and let < be the plump order given by (?). As noted above, < is transitive and well-founded and has upper bounds for any arity-indexed family and hence in particular it is \Sigma-filtered. It just remains to see that it is directed (Definition 3.2). Since A' contains the nullary operation symbol n, \kappa_\Sigma contains 0^s\triangleq \sup_n\emptyset; and given i,j\in\kappa_\Sigma, letting f:B'(b)=\{0,1\}\rightarrow \kappa_\Sigma map 0 to i and 1 to j, then i\mathbin{\sqcup^s} j \triangleq \sup_b f is an upper bound for i and j with respect to <.
Given a signature \Sigma\in\ensuremath{\mathbf{Sig}}, a functor F:\mathcal{C}\rightarrow\mathcal{D} between cocomplete categories is \Sigma-sized if it preserves colimits of all diagrams \kappa\rightarrow\mathcal{C} for any \Sigma-filtered size \kappa. A functor is sized it there exists a signature \Sigma for which it is \Sigma-sized.
Assuming \mathcal{C} is a cocomplete category, if F:\mathcal{C}\rightarrow\mathcal{C} is sized, then there exists an initial algebra for F. More precisely, there is a function assigning to each signature \Sigma and each \Sigma-sized endofunctor F an initial algebra for F.
If F is \Sigma-sized for some \Sigma\in\ensuremath{\mathbf{Sig}}, then F preserves colimits of diagrams for the \Sigma-filtered size \kappa_\Sigma constructed in the proof of Proposition 4.2. Hence by Theorem 3.8, it has an initial algebra, given by taking the colimit of its inflationary iteration.
Suppose \Sigma_c=(A_c,B_c) is a family of signatures indexed by the elements c of some set C. Then the signature sum \bigoplus_{c\in C}\Sigma_c is the signature (A,B) where A\triangleq \sum_{c\in C}A_c = \{(c,a) \mid c\in C \wedge a \in A_c\} and B\in\ensuremath{\mathbf{Set}}^A maps each (c,a) to the set B_c(a). As a special case when I=\{0,1\}, we have the binary sum \Sigma_0\oplus\Sigma_1. There is also an empty signature 0=(\emptyset,\emptyset) which acts as a unit for \oplus up to isomorphism (for a suitable notion of signature morphism).
Note that if a size is (\bigoplus_{c\in C}\Sigma_c)-filtered, it is also \Sigma_c-filtered for each c\in C. Conversely, given a single signature \Sigma, if a size is \Sigma-filtered, it is also (\bigoplus_{c\in C}\Sigma)-filtered.
Suppose that \mathcal{C},\mathcal{D} and \mathcal{E} are cocomplete categories.
Any cocontinuous functor \mathcal{C}\rightarrow\mathcal{D} is sized.
Identity functors are sized. If F:\mathcal{C}\rightarrow\mathcal{D} and G:\mathcal{D}\rightarrow\mathcal{E} are sized, so is their composition G\circ F: \mathcal{C}\rightarrow \mathcal{E}.
The terminal functor \mathcal{C}\rightarrow 1 and the projection functors \pi_1:\mathcal{C}\times\mathcal{D}\rightarrow \mathcal{C} and \pi_2:\mathcal{C}\times\mathcal{D}\rightarrow \mathcal{C} are sized; if F:\mathcal{C}\rightarrow \mathcal{D} and G:\mathcal{C}\rightarrow \mathcal{E} are sized, then so is \langle F, G\rangle:\mathcal{C}\rightarrow \mathcal{D}\times \mathcal{E}.
For any X\in\mathcal{C} the constant functor 1\rightarrow \mathcal{C} with value X is sized.
For part ?, if F:\mathcal{C}\rightarrow\mathcal{D} is cocontinuous, then it is \Sigma-sized for any \Sigma and in particular for the empty signature.
The first sentence of part ? follows from part ?. If F is \Sigma-sized and G is \Sigma'-sized, then F and G both preserve colimits over any \Sigma\oplus\Sigma'-filtered size, because such a size is also \Sigma- and \Sigma'-filtered. The composition G\circ F preserves such a colimit because F and G do. Therefore G\circ F is \Sigma\oplus\Sigma'-sized.
For part ? we use the fact that colimits in a product category are computed componentwise. Thus the terminal and projection functors are sized by part ?; and if F:\mathcal{C}\rightarrow \mathcal{D} is \Sigma-sized and G:\mathcal{C}\rightarrow \mathcal{E} is \Sigma'-sized, then \langle F, G\rangle is \Sigma\oplus\Sigma'-sized.
For part ?, note that each size \kappa is directed and hence in particular is a connected semi-category; therefore \operatorname{\mathrm{colim}}_{i\in\kappa} X is canonically isomorphic to X. So the constant functor with value X is \Sigma-sized for any \Sigma and in particular for the empty signature.
A (possibly large) cover of a set X\in\ensuremath{\mathbf{Set}} is a surjective function f:Y\twoheadrightarrow X with Y\in\ensuremath{\mathbf{Set}}_1. An indexed familyWe will refer to elements of \ensuremath{\mathbf{Sig}} as families rather than signatures when we are not thinking of them as collections of operation symbols of set-valued arity. (E_c)_{c\in C} \in \ensuremath{\mathbf{Sig}} is a wisc for X\in\ensuremath{\mathbf{Set}} if for any cover f:Y\twoheadrightarrow X, there exist c\in C and g : E_c \rightarrow Y such that f\circ g is surjective. The [wisc] axiomFor simplicity and following [StreicherT:reamc], we have given the axiom just for a pair of universes, (\ensuremath{\mathbf{Set}}_0,\ensuremath{\mathbf{Set}}_1); more generally one can ask for the property to hold for any pair (\ensuremath{\mathbf{Set}}_m,\ensuremath{\mathbf{Set}}_n). states that for every X\in\ensuremath{\mathbf{Set}} there exists a family (E_c)_{c\in C}\in\ensuremath{\mathbf{Sig}} that is a wisc for it.
Suppose [wisc] holds and that \mathcal{C} and \mathcal{D} are cocomplete categories. If (F_x:\mathcal{C}\rightarrow\mathcal{D})_{x\in X} is a family of sized functors indexed by a set X\in\ensuremath{\mathbf{Set}}, then there exists a signature \Sigma\in\ensuremath{\mathbf{Sig}} such that F_x is \Sigma-sized for all x\in X.
Consider the large set S \triangleq \sum_{x\in X}\{\Sigma'\in\ensuremath{\mathbf{Sig}} \mid \text{F_xis a’-sized functor}\} in \ensuremath{\mathbf{Set}}_1. By assumption on F, the first projection \pi_1:S\rightarrow X is a largeThis proof, as well as that for Lemma 4.12, illustrates the need for a wisc property that quantifies over large covers of small sets. cover of X. By [wisc] there is some surjection e:X'\twoheadrightarrow X in \ensuremath{\mathbf{Set}} and a function \Sigma':X'\rightarrow \ensuremath{\mathbf{Sig}} so that for all x'\in X', the functor F_{e(x')} is \Sigma'_{x'}-sized; and since e is surjective this implies that each F_x is \Sigma'_{x'}-sized for some x'\in X'. Consider the signature \Sigma \triangleq \bigoplus_{x'\in X'}\Sigma'_{x'} from Definition 4.5. By Remark 4.6, each F_x is \Sigma-sized.
Suppose that [wisc] holds, \mathcal{C} and \mathcal{D} are cocomplete categories, \mathbf{C} is a small category and that F:\mathbf{C}\times\mathcal{C}\rightarrow\mathcal{D} is a functor. If for some signature \Sigma\in\ensuremath{\mathbf{Sig}} the functor F(c,\_) is \Sigma-sized for each c\in\mathbf{C}, then \operatorname{\mathrm{colim}}_{c\in\mathbf{C}}F(c,\_):\mathcal{C}\rightarrow\mathcal{D} is also \Sigma-sized. More generally, if each F(c,\_) is sized, then so is \operatorname{\mathrm{colim}}_{c\in\mathbf{C}}F(c,\_).
If F(c,\_):\mathcal{C}\rightarrow\mathcal{D} is \Sigma-sized for all c\in\mathbf{C} and \kappa is a \Sigma-filtered size, then each F(c,\_) preserves colimits of all diagrams \kappa\rightarrow\mathcal{C}. Thus given such a diagram D:\kappa\rightarrow\mathcal{C}, we have a canonical isomorphism F(c,\operatorname{\mathrm{colim}}_{i\in\kappa}D_i) \cong \operatorname{\mathrm{colim}}_{i\in\kappa}F(c, D_i), natural in c. Taking the colimit over c\in\mathbf{C} and writing F' \triangleq \operatorname{\mathrm{colim}}_{c\in\mathbf{C}}F(c,\_), we have F'(\operatorname{\mathrm{colim}}_{i\in\kappa}D_i) = \operatorname{\mathrm{colim}}_{c\in\mathbf{C}}F(c,\operatorname{\mathrm{colim}}_{i\in\kappa}D_i) \cong \operatorname{\mathrm{colim}}_{c\in\mathbf{C}}\operatorname{\mathrm{colim}}_{i\in\kappa} F(c,D_i). Since colimits commute with each other, it follows that the canonical morphism F'(\operatorname{\mathrm{colim}}_{i\in\kappa}D_i)\rightarrow\operatorname{\mathrm{colim}}_{i\in\kappa}F'(D_i) is an isomorphism. Therefore F' is \Sigma-sized. The last sentence of the theorem follows by Lemma 4.9.
Suppose [wisc] holds and that \mathcal{C} and \mathcal{D} are cocomplete categories. If F:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{D} is sized, then there is a function X\mapsto \mu Y.F(X,Y) assigning to each X\in\mathcal{C} an initial algebra \mu Y.F(X,Y) for the functor F(X,\_):\mathcal{D}\rightarrow\mathcal{D}. The induced functor \mu Y.F(\_,Y):\mathcal{C}\rightarrow \mathcal{D} is sized.
Suppose F:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{D} is \Sigma-sized. It follows from Proposition 4.7 and Remark 4.6 that for each X\in\mathcal{C}, the functor F_X \triangleq F(X,\_):\mathcal{D}\rightarrow\mathcal{D} is \Sigma-sized. Therefore by Theorem 3.8, Theorem 4.4, the function X\mapsto \mu Y.F(X,Y)\triangleq \operatorname{\mathrm{colim}}_{i\in \kappa_\Sigma}\mu_i F_X is the required function mapping each X\in\mathcal{C} to an initial algebra for F(X,\_). Since each \mu_i F_X is \operatorname{\mathrm{colim}}_{j<i}F(X, \mu_j F_X), it follows by well-founded induction on i\in\kappa_\Sigma that each \mu_i F_X is \Sigma-sized, using Theorem 4.10 (taking \mathbf{C} to be the category generated by the thin semi-category {\downarrow}(i)). Then by Theorem 4.10 again (taking \mathbf{C} to be the category generated by \kappa) we have that \mu Y.F(\_,Y) = \operatorname{\mathrm{colim}}_{i\in \kappa_\Sigma}\mu_i F_{\_} is \Sigma-sized.
Assuming [wisc] holds, then for every family of sets (X_i)_{i\in I}\in\ensuremath{\mathbf{Sig}} there exists a family (E_c)_{c\in C}\in\ensuremath{\mathbf{Sig}} that is a wisc for each set X_i.
Consider S \triangleq \sum_{i\in I}\{W\in\ensuremath{\mathbf{Sig}} \mid \text{Wis a wisc forX_i}\} \in \ensuremath{\mathbf{Set}}_1. By [wisc], the first projection \pi_1:S\rightarrow I is a large cover of I. Since there is a wisc for I, it follows that there is some surjection e:J\twoheadrightarrow I in \ensuremath{\mathbf{Set}} and a function W:J\rightarrow \ensuremath{\mathbf{Sig}} so that for all j\in J, W_j is a wisc for X_{e(j)}. Consider the signature sum W\triangleq\bigoplus_{j\in J}W_j\in\ensuremath{\mathbf{Sig}} as in Definition 4.5. Thus writing (C,E) for W and (C_j,E_j) for each W_j, we have C\triangleq \sum_{j\in J} C_j \in \ensuremath{\mathbf{Set}} and E\in \ensuremath{\mathbf{Set}}^C is the function mapping each (j,c)\in \sum_{j\in J} C_j to E_j(c). Then we claim that W\in\ensuremath{\mathbf{Sig}} is a wisc for each set X_i. For, given any cover f:Y\twoheadrightarrow X_i, since e:J\twoheadrightarrow I is a surjection, there exists j\in J with e(j)= i; then since W_j=(C_j,E_j) is a wisc for X_{e(j)} = X_i, there exists c\in C_j and g:E_j(c)\rightarrow Y such that f\circ g is surjective. So there exists (j,c)\in C and g:E(j,c) = E_j(c) \rightarrow Y such that f\circ g is surjective. Therefore W=(C,E) does indeed have the wisc property for X_i.
Suppose that \mathcal{C} is a cocomplete category. Assuming [wisc] holds, if (F_x:\mathcal{C}\rightarrow\ensuremath{\mathbf{Set}})_{x\in X} is a family of sized functors indexed by some set X\in\ensuremath{\mathbf{Set}}, then the functor \prod_{x\in X}F_x : \mathcal{C}\rightarrow\ensuremath{\mathbf{Set}} given by taking products in \ensuremath{\mathbf{Set}} is also sized.
By Lemma 4.9, there exists a signature \Sigma so that each functor F_x is \Sigma-sized. However, we need a bigger signature than \Sigma in order to prove that \prod_{x\in X}F_x is sized. Using [wisc], let W = (E_c)_{c\in C} be a wisc for X. Then using Lemma 4.12, let W' = (E'_{c'})_{c'\in C'} be a wisc for the sets in the family (\ker p)_{c\in C, p: E_c\twoheadrightarrow X}, where
We claim that the functor F'\triangleq\prod_{x\in X}F_x is \Sigma'-sized when \Sigma' = \Sigma \oplus W \oplus W' (using the signature sum from Definition 4.5).
If D:\kappa\rightarrow \mathcal{C} is a diagram on a \Sigma'-filtered size \kappa, then by Remark 4.6, each F_x is \Sigma'-sized and so we have a canonical isomorphism \operatorname{\mathrm{colim}}_{i\in\kappa} F_x(D_i) \cong F_x(\operatorname{\mathrm{colim}}_{i\in\kappa} D_i). Taking the product over x\in X, we get \prod_{x\in X} \operatorname{\mathrm{colim}}_{i\in\kappa} F_x(D_i) \cong \prod_{x\in X} F_x(\operatorname{\mathrm{colim}}_{i\in\kappa} D_i) = (\prod_{x\in X} F_x)(\operatorname{\mathrm{colim}}_{i\in\kappa} D_i). So it just remains to show that the canonical function
is an isomorphism, that is, both an injection and a surjection. The summand W in \Sigma' ensures that \kappa has upper bounds for E_c-indexed families for any c\in C; and the W' summand ensures the same for E'_{c'}-indexed families, for any c' \in C'. The first kind of upper bound, together with the wisc property of W, comes into play in proving that \operatorname{\mathrm{can}}_{F,D} is injective; and both kinds of upper bounds and the wisc property of W and W' come into play in proving that \operatorname{\mathrm{can}}_{F,D} is surjective.
To prove that \operatorname{\mathrm{can}}_{F,D} is injective and surjective we use the fact that the colimit in \ensuremath{\mathbf{Set}} of a directed diagram D:\kappa\rightarrow\ensuremath{\mathbf{Set}} can be described explicitly as the quotient (\sum_{i\in\kappa}D_i)/{\approx} where the equivalence relation \approx identifies (i,d),(i',d') \in \sum_{i\in\kappa}D_i if there is some j\in\kappa with i<j, i'<j and D_{i,j}(d) = D_{i',j}(d'). We will write [i,d]_{\approx} for the {\approx}-equivalence class of (i,d)\in \sum_{i\in\kappa}D_i. Then the function in ? satisfies for all i\in \kappa and f\in \prod_{x\in X} F_x(D_i)
To see that \operatorname{\mathrm{can}}_{F,D} is injective, suppose we also have i'\in \kappa and f'\in \prod_{x\in X} F_x(D_i) satisfying \forall x \in X.\; [i,f(x)]_{\approx} = [i',f'(x)]_{\approx}; we wish to prove that (i,f)\approx(i',f'). By definition of \approx we have \forall x\in X.\exists j\in\kappa.\; i < j \;\wedge\; i' < j \;\wedge\; F_x(D_{i,j})(f\,x) = F_x(D_{i',j})(f'x). Since W = (E_c)_{c\in C} is a wisc for X, there exist c\in C, a surjection p:E_c\twoheadrightarrow X and a function q:E_c\rightarrow \kappa so that
Since W is a summand in \Sigma' and \kappa is a \Sigma'-filtered size, there is an <-upper bound j\in\kappa for q:E_c\rightarrow \kappa; and since \kappa is directed, we can assume i<j and i'<j. So from (?) and surjectiviy of p we deduce that \forall x\in X.\; F_x(D_{i,j})(f\,x) = F_x(D_{i',j})(f'x), which implies (i,f)\approx (i',f'). Therefore the function \operatorname{\mathrm{can}}_{F,D} in (?) is indeed injective.
To see that \operatorname{\mathrm{can}}_{F,D} is also surjective, suppose we have g\in\prod_{x\in X}\operatorname{\mathrm{colim}}_{i\in\kappa}F_x(D_i). Since
and W is a wisc for X, there exists some c\in C, p:E_c\twoheadrightarrow X and \langle q_1,q_2\rangle \in \prod_{z\in E_c} \sum_{i\in\kappa}F_{p(z)}(D_i) so that \forall z\in E_c.\; g(p\,z) =[q_1(z),q_2(z)]_{\approx}. Then since W is a summand in \Sigma' and \kappa is a \Sigma'-filtered size, there is an <-upper bound j\in\kappa for q_1:E_c\rightarrow \kappa. So we have
where q'\in\prod_{z\in E_c}F_{p(z)}(D_j) is q'(z)\triangleq F_{p(z)}(D_{q_1(z),j})(q_2(z)). It follows that the relation \Phi\subseteq \sum_{x\in X} F_x(D_j) given by \Phi(x,d) \triangleq \exists z\in E_c.\; x = p(z) \;\wedge\; d = q'(z) is total (because p is surjective); and were it also single-valued, it would determine a function f\in\prod_{x\in X} F_x(D_j) which by virtue of (?) would satisfy \operatorname{\mathrm{can}}_{F,D}[j,f] = g. However, we need to increase j to get this single-valued property. Recall that W' is a wisc for the kernel (Proof) of p:E_c\twoheadrightarrow X. If (z_1,z_2)\in \ker p, then by (?) [j,q'(z_1)]_{\approx} = g(p\,z_1) = g(p\,z_2) = [j,q'(z_2)]_{\approx}. Therefore we have
So since W'=(E_{c'})_{c'\in C'} is a wisc for \ker p and \kappa has E_{c'}-indexed upper bounds for any c'\in C' and is directed, it follows that there exists c'\in C', \langle p_1,p_2\rangle:E_{c'}\twoheadrightarrow \ker p and k\in\kappa with j<k and
Now if we let q''\in\prod_{z\in E_c}F_{p(z)}(D_k) be q''(z)\triangleq F_{p(z)}(D_{q_1(z),k})(q_2(z)), then from (?) we have
Let the relation \Phi'\subseteq \sum_{x\in X} F_x(D_k) be \Phi'(x,d) \triangleq \exists z\in E_c.\; x = p(z) \;\wedge\; d = q''(z). It is total because p is surjective; but it is also single-valued because if \Phi'(x,d) \wedge \Phi'(x,d'), then d = q''(z_1) \wedge d' = q''(z_2) for some (z_1,z_2)\in \ker p, so that there exists z''\in E_{c'} with p_1(z'')=z_1 \wedge p_2(z'') = z_2 and hence d=q''(z_1) = q''(z_2) = d' by (?). Therefore \Phi' is the graph of a function f\in\prod_{x\in X} F_x(D_k); and by virtue of (?) we have \forall x\in X.\; g(x) = [k,f(x)]_{\approx}, so that g = \operatorname{\mathrm{can}}_{F,D}[k,f]. Thus \operatorname{\mathrm{can}}_{F,D} is indeed surjective.
The symmetric containers of Gylterud [GylterudHR:symc] generalize ordinary signatures by replacing the set of operation symbols by a groupoid \mathbf{A} and the arity function by a functor B:\mathbf{A}\rightarrow\ensuremath{\mathbf{Set}}. The associated endofunctor S_{\mathbf{A},B}:\ensuremath{\mathbf{Set}}\rightarrow\ensuremath{\mathbf{Set}} maps each set X\in\ensuremath{\mathbf{Set}} to the colimit
Applying Theorem 4.4, Proposition 4.7 and Theorem 4.13 we have that any topos with universes satisfying [wisc] has initial algebras for symmetric containers.
In fact these initial algebras are special cases of QW-types [PittsAM:quoitq]: they can be seen as sets of terms quotiented by the symmetries given by the groupoid structure on the arguments of an operation symbol. So their existence in toposes with [wisc] follows from the results of that paper. However, the construction here in terms of a colimit of an inflationary iteration gives a simpler description than for the general case of a QW-type.
The text on this page is from arXiv:2105.03252v3 by Andrew M. Pitts and S. C. Steenkamp, under the licence CC BY 4.0. The corpus made these changes: it read the items out of the LaTeX source, it expanded the macros of the paper, it put each proof after its statement, and it converted the text to HTML. The formulas are the TeX of the paper, and KaTeX renders them. A formula or a reference can look different from the PDF. The page is published under CC BY 4.0.
The record of each item is in analysis/objects/2105/2105.03252.jsonl.