Makkai’s lost proof of projectivity of \(N\)
in the free topos
April 01, 2026
We give a categorical proof of the projectivity of \(N\) in the free topos — in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic — based on the unpublished proof of Michael Makkai [1].
The presentation aims to be self-contained and accessible to any reader acquainted with elementary toposes and their logic.
In 1986, Lambek and Scott wrote [2]:
The question in the text concerning the projectivity of N in the free topos, equivalently, the countable rule of choice in pure type theory, has of course been solved by proof-theoretical techniques (see Friedman and Scedrov 1983). Makkai in unpublished notes (1980) cast the logician’s proof into a categorical (actually \(2\)-categorical) mould.
Unfortunately, neither of the cited proofs ever saw the light of day, and the proofs have generally been considered lost [3].
In December 2015, Michael Makkai visited Stockholm, where the first two authors were then postdocs. We pressed him on this topic; once back home, he unearthed his original (marvellously lucid) notes and kindly gave us his blessing to write up the proof for eventual publication. After barely another decade, here it is.
In the end, our treatment diverges substantially from Makkai’s original — primarily due to the subsequent development of the field, partly of course just from personal taste, and finally from the desire to give as self-contained and elementary an exposition as possible. In particular, we hope this should be accessible for essentially anyone familiar with elementary toposes and a little of their basic development.
Like many constructive systems, intuitionistic higher-order logic (\(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)), the logic of elementary toposes, enjoys various meta-theorems saying that existence proofs can be distilled into constructions. Most fundamental is the existence property (\(\mathrm{EP}\)): if \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}A \ {\varphi(x)}\)”, then there is some \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)-definable \(a \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}A\) for which \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\varphi(a)\)”.
Categorically, this says that in the free topos, every cover of the terminal object \(\HOLinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}A \mathrel{\mid}\varphi(x)] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1\) splits; that is, \(1\) is projective. Freyd’s famous gluing argument gives a very clean, purely categorical proof of this fact.
Our main goal is to strengthen this, to show that the rule of countable choice (\(\mathrm{RC}_{\omega}\)) is admissible for \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\). Concretely, if \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ \varphi(n,x)\)”, then there is some \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)-definable function \(f : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) for which \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \varphi(n,f(n))\)”. Categorically again, this says that in the free topos, every cover of the natural numbers object \(N\) splits; in other words, \(N\) is projective.
Certainly, if \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \ \exists\mkern 2mu x \ \varphi(n,x)\)”, the existence property tells us that for each (actual) natural number \(n\), there is some IHOL-definable \(a\) such that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\varphi(\bar{n},a)\)”, where \(\bar{n}\) is the \(n\)th numeral.
It is not hard to leverage this a bit further, to an operation instead of an existence statement: syntax and proofs can be Gödel-numbered, hence well-ordered, so we can define for each \(n\) some specific \(a_n\) (Gödel-number-minimal, say) such that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\varphi(\bar{n},a_n)\)”. However, this operation is still defined externally, not in \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) as desired.
So one might next hope to run the entire above argument not in our ambient meta-theory, but internally to \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), as an argument about a internal formalisation of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) inside itself — denote this \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{}{^{}}\) to distinguish it. Then, if \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \ \exists\mkern 2mu x \ \varphi(n,x)\)”, we argue as follows. First, we internalise that proof to show that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{}{^{}}\) proves ‘\(\forall\mkern 1mu n \ \exists\mkern 2mu x \ \varphi(n,x)\)’”. Then, we would like to run the gluing argument and the Gödel-numbering trick inside \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), to define an operation \(n \mapsto a_n\) such that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n\), \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{}{^{}}\) proves ‘\(\varphi(\bar{n},a_n)\)’”. Finally, we externalise these latter proofs to get that in fact \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \ \varphi(n,a_n)\)”.
Unfortunately, that cannot quite go through as written. The alarm bells ring most loudly in the last step: it attempts to use the inference “if \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{}{^{}}\) proves ‘\(\varphi(\bar{n},a_n)\)’, then \(\varphi(n,a_n)\) holds”. But this is the sort of thing which Tarski’s undefinability of truth tells us cannot be provable or even expressible within \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) (presuming it is consistent). The same problem arises in internalising Freyd’s gluing argument, since it requires interpreting \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{}{^{}}\) internally into a category involving the ambient sets of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\).
However, the attempt can be salvaged. Instead of attempting to internalise the whole of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), we internalise just its \(r\)th-order fragment \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\), for some \(r \in \mathbb{N}\), and interpret that. This takes care, but can be done: \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\) is restricted enough that one can build, in \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), a large enough set-indexed family of sets to interpret it. This is the reflection theorem: \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) can construct the standard interpretation of each of its fragments \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\).
Now we can push through the full argument for \(\mathrm{RC}_{\omega}\). If \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \ \exists\mkern 2mu x \ \varphi(n,x)\)”, then by compactness some finite-rank fragment \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\) suffices for the proof. Internalising this, \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{r}{^{r}}\) proves ‘\(\forall\mkern 1mu n \ \exists\mkern 2mu x \ \varphi(n,x)\)’”. So we can run the gluing/Gödel-numbering argument for \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{r}{^{r}}\) inside \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), to define an operation \(n \mapsto a_n\) such that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n\), \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{r}{^{r}}\) proves \(\varphi(\bar{n},a_n)\)”. Finally, we hit these with the internal interpretation of \(\mathsf{IHOL}_{\mathsf{N}}\@ifnotmtarg{r}{^{r}}\), and get that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \ \varphi(n,\HOLinterp[a_n])\)” — a definable witness function for the original universal-existential statement, as desired.
We promised a category-theoretic proof, though — and the above sketch is couched mostly in proof-theoretic language! Where are the categories?
This is where we admit to a bait-and-switch: the proof-theoretic presentation is clearer and more elementary to sketch, but we will not actually carry it through any further. The categorical version requires a little work to set up, but provides a powerful organising framework that makes the details much easier to carry through rigorously and with good generality.
Recasting the above sketch categorically, we introduce a notion of \(r\)-ranked topos — roughly, a category of sets admitting \(r\) iterations of the power-set operation — stratifying the theory of elementary toposes analogously to the finite-rank fragments \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}} \subseteq \mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\). We then argue as follows:
Any cover \(e : A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} N\) in the free topos \(\freeTop\) lifts, by compactness, to the free \(r\)-topos \(\freeTop[r]\) for some \(r \in \mathbb{N}\). This then internalises to the internal free \(r\)-topos \(\freeTop[r][\freeTop]\) in \(\freeTop\). Topos logic is strong enough to build an internal universe closed under \(r\) iterations of power-sets, and so to construct the standard interpretation for the internal free \(r\)-topos and carry out Freyd’s gluing argument. It follows that \(\freeTop\) has a map from \(N\) giving, for each \(n\), a global section of the fibre \(A_{\bar{n}} \subseteq A\) in \(\freeTop[r][\freeTop]\). Applying to this the internal standard interpretation \(\freeTop[r][\freeTop] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop\) yields the desired section of \(e : A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} N\) in \(\freeTop\).
We start in by collecting a grab-bag of background material as required for later chapters, and fixing notation and terminology for the main notions we work with: first some general categorical logic, then some basics of essentially algebraic (aka cartesian) theories, and lastly the construction of the free topos itself.
In , we define ranked toposes, categorical analogues of the bounded-rank fragments of higher-order logic, and develop their essential properties.
In , we then develop the results on internal ranked toposes required for the main proof; we use the framework of indexed categories to handle the interaction between external and internal ranked toposes, and of locoses/arithmetic universes to construct and analyse internal free ranked toposes. The results there on exact completion and free models in arithmetic universes may be of independent interest (, ).
With this machinery in place, gives the endgame, putting together the main reflection results for projectivity of \(N\) and admissibility of \(\mathrm{RC}_{\omega}\) as sketched above (, ), along with analogues for dependent choice (, ). Finally, we look back over the proof, and discuss possible alternative approaches and related literature.
This article has benefited greatly from discussions with — among others — Phil Scott, Mike Shulman, Steve Vickers, Milly Maietti, Paul Taylor, Andrej Bauer, Davide Perinti, and the regular members of the Stockholm Logic Seminar, particularly Erik Palmgren, Johan Lindberg, Håkon Gylterud, Christian Espíndola, and Sina Hazratpour. Above all, we are grateful to Michael Makkai for his original notes and his blessing for preparing this exposition.
During its (long) preparation, the authors have been supported at various points by the Swedish Research Council project grant 2015-03835 (PI Erik Palmgren), Research Council of Norway grant 230525, the Knut and Alice Wallenberg Foundation project “Type
Theory for Mathematics and Computer Science” (PI Thierry Coquand), the Air Force Office of Scientific Research grant numbers FA9550-21-1-0009 and FA9550-21-1-00241 and the
COST Action CA20111 EuroProofNet, funded by European Cooperation in Science and Technology, www.cost.eu
We begin by recalling some background material, tailored to the forms we will require. cover general category theory and essentially algebraic theories, respectively; these serve mostly to fix notation and note a few theorems we require, so the impatient reader may safely skip them. introduces the free topos and Freyd’s gluing argument; this serves additionally as a warm-up for the ranked versions of these in [sec:ranked-toposes] [sec:indexed-ranked-toposes]. Two further topics, indexed categories and arithmetic universes, we leave until they appear later in the story.
We assume some background in general category theory — essentially, familiarity with the notions involved in elementary toposes and their basic theory. The early chapters of any text in topos theory should certainly suffice — [4], say. For everything beyond this, we recall at least in outline the necessary definitions and results.
In most choices of definitions and terminology, we follow the Elephant [4]. One peculiarity in particular deserves setting out from the start:
Convention 1 ([4]). Whenever we speak of structures satisfying existence conditions (e.g. categories with limits, essentially surjective functors), we mean these to include a choice of witnesses for the existence (chosen limits, chosen lifts-up-to-isomorphism, and so on). We do not however ask morphisms to preserve these choices, unless explicitly specified.
Assuming the Axiom of Choice, this is of course inconsequential. Our main motivation is for uniformity with internal category theory, where the chosen-structure version is almost always advantageous since it presents structured categories as essentially algebraic notions.
With this in mind, the main classes of logically-structured categories we will use throughout are:
Definition 1. A category is:
cartesian (aka left exact, lex, finite-limit, finitely complete) if it has all finite limits;
lextensive if it has finite limits, and finite coproducts, disjoint and stable under pullback;
regular if it has finite limits and image factorisations, and covers are pullback-stable (in the sense of 4 below);
exact if it has finite limits, and pullback-stable effective quotients of equivalence relations;
a pretopos if it is lextensive and exact;
an elementary topos with NNO, or just topos, if it is regular and additionally has power-objects and a natural numbers object2.
(A few more notions — locally finitely presentable categories, locoses, arithmetic universes — we will recall as and when we need them.)
Reading these according to , each kind of category comes equipped with operations providing the assumed categorical structure. So there are always two levels at which a functor \(F : \mathcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) between such categories may preserve the logical structure: weakly (the default sense), in that limits (colimits, power-objects, etc) retain their universal property under \(F\), or equivalently that the canonical comparison maps \(F(\varprojlim_i X_i) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \varprojlim_i FX_i\) are isomorphisms; or strictly, in that the functor commutes on the nose with the structure operations: \(F(\varprojlim_i X_i) = \varprojlim_i FX_i\).
Definition 2. A functor \(F : \mathcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) between cartesian categories (resp. regular categories, toposes, etc.) is cartesian (resp. regular, logical, etc.)if it (weakly) preserves the assumed structure, and strictly cartesian (resp. strictly regular, etc.)if it preserves the chosen structure on the nose.
We will often have to deal with the interplay of weakly and strictly structure-preseving functors, along with \(2\)-categorical issues and sometimes size issues; so we systematically distinguish several (\(2\)-)categories of these logically-structured categories.
Definition 3. We write:
\(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), \(\mathcalit{R{\mkern-2mu}eg}\@ifnotmtarg{}{_{}}\), and \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\) respectively for the (\(1\)-)category of small regular categories and strictly regular functors; the \(2\)-category of small regular categories, regular functors, and natural transformations; the \(2\)-category of locally small regular categories, regular functors, and natural transformations;
\(\mathrm{Cat}_\mathit{str}\@ifnotmtarg{}{()}\), \(\mathcalit{C{\mkern-2mu}at}\@ifnotmtarg{}{_{}}\) and \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\) for the corresponding \(1\)- and \(2\)-categories of categories (in this case, there is no difference between strict and non-strict functors, but \(\mathrm{Cat}_\mathit{str}\@ifnotmtarg{}{()}\) still differs from \(\mathcalit{C{\mkern-2mu}at}\@ifnotmtarg{}{_{}}\) in omitting \(2\)-cells);
\(\mathcal{\uppercase{LE{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{LE{\mkern-1mu}XT}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{E{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}\), and so on for the corresponding \(2\)-categories of cartesian, lextensive, exact, etc. categories, the corresponding structure-preserving functors, and natural transformations (for these, we never need the strict versions);
\(\strLog\), \(\@ifnotmtarg{}{\text{-}}\mathcalit{L{\mkern-2mu}og}\) and \(\LOG\) for the corresponding \(1\)- and \(2\)-categories of toposes, logical functors (strict for \(\strLog\)), and natural isomorphisms (omitted in \(\strLog\)).
Viewing a small regular category (or topos, etc.)as an object of \(\mathcalit{R{\mkern-2mu}eg}\@ifnotmtarg{}{_{}}\) (resp. \(\@ifnotmtarg{}{\text{-}}\mathcalit{L{\mkern-2mu}og}\), etc.), its specific choice of logical structure is inessential, since even isomorphisms in \(\mathcalit{R{\mkern-2mu}eg}\@ifnotmtarg{}{_{}}\) need not preserve this. Viewing it as an object of \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), however, the choice matters: different choices of regular structure on a category may yield non-isomorphic objects of \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\). We will therefore speak of strict regular categories (toposes, etc.) to emphasise when we view them as objects of the strict category.
Caveat 1. The strict notions are rather sensitively presentation-dependent: for instance, common alternative definitions of toposes such as “regular + power-objects” and “cartesian closed + subobject classifier” yield equivalent \(2\)-categories \(\LOG\), but inequivalent \(1\)-categories \(\strLog\).
For this reason, among others, the strict categories \(\strLog\), \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), and so on are generally thought of as auxiliary technical devices, with the \(2\)-categories \(\LOG\), \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\), etc. as the true objects of study.
Definition 4. Following [4], we call a map a cover if it does not factor through any proper subobject of its target. We denote covers diagrammatically by \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} B\). Say a cover is stable if every pullback of it is a cover.
A (stable) image factorisation of a map is a factorisation as a (stable) cover followed by a monomorphism.
Proposition 1 ([4]). In a cartesian category, covers are precisely the extremal epimorphisms. In a regular category, covers are precisely the regular epimorphisms. 0◻
Definition 5. An object \(P \in \mathcal{C}\) is cover-projective (resp. regular-) if maps from \(P\) lift along covers (resp. regular epimorphisms): \[\begin{tikzcd} & Y \ar[d,cover,"e"] \\ P \ar[ur,dashed,"\exists\, g"] \ar[r,"f"] & X \end{tikzcd}\]
By projective we always mean cover-projective, or equivalently regular-, since we consider projectivity only in regular categories. In a topos, all epis are regular, so ordinary projectivity (i.e. with respect to epimorphisms) also coincides. Lastly, we note the easy characterisation:
Proposition 1. In a regular category, an object is projective just if every cover of it has a splitting. 0◻
We will make frequent essential use of comma and iso-comma categories:
Definition 6. Given categories and functors \(\mathcal{C}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_0}; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_1}; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \mathcal{C}_1\), the comma category \(({F_1} \mathbin{\downarrow} {F_0})\) has as objects triples \((c_1, c_0, \varphi)\), where \(c_i \in \mathcal{C}_i\) and \(\varphi : F_1 c_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} F_0 c_0\), and maps \((c_1, c_0, \varphi) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} (d_1,d_0,\psi)\) are maps \(f_i : c_i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} d_i\) such that \(F_0 f_0 \varphi = \psi F_1 f_1\). The iso-comma \(({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) is similar, but restricting to objects \((c_1, c_0, \varphi)\) in which \(\varphi\) is an isomorphism. In both cases, here shown for the comma category, we have projections \(P_i: ({F_1} \mathbin{\downarrow} {F_0}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\) and a natural transformation (isomorphism in the iso-comma case) \(\alpha:F_1P_1\Rightarrow F_0P_0\) whose component at \((c_1, c_0, \varphi)\) is \(\varphi\): \[\begin{tikzcd} ({F_1} \mathbin{\downarrow} {F_0}) \ar[d,"P_0"] \ar[r,"P_1"] & \mathcal{C}_1 \ar[d,"F_1"] \ar[dl,"\alpha"',Rightarrow, shorten=6mm] \\ \mathcal{C}_0 \ar[r,"F_0"] & \mathcal{D}. \end{tikzcd}\]
When either functor is an identity, we will write e.g. \(({\mathcal{D}} \mathbin{\downarrow} {F})\) for \(({\mathrm{id}_\mathcal{D}} \mathbin{\downarrow} {F})\).
Proposition 1. Fix \(\mathcal{C}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_0}; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_1}; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \mathcal{C}_1\) as above.
(1) If \(\mathcal{C}_0\), \(\mathcal{C}_1\), \(\mathcal{D}\), and \(F_1\) are all regular, and \(F_0\) cartesian, then \(({F_1} \mathbin{\downarrow} {F_0})\) is regular, and its projection functors \(P_i : ({F_1} \mathbin{\downarrow} {F_0}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\) are strictly regular. Moreover, a map \((f,f')\) in \(({F_1} \mathbin{\downarrow} {F_0})\) is a cover if both of its components \(f\), \(f'\) are.
(2) If \(\mathcal{C}_0\), \(\mathcal{C}_1\), and \(\mathcal{D}\) are regular (resp. toposes), and both \(F_i\) are regular (resp. logical), then \(({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) is regular (a topos), and its projection functors are strictly regular (strictly logical).
Proof. All essentially straightforward. On the object components, logical structure is given componentwise (as it must be, for the projections to preserve it strictly). On the map component, it amounts mostly to the fact that all the regular structure is automatically (covariantly) functorial, and power-objects are functorial in isomorphisms; in case \(F_0\) is just cartesian, the map component of the image factorisation does not quite fit this pattern, but is determined uniquely by orthogonality between covers and monos. ◻
Proposition 1. For \(\mathcal{C}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_0}; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_1}; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \mathcal{C}_1\) in \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\),
(1) a functor \(G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({F_1} \mathbin{\downarrow} {F_0})\) is regular, or strictly so, just if its object components \(P_i G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\) both are;
(2) for regular \(G_i : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\), natural transformations \(\gamma : F_1 G_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} F_0 G_0\) correspond bijectively to regular functors \(G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({F_1} \mathbin{\downarrow} {F_0})\) lifting \((G_1,G_0) : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_1 \times \mathcal{C}_0\) (related via \(\alpha G = \gamma\)).
\[\begin{tikzcd}[sep=small] & \mathcal{C}_1 \ar[dr,"F_1"] \ar[dd,"\gamma",Rightarrow,dashed,shorten=1.5ex] & &[-1em] &[1.5em] &[-1em] &[1.4em] { } \ar[dr,phantom,"="{sloped,near end}] &[-2.3em] &[-0.5em] \mathcal{C}_1 \ar[dr,"F_1"] \ar[dd,"\alpha",Rightarrow,shorten=1.5ex] & \\ \mathcal{X}\ar[dr,"G_0"'] \ar[ur,"G_1"] & & \mathcal{D} & { } \ar[r,squiggly,leftrightarrow] & { } & \mathcal{X}\ar[drrr,"G_0"',bend right=10] \ar[urrr,"G_1",bend left=10] \ar[rr,"G",dashed] & & ({F_1} \mathbin{\downarrow} {F_0})\mkern-15mu \ar[dr,"P_0"] \ar[ur,"P_1"'] & & \mathcal{D} \\ & \mathcal{C}_0 \ar[ur,"F_0"'] & & & & & { } \ar[ur,phantom,"="{sloped,near end}] & & \mathcal{C}_0 \ar[ur,"F_0"'] \end{tikzcd}\]
Similarly, \(({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) enjoys analogous properties with respect to natural isomorphisms, in \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\) and also \(\LOG\).
In \(2\)-categorical terms, these form (iso-)comma objects in \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\), \(\LOG\).
Proof. Part amounts to checking that for each object piece of logical structure on \(({F_1} \mathbin{\downarrow} {F_0})\) or \(({F_1} \mathbin{\downarrow_{\cong}} {F_0})\), the map component is uniquely determined given the object parts and commutativity with the corresponding structure maps. The latter two parts follow directly. ◻
Our final comma construction has something of a different character, and will turn out to have very important consequences:
Proposition 1 (Artin gluing, [4]). Let \(F : \mathcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) be a cartesian* functor between toposes. Then \(({\mathcal{D}} \mathbin{\downarrow} {F})\) is a topos, \(P_0 : ({\mathcal{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}\) is strictly logical, and \(P_1 : ({\mathcal{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) is strictly regular.*
Moreover, this is appropriately functorial: pseudo-commuting squares \(\varphi : JF' \cong FI\) with \(I\), \(J\) logical induce logical functors \(({J} \mathbin{\downarrow} {\varphi}) : ({\mathcal{D}'} \mathbin{\downarrow} {F'}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({\mathcal{D}} \mathbin{\downarrow} {F})\), and this respects identities and composition: \[\begin{tikzcd} \mathcal{C}' \ar[r,"F'"] \ar[d,"I"] & \mathcal{D}' \ar[d,"J"] \ar[dl,phantom,"\cong"{sloped}] \\ \mathcal{C}\ar[r,"F"] & \mathcal{D} \end{tikzcd} \qquad \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \qquad}; \draw[cd-arrow-style,zigzag] (a.south west) -- (a.south east);} \mkern-1mu} \quad \begin{tikzcd}[row sep=small] ({\mathcal{D}'} \mathbin{\downarrow} {F'}) \ar[dd,"({J} \mathbin{\downarrow} {\varphi})"] \ar[dr] \ar[drr,bend left=15] \\[-2ex] & \mathcal{C}' \ar[r] \ar[dd] & \mathcal{D}' \ar[dd] \\ ({\mathcal{D}} \mathbin{\downarrow} {F}) \ar[dr] \ar[drr,bend left=15] \\[-2ex] & \mathcal{C}\ar[r] & \mathcal{D}. \end{tikzcd}\]
Proof. The regular structure is component-wise as in 1; the NNO is also componentwise, with \(N_\mathcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} FN_\mathcal{C}\) induced by \(F0_\mathcal{C}\), \(FS_\mathcal{C}\); and power-objects are given by the pullback \[P\left( \begin{tikzcd}[ baseline={([yshift=-axis_height]\tikzcdmatrixname)}] D \ar[d,"p"] \\ FC \end{tikzcd} \right) = \left( \begin{tikzcd}[sep=small, baseline={([yshift=-axis_height]\tikzcdmatrixname)}] \bullet \ar[dd] \ar[rr] \ar[ddr,drpb] &[0.6em] &[-0.4em] {\subseteq}_{D} \ar[d,inj] \\ & & PD \times PD \ar[d,"\pi_1"] \\ F PC \ar[r,"\xi_C"] & PF C \ar[r,"p^*"] & PD \end{tikzcd}\right) \] where \(\xi_C\) is the canonical comparison map \(FPC \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} PFC\), corresponding to \(F({\in_C}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} FC \times F PC\). In the internal language, the pullback can be written as \(\HOLinterp[ a \mspace{2.5 mu plus 1mu minus 1mu}\mathord{:}\mspace{2.5 mu plus 1mu minus 1mu} FPC,\, b \mspace{2.5 mu plus 1mu minus 1mu}\mathord{:}\mspace{2.5 mu plus 1mu minus 1mu} PD \mathrel{\mid} b \subseteq \{ y \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}D \mathrel{\mid}p(b) \mathrel{\raisebox{0.065ex}{\mathrm{\small \lowercase{\textit{F}}}}\mkern-0.5mu{\in}} a \} ]\).
Verification of the functoriality is gruesome but routine. ◻
By essentially algebraic theories we mean, initially and broadly, that class of theories which correspond to cartesian categories, and whose categories of models in \(\mathrm{Set}\) are, accordingly, locally finitely presentable. There are several different syntactical characterisations of these, including the essentially algebraic theories of [5], the cartesian theories of [4], and the partial Horn theories of [6]. Of these, we use cartesian theories, as defined in [4], when we need a syntactic perspective.
Theorem 1 ([7], [4]). The following are equivalent, for a category \(\mathcal{M}\):
(a) \(\mathcal{M}\) is locally finitely presentable, i.e.it is cocomplete and has a small, full subcategory \(\mathcal{M}_{\mathrm{fp}}\) of finitely presented objects such that every object is a directed colimit of objects from \(\mathcal{M}_{\mathrm{fp}}\) [7].
(b) \(\mathcal{M}\simeq\mathcal{\uppercase{LE{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}(\mathrm{C},\mathrm{Set})\) for some small cartesian category \(\mathrm{C}\).
(c) \(\mathcal{M}\simeq\mathrm{Mod}\@ifnotmtarg{\mathrm{Set}}{_{\mathrm{Set}}}(\mathsf{T})\) for some cartesian theory \(\mathsf{T}\) of predicate logic.
(d) \(\mathcal{M}\simeq\mathrm{Mod}\@ifnotmtarg{\mathrm{Set}}{_{\mathrm{Set}}}(\mathbf{S})\) for some finite limit sketch \(\mathbf{S}\), in the sense of [4].
Furthermore:
(1) In condition , the cartesian category \(\mathrm{C}\) is equivalent to \(\mathcal{M}_{\mathrm{fp}}^\mathrm{op}\); indeed, this underlies a biequivalence \(\mathcal{\uppercase{LFP}}\@ifnotmtarg{}{_{}}\simeq_2 \mathcalit{L{\mkern-2mu}ex}\@ifnotmtarg{}{_{}}^\mathrm{op}\) (“Gabriel–Ulmer duality”, [8]).
(2) If \(\mathcal{M}\simeq\mathrm{Mod}\@ifnotmtarg{\mathrm{Set}}{_{\mathrm{Set}}}(\mathsf{T})\) for some finitely axiomatised cartesian theory as in , then it is equivalent to \(\mathrm{Mod}\@ifnotmtarg{\mathrm{Set}}{_{\mathrm{Set}}}(\mathbf{S})\) for some finite finite limit sketch \(\mathbf{S}\) as in , and vice versa.
(3) Given a cartesian theory \(\mathsf{T}\) as in , a cartesian category as in is given by the syntactic category \(\mathrm{C}_{\mathsf{T}}\) of \(\mathsf{T}\), with objects cartesian formulas-in-context \([ \vec{x} \mathrel{\mid}\varphi(\vec{x}) ]\) of \(\mathsf{T}\). 0◻
Definition 7. By an essentially algebraic theory \(\mathsf{T}\), we mean agnostically a locally finitely presentable category \(\mathcal{M}_\mathsf{T}\), or a small cartesian category \(\mathrm{C}_{\mathsf{T}}\), justified by above. We say \(\mathsf{T}\) is finitely presented if it admits a presentation by a finite cartesian theory, or equivalently a finite finite limit sketch (sic), in light of above.
A model of \(\mathsf{T}\) in a cartesian category \(\mathcal{E}\) is just a cartesian functor \(M : \mathrm{C}_{\mathsf{T}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) (equivalently, a model of in \(\mathcal{E}\) the theory or sketch presenting \(\mathsf{T}\)); we denote the category of these by \(\mathrm{Mod}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}(\mathsf{T})\).
We call objects of \(\mathrm{C}_{\mathsf{T}}\) types of \(\mathsf{T}\), and their interpretations \(\EATinterp[X][M] \in \mathcal{E}\) under a model \(M \in \mathrm{Mod}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}(\mathsf{T})\) the types of \(M\).
We will typically present essentially algebraic theories by describing their category of models, in such a way that they are evidently models of a suitable cartesian theory. In particular, the \(1\)-categories of strict logically-structured categories defined above are all essentially-algebraic:
Proposition 1. \(\mathrm{Cat}_\mathit{str}\@ifnotmtarg{}{()}\), \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), \(\strLog\) are each the category of models of some essentially algebraic theory.
Proof. The theory of categories is standard, and easy to write down. It can then be extended by operations for the further assumed structure, and operations/axioms enforcing their defining properties.
The one subtlety is that the definitions of covers and power-objects quantify over monomorphisms, which are not in general an essentially-algebraic notion. Given finite limits, though, they can be defined essentially-algebraically as maps whose kernel pair projections are isomorphisms.
It is then clear that the models of these theories are categories, regular categories, and toposes respectively, and their homomorphisms precisely the strictly structure-preserving functors. ◻
We exploit several consequences of essential-algebraicity. Most ubiquitously, it allows us to uniformly internalise all these notions.
Definition 8. Let \(\mathcal{E}\) be a cartesian category. An internal category (regular category, topos, etc.)in \(\mathcal{E}\) means a model of the cartesian theory of categories (regular categories, toposes, etc.)in \(\mathcal{E}\). Maps of these can be viewed as functors (strictly regular, logical, etc.); we denote the resulting \(1\)-categories by \(\mathrm{Cat}_\mathit{str}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\), \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\), \(\strLog[][\mathcal{E}]\), etc.
With the evident notion of natural transformation, we denote the \(2\)-category of internal categories by \(\mathrm{Cat}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\). (One may also define \(\mathrm{Reg}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\), \(\intLog[][\mathcal{E}]\), with suitable notions of (weakly) regular/logical internal functors; but the definitions are a little involved and we never need them.)
Our other main uses of essential-algebraicity are to obtain initial logically-structured categories (and later internalise them, in 3.3), and to justify appeals to compactness. Categorically, this latter amounts to understanding how initial models interact with filtered colimits of theories — in our application, \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) as the colimit of its finite-rank fragments \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\) (all in their categorical forms, toposes and \(r\)-toposes).
In fact it turns out more convenient to give the general compactness result dually, in terms of categories of models:
Lemma 1. Let \(\mathcal{I}\) be a filtered category, \((\mathcal{M}_i)_{i \in \mathcal{I}^\mathrm{op}}\) a diagram (strict or pseudo) of lfp categories and finitary functors, and \(M_\infty\) some (bi-)limit for it in both \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\) and \(\mathcal{\uppercase{LFP}}\@ifnotmtarg{}{_{}}\). 3 Write the functors of the diagram and cone as \(U_i : \mathcal{M}_j \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{M}_i\), for each \(i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} j\) in \(\mathcal{I}\), and also for \(j = \infty\); and write \(A_i\) for the initial object of \(\mathcal{M}_i\).
Then for each \(i\), \(U_i A_\infty \cong\varinjlim_{j \in i/\mathcal{I}} U_i A_j\).
Proof. For each \(i\), set \(A_{\infty,i} \coloneq \varinjlim_{j \in i/\mathcal{I}} U_i A_j\). Functors \(j/\mathcal{I} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} i/\mathcal{I}\) between coslices of a filtered category are final; so we have isomorphisms \(U_i A_{\infty,j} \cong A_{\infty,i}\) for each \(i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} j\) making the objects \(A_{\infty,i}\) into a coherent family in the diagram \((\mathcal{M}_i)_{i \in \mathcal{I}^\mathrm{op}}\). They thus lift to some object \(A_{\infty,\infty} \in \mathcal{M}_\infty\), with coherent isomorphisms \(U_i A_{\infty,\infty} \cong A_{\infty,i}\) for each \(i\).
Now it is direct to check that \(A_{\infty,\infty}\) is initial in \(\mathcal{M}_{\infty}\). Given any \(X \in \mathcal{M}_\infty\), the maps \(A_j \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U_j X\) assemble into maps \(A_{\infty,i} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U_i X\) naturally in \(i\), and hence into a map \(A_{\infty,\infty} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) in \(\mathcal{M}_\infty\). Uniqueness is similar. ◻
Gabriel–Ulmer duality tells us we can equivalently view this situation as a colimit of theories, \(\mathsf{T}_\infty = \varinjlim_{i \in \mathcal{I}} \mathsf{T}_i\). In applications, however, the limit condition on categories of models is easier to verify.
Proposition 1. [4] Let \(\mathsf{T}\) be an essentially algebraic theory, and \(X \in \mathrm{C}_{\mathsf{T}}\) some type of \(\mathsf{T}\). Then for any filtered colimit of models \(M = \varinjlim_{i} M_i\), we have \(\EATinterp[X][M] \cong\varinjlim_i \EATinterp[X][M_i]\).
Proof. This is the standard fact that filtered colimits in \(\mathcal{\uppercase{LE{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}(\mathrm{C}_{\mathsf{T}},\mathrm{Set})\) are computed pointwise: \(\mathcal{\uppercase{LE{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}(\mathrm{C}_{\mathsf{T}},\mathrm{Set})\) is closed under filtered colimits in \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}(\mathrm{C}_{\mathsf{T}},\mathrm{Set})\) since filtered colimits commute with finite limits. ◻
Corollary 1. Suppose \(\mathrm{C}_\infty = \varinjlim_{i \in \mathcal{I}} \mathrm{C}_i\) is a filtered colimit in \(\mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), and \((X_i \in \mathrm{C}_i)_{i \in I \cup \{\infty\}}\) a matching family of objects in the diagram and colimit. Then we have a filtered colimit of sets \[\textstyle \{ Y \in \mathrm{C}_\infty,\, e : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} X_\infty \} = \varinjlim_{i \in \mathcal{I}} \{ Y \in \mathrm{C}_i,\, e : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} X_i \}. \qedhere\]
Various constructions of the free topos exist in the literature. All agree up to equivalence, as they are bi-initial in the \(2\)-category \(\LOG\) of toposes and logical functors; this is the defining property of the free topos [4]. (An object \(\mathcal{C}\) of a \(2\)-category \(\mathcal{K}\) is bi-initial if each hom-category \(\mathcal{K}(\mathcal{C},\mathcal{D})\) is contractible: there is an essentially unique map from \(\mathcal{C}\) to each object of \(\mathcal{K}\).)
Most developments characterise it moreover up to isomorphism, as a strictly initial object in some \(1\)-category of toposes and strictly logical functors, or of higher-order theories and interpretations (e.g.[2]). As with 1, however, it is worth noting that this is somewhat fragile: different “equivalent” definitions of toposes yield equivalent but not isomorphic constructions of the free topos.
We present here one possible construction. This is not essential — we could work throughout with an off-the-shelf version, using just the \(2\)-categorical universal property — but it forms a useful warmup for the development of free ranked and internal toposes below.
Definition 9. We denote by \(\freeTop\) the free strict topos: that is, the initial object of \(\strLog\) (which exists since strict toposes are an essentially algebraic notion, 1).
The desired \(2\)-categorical universal property follows purely formally with the aid of the iso-comma construction, 1.
Proposition 1. The free strict topos \(\freeTop\) is moreover bi-initial in \(\LOG\).
Proof. We need to show that each hom-category \(\LOG(\freeTop, \mathcal{E})\) is contractible.
For inhabitedness, take some choice of topos structure on \(\mathcal{E}\); then the substructure generated by its operations is a small (indeed, countable) subtopos \(\mathrm{E}\subseteq \mathcal{E}\), into which \(\freeTop\) maps by its initiality in \(\strLog\).
It remains to show that for any logical \(F_0, F_1 : \freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\), there is a unique natural isomorphism \(F_0 \cong F_1\). But by 1, these correspond precisely to strictly logical functors \(\freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) over \((F_1,F_0) : \freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\times \mathcal{E}\), unique existence of which is immediate by strict initiality of \(\freeTop[r]\). \[\begin{tikzcd}[row sep=normal,column sep=large, baseline=(\tikzcdmatrixname-2-1.base)] & ({F_1} \mathbin{\downarrow_{\cong}} {F_0}) \ar[d,"{(P_1,P_0)}"] \ar[r] & \mathcal{E}^{\cong} \ar[d,"{(s,t)}"] \\ \freeTop \ar[ur,dashed,bend left=10] \ar[r,"\Delta_{\freeTop}"] & \freeTop \times \freeTop \ar[r,"F_1 \times F_0"] & \mathcal{E}\times \mathcal{E} \end{tikzcd} \qedhere\] ◻
Remark 1. The rôle of the iso-comma topos here, and specifically the fact that topos structure is closed only under iso-comma categories, illustrates why the \(2\)-cells of \(\LOG\) are taken as just natural isomorphisms: with non-invertible transformations included, \(\freeTop\) would not be bi-initial.
For regular or cartesian categories (say), since comma categories are available, the analogous argument gives a bi-initial object with respect to all natural transformations.
At base this comes down to the fact that cartesian/regular structure is all covariantly functorial, whereas toposes include both co- and contra-variant structure.
We can now give Freyd’s classic categorical proof of the existence property for higher-order logic ([9], [10]).
Proposition 1 (Freyd gluing). The terminal object of \(\freeTop\) is projective.
Proof. Consider the Artin gluing category \(({\mathrm{Set}} \mathbin{\downarrow} {\Gamma})\) of the global sections functor \(\Gamma : \freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Set}\), with projection functors \(P_0 : ({\mathrm{Set}} \mathbin{\downarrow} {\Gamma}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop\), \(P_1 : ({\mathrm{Set}} \mathbin{\downarrow} {\Gamma}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Set}\). This is a topos, by 1; so initiality gives a strictly logical interpretation functor \(\HOLinterp : \freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({\mathrm{Set}} \mathbin{\downarrow} {\Gamma})\), and since \(P_0\) is strictly logical, \(P_0 \HOLinterp = \mathrm{id}_{\freeTop}\). Write \(\HOLinterp_1\) for the composite \(P_1 \HOLinterp : \freeTop \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Set}\), and \(\rho\) for the natural transformation \(\HOLinterp_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \Gamma P_0 \HOLinterp = \Gamma\). \[\begin{tikzcd} & ({\mathrm{Set}} \mathbin{\downarrow} {\Gamma}) \ar[d,"P_0"] \ar[r,"P_1"] & \mathrm{Set}\ar[d,"\mathrm{id}"] \ar[dl,Rightarrow,"\rho"',shorten=6mm] \\ \freeTop[r] \ar[ur,dashed,"\HOLinterp"] \ar[r,"\mathrm{id}"] & \freeTop[r] \ar[r,"\Gamma"] & \mathrm{Set} \end{tikzcd}\]
Now for any cover \(e : A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1\) in \(\freeTop\), its interpretation \(\HOLinterp[e]\) is a cover \((\HOLinterp[e]_1,e):(\HOLinterp[A]_1,A,\rho_A) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} (1,1,\rho_1)\). \[\begin{tikzcd} A \ar[d,->>,"e"'] & & \HOLinterp[A]_1 \ar[r,"\rho_A"] \ar[d,->>,"{\HOLinterp[e]_1}"'] & \Gamma(A) \ar[d,"\Gamma(e)"] \\ 1 & & \mathllap{1 = {}}\HOLinterp[1]_1 \ar[r,"\rho_1"] & \Gamma(1) \mathrlap{{}\cong 1} \end{tikzcd}\] Then \(\HOLinterp[e]_1\) is a cover, by 1; that is, \(\HOLinterp[A]_1\) inhabited. So taking some \(x \in \HOLinterp[A]_1\), \(\rho_A(x)\) gives a global section of \(A\) as required. ◻
Definition 10. For \(r \in \mathbb{N}\cup \{ \infty \}\), an \(r\)-ranking on a category \(\mathcal{E}\) is a sequence of distinguished classes of objects \(\mathcal{E}_0 \subseteq \mathcal{E}_1 \subseteq \cdots \subseteq \mathcal{E}_i \cdots \subseteq \mathop{\mathrm{ob}}\mathcal{E}\), for \(0 \leq i < r\).
A functor \(f : \mathcal{E} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{F}\) of \(r\)-ranked categories strictly (resp. weakly) preserves rank if for each \(x \in \mathcal{E}_i\), \(fx\) lies in \(\mathcal{F}_i\) (resp. isomorphic to some object of \(\mathcal{F}_i\)). As usual we take preserves rank, unqualified, to mean the weak version.
We will view the classes \(\mathcal{E}_i\) as full subcategories of \(\mathcal{E}\), and say objects have rank \(\leq i\) if they lie in \(\mathcal{E}_i\). Note rank here is always cumulative — we never distinguish the precise minimal rank of objects — and is not assumed invariant under isomorphism.
For the remainder of the paper, \(r\) will by default range over \(\mathbb{N}\cup \{\infty\}\).
Definition 11. An \(r\)-ranked topos is a regular category \(\mathcal{E}\) with NNO, \(r\)-ranked such that:
each \(\mathcal{E}_i\) is a regular subcategory of \(\mathcal{E}\) and contains the NNO;
for each \(0 \leq i < r-1\), each object of \(\mathcal{E}_i\) has a power-object in \(\mathcal{E}\), lying in \(\mathcal{E}_{i+1}\).
We will often write just \(r\)-topos; of course this should not be confused with the more established higher-categorical senses of \(n\)-topos. A functor of \(r\)-toposes is (strictly) \(r\)-logical if it is (strictly) regular and rank-preserving, and (strictly) preserves the NNO and the assumed power-objects. More rarely, we will call a functor from an \(r\)-topos just logical if it preserves the regular structure, NNO, and assumed power-objects, but is not necessarily rank-preserving; we will note clearly when we mean this!
Following the convention of 3, we write \(\strLog[r]\), \(\@ifnotmtarg{r}{r\text{-}}\mathcalit{L{\mkern-2mu}og}\), \(\LOG[r]\) for the \(1\)- and \(2\)-categories of small/locally small \(r\)-toposes, \(r\)-logical functors (strict for \(\strLog[r]\)), and natural isomorphisms (omitted in \(\strLog[r]\)).
As usual, we say strict \(r\)-topos to emphasise considering a small \(r\)-topos as an object of \(\strLog[r]\). Note however that even then, the chosen regular structure and power objects on the rank subcategories \(\mathcal{E}_i\) are not assumed strictly preserved by the inclusions between ranks or into \(\mathcal{E}\).
Remark 1. One could strengthen the definition of \(r\)-toposes to assume each rank is not just regular but in fact an arithmetic universe (22). For further development of ranked toposes as a logical setting in their own right, that would probably be more natural. In the present article, however, there would be little benefit, and it would substantially complicate the construction of internal concrete \(r\)-toposes via ranked universes (4.1), We return to this point in 1 below.
It is easy to check that \(r\)-toposes are essentially algebraic, along similar lines to 1:
Proposition 1.
For each \(r\), \(r\)-ranked categories and strictly rank-preserving functors are the models and homomorphisms of an essentially algebraic theory.
For each \(r\), strict \(r\)-toposes and strict \(r\)-logical functors are the models and homomorphisms of an essentially algebraic theory \(\mathsf{T}_r\).
For \(r \in \mathbb{N}\), this theory is finitely presented.
The evident forgetful functors \(\strLog[0] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \strLog[1] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \cdots \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \strLog[\infty]\) correspond to theory extensions \(\mathsf{T}_r \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} \mathsf{T}_s\), and so are finitary functors of locally finitely presentable categories.
This exhibits \(\strLog[\infty]\) as a (strict \(2\)-)limit of the tower of categories \(\strLog[r]\), in both \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\) and \(\mathcal{\uppercase{LFP}}\@ifnotmtarg{}{_{}}\) (equivalently, exhibits the theory of \(\infty\)-ranked toposes as the colimit of the theories of \(r\)-toposes). 0◻
Definition 12. Write \(\freeTop[r]\) for the free (strict) \(r\)-topos, i.e. the (strictly) initial object of \(\strLog[r]\), for each \(r \in \mathbb{N}\cup \{\infty \}\).
We will omit “strict” and call \(\freeTop[r]\) just the free \(r\)-topos, justified by 1 below.
Proposition 1. \(\freeTop[\infty] \cong\varinjlim_{r \in \mathbb{N}} \freeTop[r]\), as a strict filtered colimit of categories.
Proof. Direct by 1, since as noted in 1([item:inf-topos-eat-as-colimit]), \(\strLog[\infty] = \varprojlim_{r \in \mathbb{N}} \strLog[r]\) both in \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\) and \(\mathcal{\uppercase{LFP}}\@ifnotmtarg{}{_{}}\). ◻
Bi-initiality of the free strict \(r\)-topos in \(\LOG[r]\) will follow purely formally from its \(1\)-initiality together with a careful construction of iso-comma \(r\)-toposes, just as we showed for ordinary toposes in 1.3.
Proposition 1. Suppose \(\mathcal{C}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_0}; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle F_1}; \draw[cd-arrow-style,->] (a.south east) -- (a.south west);} \mkern-1mu} \mathcal{C}_1\) are \(r\)-toposes and logical functors (not necessarily rank-preserving). Then:
(1) \(({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) is an \(r\)-topos, where \((c_1,c_0,\varphi)\) is taken to have rank \(\leq i\) just if both \(c_0\) and \(c_1\) do;
(2) the projection functors \(P_i : ({F_1} \mathbin{\downarrow_{\cong}} {F_0}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\) are strictly \(r\)-logical;
(3) a functor \(G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({F_1} \mathbin{\downarrow_{\cong}} {F_0})\) is \(r\)-logical (resp. strictly \(r\)-logical, rank-preserving) if its projections \(P_i G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\) both are;
(4) for \(r\)-logical \(G_i : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_i\), natural transformations \(\gamma : F_1 G_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} F_0 G_0\) correspond bijectively to \(r\)-logical functors \(G : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({F_1} \mathbin{\downarrow} {F_0})\) lifting \((G_1,G_0) : \mathcal{X} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}_1 \times \mathcal{C}_0\).
Proposition 1. For each \(r\), the free strict \(r\)-topos \(\freeTop[r]\) is moreover bi-initial in \(\LOG[r]\).
Proof. Purely formal with the aid of the iso-comma construction, exactly as in the ordinary topos case, 1. ◻
Proposition 1. Any logical functor out of the free \(r\)-topos \(\freeTop[r]\) preserves rank (in the default, weak sense).
Proof. This too follows formally from the iso-comma construction. Given \(F : \freeTop[r] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) logical, consider the iso-comma \(r\)-topos \(({F} \mathbin{\downarrow_{\cong}} {\mathcal{E}})\). Initiality gives a section \(S\) of the projection \(P_1 : ({F} \mathbin{\downarrow_{\cong}} {\mathcal{E}}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop[r]\); the composite \(P_0 S : \freeTop[r] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) is then a strictly rank-preserving functor naturally isomorphic to \(F\), so witnesses that \(F\) preserves rank. \[\begin{tikzcd}[/tikz/baseline=(\tikzcdmatrixname-2-1.base)] & ({F} \mathbin{\downarrow_{\cong}} {\mathcal{E}}) \ar[d,"P_1"] \ar[r,"P_0"] & \mathcal{E}\ar[d,"\mathrm{id}_\mathcal{E}"] \ar[dl,phantom,"\cong"{sloped}] \\ \freeTop[r] \ar[r,"\mathrm{id}"] \ar[ur,"S",dashed] & \freeTop[r] \ar[r,"F"] & \mathcal{E}. \end{tikzcd} \qedhere\] ◻
Our next goal is showing that the free \(\infty\)-ranked topos \(\freeTop[\infty]\) is equivalent to the free ordinary topos \(\freeTop\). The guiding idea is that the categorical constructors are the same: the ranks just come along for the ride. The ranked version will contain “doppelgangers” of logical constructions taken at different ranks; but since all the assumed operations are determined by universal properties, such doppelgangers will be canonically isomorphic, so will not change the result, up to equivalence.
Definition 13. Given a topos \(\mathcal{E}\), we can view \(\mathcal{E}\) as an \(\infty\)-ranked topos \(\mathcal{E}^\mathrm{full}\) (the full ranking of \(\mathcal{E}\)), by setting \(\mathcal{E}^\mathrm{full}_i \mathrel{\vcenter{:}}=\mathop{\mathrm{ob}}\mathcal{E}\) for all \(i\). This forms the object part of an evident (strict) \(2\)-functor \(\LOG \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \LOG[\infty]\).
Definition 14. Given an \(\infty\)-ranked topos \(\mathcal{E}\), its ranked core is the category \({\mathcal{E}}^\mathrm{rk}\) with objects \(\mathop{\mathrm{ob}}{\mathcal{E}}^\mathrm{rk} \mathrel{\vcenter{:}}=\coprod_{i \in \mathbb{N}} \mathcal{E}_i\), and maps induced by the evident projection \(\mathop{\mathrm{ob}}{\mathcal{E}}^\mathrm{rk} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathop{\mathrm{ob}}\mathcal{E}\) to give a full and faithful functor \({\mathcal{E}}^\mathrm{rk} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\).
It is clear that \({\mathcal{E}}^\mathrm{rk}\) is a topos, with a natural \(\infty\)-ranking given by \(({\mathcal{E}}^\mathrm{rk})_i \mathrel{\vcenter{:}}=\coprod_{j \leq i} \mathcal{E}_j\), making \({\mathcal{E}}^\mathrm{rk} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) \(r\)-logical. Moreover, this forms the object part of an evident (strict) \(2\)-functor \(\LOG[\infty] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \LOG\).
Proposition 1. For any \(\infty\)-ranked topos \(\mathcal{E}\), if \({\mathcal{E}}^\mathrm{rk} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) is essentially surjective, then \(\mathcal{E}\) is a topos. 0◻
Proposition 1. The free \(\infty\)-ranked topos \(\freeTop[\infty]\) is a topos.
Proof. By 1, as initiality gives a section of \({(\freeTop[\infty])}^\mathrm{rk} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop[\infty]\). ◻
Proposition 1. The free \(\infty\)-ranked topos is equivalent to the free topos.
Proof. Consider the \(2\)-category of toposes equipped with an \(\infty\)-ranking; logical (not necessarily rank-preserving) functors; and natural isomorphisms. \(\freeTop\), with its full ranking, is certainly bi-initial there; but so is \(\freeTop[\infty]\), since it is a topos (1) and logical functors out of it are automatically rank-preserving (1). The proposition follows. ◻
The standard results on Artin/Freyd gluing of toposes given in [sec:cat-thy-prelims] [sec:free-topos-prelims] adapt directly to ranked toposes.
Proposition 1 (Artin gluing). Let \(F : \mathcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) be a cartesian, rank-preserving functor between \(r\)-toposes. Then equipping the comma category \(({\mathcal{D}} \mathbin{\downarrow} {F})\) with the levelwise* ranking (an object \(p : D \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} FC\) has rank \(\leq i\) just if \(C\), \(D\) both do), it carries an \(r\)-topos structure making the second projection functor \(P_0 : ({\mathcal{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{C}\) strictly \(r\)-logical, the first \(P_1 : ({\mathcal{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{D}\) strictly regular, and both strictly rank-preserving.*
Moreover, this is functorial as in 1: pseudo-commuting squares \(\varphi : JF' \cong FI\) with \(I\), \(J\) \(r\)-logical induce \(r\)-logical functors \(({J} \mathbin{\downarrow} {\varphi}) : ({\mathcal{D}'} \mathbin{\downarrow} {F'}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({\mathcal{D}} \mathbin{\downarrow} {F})\), respecting identities and composition.
Proof. The regular structure (total and rank-wise) is furnished by 1; similarly, the NNO and power-objects are constructed just as in the topos case (1), noting that as \(F\) preserves rank, the pullback there exists and has rank \(i+1\) if the objects \(C\), \(D\) have rank \(i\). Functoriality once again is lengthy but routine. ◻
Proposition 1 (Freyd gluing). The terminal object of \({\freeTop[r]}\) is projective.
Proof. Almost word-for-word as in 1, endowing \(\mathrm{Set}\) with the full ranking in order to make the global sections functor rank-preserving and apply 1. ◻
The endgame of the main result makes essential use of internal \(r\)-toposes in the free topos. To cleanly pass between external and internal categories, we view them both in the more general setting of indexed categories. A good introduction to the theory of indexed categories can be found in [4]; for now, we briefly recall just the material we need:
Definition 15. Given a category \(\mathcal{E}\) (the base), an \(\mathcal{E}\)-indexed category \(\mathbfcal{C}\) is a pseudo-functor \(\mathbfcal{C}:\mathcal{E}^\mathrm{op} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\); that is, for each \(X \in \mathcal{E}\) a category \(\mathbfcal{C}_X\) (the fibre category over \(X\)), and for each \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) a reindexing functor \(f^* : \mathbfcal{C}_X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}_Y\), all functorial in \(\mathcal{E}\) up to coherent isomorphism.
An \(\mathcal{E}\)-indexed functor \(F : \mathbfcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}\) consists of functors \(F_X : \mathbfcal{C}_X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}_X\), commuting with reindexing up to coherent isomorphism. With a suitable notion of natural transformations, \(\mathcal{E}\)-indexed categories form a \(2\)-category which we denote \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{\mathcal{E}}{\mkern-3.5mu}}}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}\).
Remark 1. Indexed categories can alternatively be presented as fibred categories, essentially a reorganisation of the same data, whose theory is in some respects technically cleaner. Everything we do here with indexed categories can equivalently be read in fibred terms. A useful comparison of the two approaches is given in [11].
Examples 1.
For any \(\mathcal{E}\), \(\mathcal{C}\), the constant \(\mathcal{E}\)-indexing of \(\mathcal{C}\) has all fibres equal to \(\mathcal{C}\), and trivial reindexing.
For any \(\mathcal{C}\), the standard \(\mathrm{Set}\)-indexing of \(\mathcal{C}\) has fibres \(\mathcal{C}^X\) for \(X \in \mathrm{Set}\), with reindexing given by precomposition.
For cartesian \(\mathcal{E}\), the self-indexing of \(\mathcal{E}\) has fibres \(\mathcal{E}/X\), with reindexing given by pullback. When working in indexed categories over a base \(\mathcal{E}\), we will generally identify \(\mathcal{E}\) with its self-indexing.
Given \(\mathbfcal{C}\) indexed over \(\mathcal{E}\), and \(X \in \mathcal{E}\), the restriction of \(\mathbfcal{C}\) to \(\mathcal{E}/X\) is the \(\mathcal{E}/X\)-indexed category \(\mathbfcal{C}{\restriction_{X}}\) given by \((\mathbfcal{C}{\restriction_{X}})_{(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X)} \mathrel{\vcenter{:}}=\mathbfcal{C}_Y\), with evident reindexing. The restriction of the self-indexing of \(\mathcal{E}\) to \(\mathcal{E}/X\) is precisely the self-indexing of the slice \(\mathcal{E}/X\).
Definition 16. An indexed category \(\mathbfcal{C}\) over a base \(\mathcal{E}\) is regular (resp. a topos, etc.)if all its fibre categories \(\mathbfcal{C}_X\) are regular (resp. toposes), and for each \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) in \(\mathcal{E}\) the reindexing functor \(f^*:\mathbfcal{C}_X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}_Y\) is regular (resp. logical). An indexed functor \(F : \mathbfcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}\) is regular (logical, etc.)just if its fibre functors \(F_X\) all are.
For the next few items, fix an indexed category \(\mathbfcal{C}\) over a base \(\mathcal{E}\).
Definition 17 ([4], [11]). \(\mathbfcal{C}\) is called locally \(\mathcal{E}\)-small if for all objects \(A, B \in \mathbfcal{C}_X\), the presheaf \((\mathcal{E}/X)^\mathrm{op} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Set}\) sending \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) to \(\mathbfcal{C}_Y(f^*A,f^*B)\) is representable. That is, there is an object \(\chi : \mathbfcal{C}_{X}(A,B)_{\mathcal{E}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) in \(\mathcal{E}/X\) (their hom-object), with for each \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) a bijection \(\mathbfcal{C}_Y(f^* A,f^*B) \cong\mathcal{E}/X(Y,\mathbfcal{C}_{X}(A,B)_{\mathcal{E}})\), naturally in \(f\).
The universal map from \(A\) to \(B\) is the map \(u : \chi^*A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \chi^*B\) in \(\mathbfcal{C}_{\mathbfcal{C}_{X}(A,B)_{\mathcal{E}}}\) corresponding to \(\mathrm{id}_{{\mathbfcal{C}_{X}(A,B)_{\mathcal{E}}}}\).
Proposition 1.
When \(\mathbfcal{C}\) is locally small, its hom-objects assemble automatically into an indexed functor \(\mathbfcal{C}^\mathrm{op}\times \mathbfcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\). In particular, for each \(A \in \mathbfcal{C}_X\), there is an \(\mathcal{E}/X\)-indexed functor \(\mathbf{y}_{A} : \mathbfcal{C}{\restriction_{X}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}/X\), sending each \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\), \(B \in \mathbfcal{C}_Y\) to \(\mathbfcal{C}_{Y}(f^*A,B)_{\mathcal{E}}\).
If \(F : \mathbfcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}\) is an indexed functor, with \(\mathbfcal{C}\), \(\mathbfcal{D}\) locally small, then \(F\) acts on hom-objects, inducing maps \(F_{A,B} : \mathbfcal{C}_{X}(A,B)_{\mathcal{E}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}_{X}(FA,FB)_{\mathcal{E}}\), suitably naturally in \(X\), \(A\), \(B\).
Proof. By the Yoneda lemma, it suffices to give natural transformations between the presheaves that the objects \(\mathbfcal{C}_{X}(A,B)_{\mathcal{E}}\) were defined to represent. But this is direct in each case by unwinding the definitions. ◻
Definition 18. A map \(e \in \mathbfcal{C}_X\) is an indexed cover if for every \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\), the reindexing \(f^*e\) is a cover in \(\mathbfcal{C}_Y\).
Proposition 1. If \(\mathbfcal{C}\) is (indexed-)regular, then a map \(e \in \mathbfcal{C}_X\) is an indexed cover in \(\mathbfcal{C}\) just if it is a cover in \(\mathbfcal{C}_X\).
Proof. Indexed-regularity says reindexing is regular, so preserves covers. ◻
For the next few items, assume additionally that \(\mathcal{E}\) is regular.
Definition 19. An object \(P \in \mathbfcal{C}_X\) is indexed (cover-)projective if for each reindexing \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\), map \(k : f^*P \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\), and indexed cover \(e : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} A\) in \(\mathbfcal{C}_Y\), there is some cover \(g : Z \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} Y\) and a lift \(\hat{k}\) of \(g^*k\) along \(g^*e\): \[\begin{tikzcd}[row sep=small] & B \ar[dd,cover,"e"] & & & & g^*B \ar[dd,cover,"g^*e"] \\ & & { } \ar[r,squiggly,maps to] & { } \\ f^*P \ar[r,"k"] & A & & &g^*f^* P \ar[r,"g^*k"] \ar[uur,"\widehat{k}",dashed] & g^*A \end{tikzcd}\]
Examples 1.
In the standard \(\mathrm{Set}\)-indexing of an ordinary regular category \(\mathcal{C}\), an object \(A \in \mathcal{C}^X\) is indexed-projective just if each \(A_x\) is projective in \(\mathcal{C}\).
In the self-indexing of a topos \(\mathcal{E}\), an object \(A \in \mathcal{E}\simeq\mathcal{E}/1=\mathcal{E}_1\) is indexed-projective just if it is internally projective in \(\mathcal{E}\), in the topos-theoretic sense of [4].
Proof. The \(\mathrm{Set}\)-indexing example is straightforward. The correspondence with internal projectivity in toposes is essentially [12]. ◻
Proposition 1. The following are equivalent, for \(P \in \mathbfcal{C}_X\):
(1) \(P\) is indexed-projective.
(2) (When \(\mathbfcal{C}\) is regular.) Any cover of any reindexing of \(P\) splits on some cover of its base. That is, for each \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) and cover \(e : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} f^*P\), there is some cover \(g : Z \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} Y\) such that \(g^*e\) splits in \(\mathbfcal{C}_Z\).
(3) (When \(\mathbfcal{C}\) is locally small.) The indexed representable functor \(\mathbf{y}_{P} : \mathbfcal{C}{\restriction_{X}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}/X\) preserves covers. 0◻
Proof. \(\Leftrightarrow\) adapts easily from the ordinary case, 1.
\(\Rightarrow\) : Suppose \(\mathbf{y}_{P}\) preserves covers. Then for any reindexing \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\), and cover \(e : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} A\) and map \(k : f^* P \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\) in \(\mathbfcal{C}_Y\), a cover of \(Y\) on which \(k\) lifts to \(B\) is given by the following pullback: \[\begin{tikzcd} \bullet \ar[r,dashed,"\widehat{k}"] \ar[d,dashed,cover] \ar[dr,drpb] & \mathbfcal{C}_{Y}(f^*P,B)_{\mathcal{E}} \ar[d,cover,"(\mathbf{y}_{P})_f(e)"{description,pos=0.45}] \\ Y \ar[r,"k"] & \mathbfcal{C}_{Y}(f^*P,A)_{\mathcal{E}} \end{tikzcd}\]
\(\Rightarrow\) : Suppose \(P\) is indexed-projective. Given \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) and \(e : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} A\) in \(\mathbfcal{C}_Y\), consider the universal map from \(f^*P\) to \(A\) in \(\mathbfcal{C}_{\mathbfcal{C}_{Y}(f^*P,A)_{\mathcal{E}}}\), denoted \(u : \chi^*f^*P \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \chi^*A\) as in 17. We know \(u\) must lift to a map \(\widehat{u} : g^*\chi^*f^*X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} g^*\chi^*B\) on some cover \(g : Z \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}_{Y}(f^*P,A)_{\mathcal{E}}\); but that amounts exactly to a triangle of the following form \[\begin{tikzcd} & \mathbfcal{C}_{Y}(f^*P,B)_{\mathcal{E}} \ar[d,"(\mathbf{y}_{P})_f(e)" description] \\ Z \ar[r,cover,"g",dashed] \ar[ur,"\widehat{u}",dashed] & \mathbfcal{C}_{Y}(f^*P,A)_{\mathcal{E}}, \end{tikzcd}\] implying by right-cancellation that \((\mathbf{y}_{P})_f(e)\) is a cover as required. ◻
Definition 20 ([4], cf.[11]). An internal category \(\mathrm{C}\) in \(\mathcal{E}\) can be viewed as an \(\mathcal{E}\)-indexed category \(\left[ \mathrm{C} \right]\), its externalisation, with \(\mathop{\mathrm{ob}}\left[ \mathrm{C} \right]_X \mathrel{\vcenter{:}}=\mathcal{E}(X,\mathop{\mathrm{ob}}\mathrm{C})\), and so on.
An \(\mathcal{E}\)-indexed category is called \(\mathcal{E}\)-small if it is equivalent to the \(\mathcal{E}\)-externalisation of some internal category.
Proposition 1. An \(\mathcal{E}\)-small indexed category is locally \(\mathcal{E}\)-small.
Proof. It suffices to check for the externalisation of an internal category, which is direct: for \(A,B \in \mathop{\mathrm{ob}}\left[ \mathrm{C} \right]_X = \mathcal{E}(X,\mathop{\mathrm{ob}}\mathrm{C})\), their hom-object is the pullback of \(\mathop{\mathrm{mor}}\mathrm{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} (\mathop{\mathrm{ob}}\mathrm{C})^2\) along \((A,B) : X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} (\mathop{\mathrm{ob}}\mathrm{C})^2\). ◻
We will generally identify internal categories with their externalisations, justified by the following proposition:
Proposition 1 ([4], cf.[11]). The externalisation of internal categories forms a \(2\)-functor \(\mathrm{Cat}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{\mathcal{E}}{\mkern-3.5mu}}}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}\), which is \(2\)-fully-faithful, in that the maps on hom-categories \(\mathrm{Cat}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}(\mathrm{C},\mathrm{D}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{\mathcal{E}}{\mkern-3.5mu}}}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}(\left[ \mathrm{C} \right],\left[ \mathrm{D} \right])\) are equivalences. 0◻
Proposition 1. An internal category is regular (resp. a topos), viewed as an indexed category, just if it admits the structure of an internal regular category (topos).
Proof. Any model \(M\) in \(\mathcal{E}\) of any essentially algebraic theory \(\mathsf{T}\) induces by Yoneda a functor \(\mathcal{E}^\mathrm{op} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Mod}\@ifnotmtarg{}{_{}}(\mathsf{T})\); in particular, an internal regular category \(\mathrm{C}\) yields a functor \(\mathcal{E}^\mathrm{op} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{Reg}_\mathit{str}\@ifnotmtarg{}{()}\), whose underlying indexed category is just the externalisation of \(\mathrm{C}\).
Conversely, if an internal category \(\mathrm{C}\) is indexed-regular, then regular structure on \(\mathrm{C}\) can be chosen as the universal instances of the corresponding operations on the externalisation. For instance, the product operation \(\mathop{\mathrm{ob}}\mathrm{C}\times \mathop{\mathrm{ob}}\mathrm{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathop{\mathrm{ob}}\mathrm{C}\) arises as the product of the pair \(\pi_0\), \(\pi_1\) in \(\left[ \mathrm{C} \right]_{(\mathop{\mathrm{ob}}\mathrm{C}\times \mathop{\mathrm{ob}}\mathrm{C})}\).
The topos case is directly analogous. ◻
Definition 21. An indexed \(r\)-topos over \(\mathcal{E}\) is an \(\mathcal{E}\)-indexed category \(\mathbfcal{C}\) together with \(r\)-topos structure on each fibre, and such that all reindexing functors are \(r\)-logical.
Given an indexed \(r\)-topos \(\mathbfcal{C}\) over \(\mathcal{E}\), the indexed subcategory \(\mathbfcal{C}_i\) is defined by taking \((\mathbfcal{C}_i)_X \mathrel{\vcenter{:}}=(\mathbfcal{C}_X)_i \subseteq \mathbfcal{C}_X\) as expected; for the reindexing functor along \(f : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\), we know that \(f^* : \mathbfcal{C}_X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}_{Y}\) preserves rank (albeit weakly), so we may take some perturbation of it up to isomorphism which maps \((\mathbfcal{C}_X)_i\) strictly into \((\mathbfcal{C}_Y)_i\). There are evident full and faithful indexed functors \(\mathbfcal{C}_i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}\) and \(\mathbfcal{C}_j \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{C}_i\) as in the non-indexed case.
Most results and constructions of 2 now adapt more or less straightforwardly to indexed and internal versions, compatibly with externalisation.
Proposition 1. For any category \(\mathcal{E}\), \(\freeTop[r]\) with the constant* \(\mathcal{E}\)-indexing is (bi-)initial among \(\mathcal{E}\)-indexed \(r\)-toposes and \(r\)-logical functors. 0◻*
Proposition 1 (Indexed Artin gluing). Let \(F : \mathbfcal{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}\) be a cartesian, rank-preserving functor of indexed \(r\)-toposes over \(\mathcal{E}\). Then the indexed comma category \(({\mathbfcal{D}} \mathbin{\downarrow} {F})\) carries an \(r\)-topos structure, given fibrewise by the levelwise ranking as in 1.
Moreover, an \(r\)-logical functor \(H : \mathbfcal{D} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathbfcal{D}'\) induces an \(r\)-logical functor \(({\mathbfcal{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({\mathbfcal{D}'} \mathbin{\downarrow} {GF})\), strictly over \(\mathbfcal{C}\). 0◻
Proposition 1 (Internal Artin gluing). Let \(F : \mathrm{C} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{D}\) be a cartesian, rank-preserving functor of internal \(r\)-toposes, in a cartesian category \(\mathcal{E}\). Then the internal comma category \(({\mathrm{D}} \mathbin{\downarrow} {F})\) carries an internal \(r\)-topos structure, whose externalisation is precisely the indexed Artin gluing of 1; moreover, the first projection \(P_0 : ({\mathrm{D}} \mathbin{\downarrow} {F}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{C}\) is a strict map of internal \(r\)-toposes.
Proof. This amounts to checking that the \(r\)-topos structure on the comma category in 1 is all essentially-algebraically defined. ◻
Proposition 1.
(1) The externalisation of an internal ranked category (resp. \(r\)-topos) carries an indexed ranking (resp. \(r\)-topos structure).
(2) If \(\mathrm{C}\) is an internal ranked category in \(\mathcal{E}\) whose externalisation is an \(r\)-topos, then \(\mathrm{C}\) carries the structure of an internal \(r\)-topos.
Proof. Part is immediate by Yoneda, as in 1.
For part , regular structure on \(\mathrm{C}\) and the subcategories \(\mathrm{C}_{\leq i}\) follows by 1, along with regularity of the subcategory inclusions; and the maps \(P_i : \mathop{\mathrm{ob}}\mathrm{C}_i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathop{\mathrm{ob}}\mathrm{C}_{i+1}\) providing power-object structure may be constructed along the same lines as the proof of 1. ◻
We now turn to the question of internal free \(r\)-toposes: first their existence, and then a closer inspection to determine that (as expected) they can be constructed syntactically, and hence admit a form of Gödel-numbering.
An appropriate minimal categorical setting for syntactic constructions is provided by locoses and arithmetic universes, introduced by Joyal and developed by Maietti and others [13], [14]. We briefly recall their key points here; for a more thorough introduction, see [15].
Definition 22. A locos is a lextensive category with parametrised list objects.
An arithmetic universe (AU), or list-arithmetic pretopos, is a locos that is moreover exact; equivalently, a pretopos with parametrised list objects.
A (locos-/AU-)logical functor is a lextensive (resp. pretopos) functor preserving list objects.
We write \(\mathcal{\uppercase{LOC}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{AU}}\@ifnotmtarg{}{_{}}\) for the \(2\)-categories of locoses/AU’s, suitably logical functors, and natural transformations.
Joyal originally introduced arithmetic universes to give a categorical account of Gödel’s incompleteness theorems [13]. A key step is showing the structure of an AU suffices to construct a free internal AU — a categorical analogue of arithmetic’s ability to encode its own syntax. Analysing what that construction relies on leads to the generalisation:
Theorem 2 ([16]). Any finitely presented essentially algebraic theory has an initial internal model in any AU, and AU-logical functors preserve these.
Unfortunately, while the result is well-known in folklore, the only full presentation we are aware of is in the unpublished manuscript [16]; the result has never appeared in the published literature, as discussed in [17]. The nearest published results we are aware of are:
[6] gives a clean presentation of a syntax for essentially algebraic theories, sufficiently elementarily that (with some work) the whole presentation can be internalised in an arithmetic universe, via e.g. the type theory for them developed in [15].
[18] constructs the initial internal AU in an AU, and states the general theorem, but leaves part of the proof conjectural.
[19] gives the result for EATs presented by finite-product sketches.
[15] constructs several more initial internal categories with extra logical structure, heuristically demonstrating all the techniques needed for the general theorem.
The specific case we require is just:
Theorem 3. For each \(r \in \mathbb{N}\), any arithmetic universe \(\mathcal{E}\) has an initial internal strict \(r\)-topos, which we denote \(\freeTop[r][\mathcal{E}]\); and AU-logical functors preserve these.
Proof. By 2; or more concretely, by adapting the constructions of the initial internal AU from [18], [15]. ◻
We will make extensive use of these internal free \(r\)-toposes. However, for our endgame, we need to squeeze a bit more juice out of their construction. As described in the sketch, we will need that elements of the free \(r\)-topos admit Gödel-numbering — that is, are internally enumerable — and hence admit choice functions by taking minimal witnesses.
We therefore develop the basic theory of enumerable objects in locoses and arithmetic universes — their choice properties, and their appearance in initial algebraic structures. Most ideas involved appear in earlier work [13], [15], [18], but not quite in the forms we require.
Definition 23. A predicate in a locos 4 is a map \(N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} 2\). The realisation of a predicate \(p\) is the pullback along \(p\) of \(1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} 2\), a complemented subobject of \(N\). Write \(\operatorname{Pred}(\mathcal{E})\) for the category of predicates in \(\mathcal{E}\) and maps in \(\mathcal{E}\) between their realisations.
Call an object of \(\mathcal{E}\) strictly enumerable if it admits a complemented monomorphism to \(N\), or equivalently lies in the essential image of \(\operatorname{Pred}(\mathcal{E})\). More generally, call a map \(p : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\) in \(\mathcal{E}\) strictly enumerable if it is so as an object of the slice \(\mathcal{E}/A\).
When \(\mathcal{E}\) is regular, call an object of \(\mathcal{E}\) enumerable if it is covered by (i.e. admits a cover from) a strictly enumerable object; call a map enumerable if it is enumerable as an object of the slice.
Proposition 1. Strictly enumerable maps in any locos (resp. enumerable maps in a regular locos) are stable under pullback, closed under composition, and preserved by (regular) locos-logical functors.
Proof. Direct, using the standard encoding \(N^2 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} N\) for composition. ◻
Proposition 1. In a regular locos, any map from an enumerable object to an object with enumerable diagonal is enumerable. In particular, any map from an enumerable to a strictly enumerable object is enumerable.
Proof. For any \(f : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\), the graph factorisation \((\mathrm{id},f) : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} B \times A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\) exhibits \(f\) as a pullback of the diagonal \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A \times A\) followed by a pullback of \(B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} 1\); so if these are both enumerable, so is \(f\).
For the strictly enumerable case, note that any subobject of \(N\) inherits its decidable equality, so certainly has enumerable diagonal. ◻
That proposition, together with the next few results, amount to an analysis and generalisation of the construction of images in \(\operatorname{Pred}\mathcal{E}\) from [15].
Definition 24. Say a map has split image if it factors as a split epi followed by a mono.
Proposition 1. In any cartesian category,
(1) a split image is a stable image factorisation;
(2) any cover with split image is split;
(3) if \(f : B \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\) is covered by \(g : \bar{B} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A\) (i.e. \(g = ef\), with \(e\) a cover), and \(g\) has split image, then so does \(f\). 0◻
Proposition 1. Any enumerable map has split image.
Proof. Given a strictly enumerable object \(A = \AUinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N\mathrel{\mid}\alpha(x) = 1]\), a split image for \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} 1\) is given by the subobject of minimal representatives, \(\AUinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N\mathrel{\mid}\alpha(x) = 1 \land \bigwedge_{y < x} (\alpha(y) = 0) ]\).
The case for a general strictly enumerable map follows by passing to the slice over its base; and for an enumerable map, by 1. ◻
Proposition 1. Any map from an enumerable object to an object with enumerable diagonal (in particular, any strictly enumerable object) has split image. Any cover between such objects splits.
Proposition 1 ([15]). Let \(\mathcal{E}\) be a locos. Then \(\operatorname{Pred}{\mathcal{E}}\) is a regular sub-locos of \(\mathcal{E}\), in which every cover splits; equivalently, all objects are projective.
Proof. Closure under the locos structure of \(\mathcal{E}\) is generally straightforward; regularity and splitting are by 1. ◻
Our next main goal is the fact that in the internal free \(r\)-topos \(\freeTop[r][\mathcal{E}]\), each type is enumerable. Classical Gödel-numbering achieves this by constructing the free model entirely within the world of formal quotients of recursive subsets of \(\mathbb{N}\). Categorically, this amounts to lifting \(\freeTop[r][\mathcal{E}]\) to a suitable category of such formal quotients: the exact completion of \(\operatorname{Pred}{\mathcal{E}}\).
We recall the definition briefly; for full details see [20], [4].
Definition 25. The exact-over-lex or briefly ex/lex completion of a cartesian category \(\mathcal{E}\), denoted \({\mathcal{E}}_{\mathrm{ex/lex}}\), has objects pseudo-equivalence relations in \(\mathcal{E}\), i.e. maps \(R \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A \times A\) in \(\mathcal{E}\) satisfying reflexivity, symmetry, and transitivity. The exact-over-regular or ex/reg completion, \({\mathcal{E}}_{\mathrm{ex/reg}}\), is the full subcategory of \({\mathcal{E}}_{\mathrm{ex/lex}}\) on equivalence relations, i.e. objects with \(R \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} A \times A\) mono.
Proposition 1. If \(\mathcal{E}\) is cartesian (resp. regular), then \({\mathcal{E}}_{\mathrm{ex/lex}}\) (resp. \({\mathcal{E}}_{\mathrm{ex/reg}}\)) is exact, and these constructions form left bi-adjoints to the forgetful \(2\)-functors \(\mathcal{\uppercase{E{\mkern-1mu}X}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{LE{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{E{\mkern-1mu}X}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\).
If \(\mathcal{E}\) is additionally lextensive, then so are \({\mathcal{E}}_{\mathrm{ex/lex}}\) and \({\mathcal{E}}_{\mathrm{ex/reg}}\), and these form left adjoints to the forgetful \(2\)-functors \(\mathcal{\uppercase{PRET{\mkern-3mu}OP}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{LE{\mkern-1mu}XT}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{PRET{\mkern-3mu}OP}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{REGLE{\mkern-1mu}XT}}\@ifnotmtarg{}{_{}}\).
Proof. The universal properties in \(\mathcal{\uppercase{E{\mkern-1mu}X}}\@ifnotmtarg{}{_{}}\) are well known, given in for instance [20], [4]. For the lextensive/pretopos case, we are unaware of a source stating the universal properties, but they follow straightforwardly from the construction of coproducts/lextensivity in [21], [22]. ◻
Theorem 4. The ex/lex (resp. ex/reg) completion of a locos (resp. regular locos) is an arithmetic universe. Moreover, these form left bi-adjoints to the forgetful \(2\)-functors \(\mathcal{\uppercase{AU}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{LOC}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{AU}}\@ifnotmtarg{}{_{}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{\uppercase{REGLOC}}\@ifnotmtarg{}{_{}}\).
Proof. The special case on the locos of predicates of a Skolem theory goes back to [13], and is presented thoroughly in [15] and analysed further in [23].
Building on 1, we just need to show (for the ex/lex case) that if \(\mathcal{E}\) is a locos, then \({\mathcal{E}}_{\mathrm{ex/lex}}\) has list objects, the unit \(\mathcal{E} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} {\mathcal{E}}_{\mathrm{ex/lex}}\) preserves them, and for any locos functor from \(\mathcal{E}\) to an AU \(\mathcal{F}\), its extension to an exact functor \({\mathcal{E}}_{\mathrm{ex/lex}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{F}\) also preserves them; and similarly for the ex/reg case.
Given a pseudo-equivalence relation \(R \parpair{}{} A\), \(\mathop{\mathit{List}}R \parpair{}{} \mathop{\mathit{List}}A\) is also a pseudo-equivalence relation (since \(\mathop{\mathit{List}}\) commutes with pullbacks), giving a parametrised list object for \(R \parpair{}{} A\) in \({\mathcal{E}}_{\mathrm{ex/lex}}\), and which moreover is mono (i.e. lies in \({\mathcal{E}}_{\mathrm{ex/reg}}\)) in case \(R\) was.
The unit functor from \(\mathcal{E}\) clearly preserves list objects.
Finally, for a locos map \(F : \mathcal{E} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{F}\) with \(\mathcal{F}\) an AU, checking that the extension \(\bar{F} : {\mathcal{E}}_{\mathrm{ex/lex}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{F}\) preserves these (and \({\mathcal{E}}_{\mathrm{ex/reg}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{F}\) in case \(\mathcal{E}\), \(F\) regular) amounts to checking that \(\mathop{\mathit{List}}\) commutes with quotients of equivalence relations in \(\mathcal{F}\), which is lengthy but routine. (The special case of natural numbers objects is given in [24], adapting [25].) ◻
In particular, for any arithmetic universe \(\mathcal{E}\), \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\) is also an AU, with an AU-logical realisation functor \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) extending the realisation of predicates. (Note that this is not generally full or faithful.) Objects of \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\), or their realisations, may be called enumerably presented objects of \(\mathcal{E}\); in particular, the realisations are clearly enumerable.
With hindsight, the locos/AU structures of \(\operatorname{Pred}(\mathcal{E})\) and \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\) are clearly discernible in classical proof theory: they abstract the constructions that Gödel-numbering uses to build syntax and free algebras entirely within the world of recursive sets and their formal quotients. Concretely, key consequences of Gödel-numbering now follow directly for AU’s:
Corollary 2. In any AU, each type of the internal free \(r\)-topos (or more generally, the initial model of any finitely presented EAT) is enumerable.
Proof. Since realisation \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) is AU-logical, it preserves initial models (2), and in particular sends \(\freeTop[r][{(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}]\) to \(\freeTop[r][\mathcal{E}]\). ◻
We could equivalently have used \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/reg}}\) here: the two are equivalent since in \(\operatorname{Pred}\mathcal{E}\) all objects are projective, so by [20], \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{reg/lex}} \simeq\mathcal{E}\) and \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}} \simeq{(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/reg}}\).
Caveat 1. It is very tempting to think that realisations of objects of \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\) have enumerable diagonal, and hence that covers between them should split according to 1.
Indeed, given a pseudo-equivalence relation \(R \parpair{}{} A\) in \(\operatorname{Pred}\mathcal{E}\), we know the pullback of the diagonal \(\Delta_{A/R}\) to \(A \times A\) along the canonical cover \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} A/R\) is precisely \(R \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} A \times A\) (by exactness), and hence enumerable by 1. However, this does not imply that the diagonal \(\Delta_{A/R}\) is itself enumerable: enumerability does not in general descend along covers.
We can now give the main reflection result: the standard interpretation of \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\) internally to a topos, organised via \(r\)-universes, sequences of universes suitably closed under the constructions of \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\). Equipped with this, we will then be able to first run the Freyd gluing argument internally to a topos, and then bump it up to our main result, projectivity of \(N\) in the free topos.
Reflection arguments rely essentially on the logic in question being able to host the standard interpretation for its fragments. Constructing this typically involves building a sufficiently large universe of sets or predicates to host the interpretation.
In our case, to internalise Freyd gluing for \(r\)-toposes within a topos \(\mathcal{E}\), we need the standard interpretation of its internal free \(r\)-topos; that is, an \(r\)-logical functor \(\freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) (of \(\mathcal{E}\)-indexed \(r\)-toposes, identifying \(\freeTop[r][\mathcal{E}]\) with its externalisation and \(\mathcal{E}\) with its self-indexing as usual). For this, it suffices to construct some internal sub-\(r\)-topos of \(\mathcal{E}\); that is, an internal \(r\)-topos \(\mathrm{E}'\) whose externalisation is an indexed sub-\(r\)-topos of \(\mathcal{E}\). As \(\freeTop[r][\mathcal{E}]\) interprets by initiality into \(\mathrm{E}'\), the composite \(\freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{E}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) then yields the desired interpretation.
In this section, we construct such an internal sub-\(r\)-topos in any topos, by building a \(r\)-ranked universe — a sequence of universes closed under type constructions analogously to the levels of an \(r\)-topos.
Precisely, by a family or universe in a category with pullbacks, we simply mean a map, viewed as a family of objects indexed by its base; we will typically say “universe” just when the family is closed under some logical constructions, but will always state such closure assumptions explicitly. We typically write a family as \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\), and call it by metonymy just \(U\) [26].
Note that some literature, following [27], uses universe to mean a class of maps — essentially what we present as the indexed subcategory associated to a universe. In their terms, our universes are the (weakly) generic maps for their universes.
Fix for the rest of this section an ambient regular category \(\mathcal{E}\) with \(N\).
Definition 26. We say a family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) is contained in another \(q' : \tilde{U}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U'\) just if \(q\) is a pullback of \(q'\), and call families equivalent if they are contained in each other.
Proposition 1. Suppose \(\mathcal{E}\) is lextensive. If a family \(U\) is contained in another \(U'\), there is a family \(U''\) equivalent to \(U'\) for which the containment of \(U\) is witnessed by a monomorphism.
Proof. Take \(\tilde{U}'' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U''\) to be just \(\tilde{U}+ \tilde{U}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U+ U'\). ◻
Definition 27. Let \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) be any family in \(\mathcal{E}\). Then we write \(\mathbfcal{U}\) for the full \(\mathcal{E}\)-indexed subcategory of \(\mathcal{E}\) on objects from \(U\): that is, the \(\mathcal{E}\)-indexed category \(\mathop{\mathrm{ob}}\mathbfcal{U}_X \coloneq \mathcal{E}(X,U)\), and maps induced from \(\mathcal{E}\) by the mapping \(\mathbfcal{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) sending \(f : X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) to \(f^*\tilde{U}\), so that the resulting \(\mathcal{E}\)-indexed functor \(\mathbfcal{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) is full and faithful (considering \(\mathcal{E}\) with its self-indexing throughout, as usual). Equivalently, one could define \(\mathbfcal{U}_X\) as the full subcategory of \(\mathcal{E}/X\) on objects that are contained in \(U\), as families.
Proposition 1. For families \(U\), \(U'\), the family \(U\) is contained in (resp. equivalent to) \(U'\) just if \(\mathbfcal{U}\subseteq \mathbfcal{U}'\) (resp. \(\simeq\)) as indexed subcategories of \(\mathcal{E}\). 0◻
Definition 28. Given a family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) say that \(U\) is closed under binary products (resp. binary sums, subobjects), or contains \(1\) (resp. \(N\)) if \(\mathbfcal{U}\), is closed under these as a subcategory of \(\mathcal{E}\).
More generally, say \(q' : \tilde{U}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U'\) has power-objects (products, etc.) for \(U\) if \(\mathbfcal{U}'\) has power-objects (products, etc.) for \(\mathbfcal{U}\) as subcategories of \(\mathcal{E}\).
Translating this to more concrete data, we see:
Proposition 1. Given families \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\), \(q' : \tilde{U}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U'\) in \(\mathcal{E}\):
\(U\) contains \(N\) (resp. \(1\)) just if there is some global element \(e : 1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) such that \(e^*\tilde{U}\) is an NNO (resp. terminal) in \(\mathcal{E}\);
\(U\) is closed under binary products (resp. sums) just if there is \(f : U\times U \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) such that \(f^*\tilde{U}\) is a product (resp. sum) for \(\pi_0^*\tilde{U}\) and \(\pi_1^*\tilde{U}\) in \(\mathcal{E}/U\times U\);
\(U\) is closed under subobjects just if for every \(f : X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) and mono \(m : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} f^*\tilde{U}\), the composite \(\pi_0 m : Y \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) is a pullback of \(q\); or equivalently (if \(q\) has a power-object \(P_{U} \tilde{U}\) in \(\mathcal{E}/U\)) just if there is some map \(P_{U} \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) exhibiting the composite \({\epsilon} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} \tilde{U}\times_{U} P_{U} \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} P_{U}\) as a pullback of \(q\);
\(U'\) has power-objects for \(U\) just if there is \(f : U \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U'\) such that \(f^*\tilde{U}'\) is a power-object for \(\tilde{U}\) in \(\mathcal{E}/U\);
Proof. In each case, the given operations on \(U\) directly provide categorical closure of the corresponding subcategory. Conversely, categorical closure yields operations on \(U\) as the universal instance of each closure condition. For instance, if \(\mathbfcal{U}\) is closed under products, then the product of the pair \(\pi_0\), \(\pi_1\) in \(\mathbfcal{U}_{U\times U}\) — the “family of all products of objects from \(U\)” — is precisely a product operation \(U\times U \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) as required. ◻
Definition 29. A simple universe in a regular category with NNO is a family closed under binary products and subobjects, and containing \(1\) and \(N\).
Definition 30. An \(r\)-universe \(U_\bullet\) is a simple universe \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\), with a sequence of subobjects \(U_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} U_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} U_i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} \ldots U\) (for \(i \leq r\)), such that considering the \(U_i\) as universes by pulling back \(q\), each \(U_i\) is a simple universe, and \(U_{i+1}\) has power-objects for \(U_i\).
Proposition 1. For any simple universe \(U\), \(\mathbfcal{U}\) is a regular indexed subcategory of \(\mathcal{E}\) with \(N\). For any \(r\)-universe \(U_\bullet\), the sequence of subcategories \(\mathbfcal{U}_i \subseteq \mathbfcal{U}\) form an indexed \(r\)-topos, and the inclusion to \(\mathcal{E}\) is logical.
Proof. Closure of \(\mathbfcal{U}\) under subobjects in \(\mathcal{E}\) implies closure under equalisers and images, and hence (together with \(\times\) and \(1\)) closure under all regular structure of \(\mathcal{E}\). ◻
Proposition 1 (Cf.[11]). If a family \(\tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) is exponentiable, then \(\mathbfcal{U}\) is \(\mathcal{E}\)-small.
Proof. The internal avatar \(\mathrm{U}\) (which goes back to [28, Sec. 4]) is defined by taking \(\mathop{\mathrm{ob}}\mathrm{U}\mathrel{\vcenter{:}}= U\), and \(\mathop{\mathrm{mor}}\mathrm{U}\) the exponential \((U\times \tilde{U})^{\tilde{U}\times U}\) in \(\mathcal{E}/U\times U\). It is direct to check that \(\mathrm{U}\simeq\mathbfcal{U}\). ◻
Proposition 1. Suppose \(\mathcal{E}\) is a topos. Then any simple universe \(U\) in \(\mathcal{E}\) determines a full internal regular subcategory of \(\mathcal{E}\); and any \(r\)-universe \(U_\bullet\) determines a full internal sub-\(r\)-topos \(\mathrm{U}\) of \(\mathcal{E}\), with \(\mathrm{U}_i \simeq\mathbfcal{U}_i\) for each \(0 \leq i < r\).
Proof. In each case, 1 gives an internal avatar \(\mathrm{U}\simeq\mathbfcal{U}\).
For \(U\) a simple universe, \(\mathbfcal{U}\) is indexed-regular by [prop:simple-universe-reg-subcat], so \(\mathrm{U}\) carries internal regular structure by 1.
For \(U_\bullet\) an \(r\)-universe, the subobjects \(U_i \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} U= \mathop{\mathrm{ob}}\mathrm{U}\) give an internal ranking on \(\mathrm{U}\). The externalisations of the rank subcategories \(\mathrm{U}_i\) are equivalent to the subcategories \(\mathbfcal{U}_i \subseteq \mathbfcal{U}\), so form an indexed \(r\)-topos by [prop:simple-universe-reg-subcat], and thus an internal one by 1. ◻
So \(r\)-universes yield internal sub-\(r\)-toposes, as desired; it remains to show such universes exist, in a rich enough ambient category.
Proposition 1. Any family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) in an arithmetic universe is contained in a family closed under products.
Proof. Take the family \(\mathop{\mathit{List}}(q) : \mathop{\mathit{List}}(\tilde{U}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathop{\mathit{List}}(U)\). This contains \(U\) as the singleton lists, and is closed under products: the fibre of \(\mathop{\mathit{List}}(q)\) over a list from \(U\) is the product of the corresponding fibres of \(q\), and so concatenation of lists gives a product operation for the fibres. Careful verification of this is lengthy but straightforward with the internal type theory, along similar lines to an ordinary proof in \(\mathrm{Set}\). . ◻
Proposition 1. Any family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) in a topos is contained in a family \(U'\) closed under subobjects, and moreover closed under products if \(U\) was.
Proof. Take \(q'\) to be \({\in} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} P_{\mathcal{E}/U}(\tilde{U})\), i.e.the power-object of \(\tilde{U}\) in \(\mathcal{E}/U\). This is always closed under subobjects, since a subobject of a subobject is a subobject; and if \(U\) was closed under products, then this is too, since a product of subobjects is a subobject of a product. Again, careful verification is straightforward in the internal language. ◻
Proposition 1. For any family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) in a topos, there is a simple universe containing \(U\).
Proof. First replace \(U\) by \(q + {!_N} : \tilde{U}+ N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U+ 1\), to include \(N\). (This can be skipped if \(U\) already contains \(N\).) Then apply the two preceding propositions in turn: add products, and then add subobjects, preserving the product-closure. ◻
Proposition 1. For any family \(q : \tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) in a topos, there is a simple universe containing \(U\) and with power-objects for it.
Proof. Take the slice-wise power-object \(P_{\mathcal{E}/U}(\tilde{U}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\); this tautologically has power-objects for \(U\). Now apply the previous proposition to this family, extending it to a simple universe. By construction, this has power-objects for \(U\); but it also contains \(U\), by closure under subobjects, since any object embeds into its own power-object as singletons. ◻
Corollary 3. Any family in a topos is contained in some \(r\)-universe, for each \(r \in \mathbb{N}\).
Proof. Starting from the given family \(U_0\), we repeatedly apply 1, together with 1 to keep the inclusions mono, yielding a sequence of simple universes \(U_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} U_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} \cdots\), each with power-objects for the previous. Cutting off at stage \(r\) evidently forms an \(r\)-universe. ◻
Corollary 4. Any family in a topos is contained in some internal sub-\(r\)-topos, for each \(r \in \mathbb{N}\). 0◻
Proposition 1. Let \(\mathcal{E}\) be any topos. Then for each \(r \in \mathbb{N}\), there is an essentially unique \(r\)-logical functor of \(\mathcal{E}\)-indexed \(r\)-toposes \(\HOLinterp : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) (giving \(\mathcal{E}\) its self-indexing and full ranking), which we call the standard interpretation* of \(\freeTop[r][\mathcal{E}]\).*
Proof. gives an internal sub-\(r\)-topos \(\mathrm{E} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\). Composing this with the \(r\)-logical functor \(\freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{E}\) supplied by initiality yields an \(r\)-logical functor \(\HOLinterp : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) as desired.
Essential uniqueness follows as in 1 1, requiring just the additional observation that for \(r\)-logical \(F_0, F_1 : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\), the iso-comma \(({F_0} \mathbin{\downarrow_{\cong}} {F_1})\) is \(\mathcal{E}\)-small, by cartesian closure of \(\mathcal{E}\). ◻
Remark 1. As expected for reflection principles, 1 cannot be extended to the internal free topos: Gödel incompleteness implies that there is a non-degenerate topos \(\mathcal{G}\) whose internal free topos \(\freeTop[][\mathcal{G}]\) is degenerate, and hence cannot admit any logical functor to \(\mathcal{G}\).
Remark 1. If the ranks of an \(r\)-topos are assumed not just regular but in fact arithmetic universes, as suggested in 1, then the universes of this section need to be closed under sums and list objects. This complicates the closure of a family \(\tilde{U} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} U\) under all required operations (1): the closure is no longer simply “subobjects of formal products from the family”, easily indexed by \(P(\mathop{\mathit{List}}(U))\), but must interleave formal “list object” and “sum” operations with the products, and hence be indexed by something like the power-object of a suitable \(W\)-type. This can certainly still be done, but requires substantially more work, especially to describe the resulting total space.
On the flip side, with our current approach of regular ranks, the ranks of the universes constructed are unclear. Assuming ranks are AU’s should mean that the closure/successor constructions of 1 1 only increase rank by one or two, and hence allow the standard interpretation of an \(r\)-topos in a \((2r+1)\)- or even \((r+1)\)-topos.
With the internal standard interpretation of \(\mathrm{IHOL}_{N}\@ifnotmtarg{r}{^{r}}\) in \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) assembled, we are now ready to draw the desired applications to projectivity principles.
Theorem 5 (Internal Freyd gluing). In any topos \(\mathcal{E}\), the terminal object of the internal free \(r\)-topos \(\freeTop[r][\mathcal{E}]\) is (indexed-) projective.
Proof. We adapt the proof of 1 once again, with just a little extra work this time for the internalisation.
By 4, \(\mathcal{E}\) has some internal full sub-\(r\)-topos \(\mathrm{E}'\) including the family \(\mathop{\mathrm{mor}}\freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} (\mathop{\mathrm{ob}}\freeTop[r][\mathcal{E}])^2\) of hom-sets of \(\freeTop[r][\mathcal{E}]\), and hence such that the global sections functor \(\Gamma : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) factors as \(\Gamma' : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathrm{E}' \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\).
Now by 1, the comma category \(({\mathrm{E}'} \mathbin{\downarrow} {\Gamma'})\) is an internal \(r\)-topos, and its first projection functor \(\freeTop[r][\mathcal{E}]\) is strictly \(r\)-logical; so it admits an interpretation functor \(\freeTop[r][\mathcal{E}]\). Composing with the (\(r\)-logical, strictly over \(\freeTop[r][\mathcal{E}]\)) inclusion \(({\mathrm{E}'} \mathbin{\downarrow} {\Gamma'}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} ({\mathcal{E}} \mathbin{\downarrow} {\Gamma})\) gives an \(r\)-logical strict splitting of the projection \(({\mathcal{E}} \mathbin{\downarrow} {\Gamma}) \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop[r][\mathcal{E}]\): \[\begin{tikzcd}[column sep={5em,between origins}] & ({\mathrm{E}'} \mathbin{\downarrow} {\Gamma'}) \ar[d,"P_0"] \ar[r,inj] & ({\mathcal{E}} \mathbin{\downarrow} {\Gamma}) \ar[d,"P_0"] \ar[r,"P_1"] & \mathcal{E}\ar[d,"\mathrm{id}"] \ar[dl,Rightarrow,shorten=6mm] \\ \freeTop[r][\mathcal{E}] \ar[ur,"\HOLinterp",dashed] \ar[r,"\mathrm{id}"] & \freeTop[r][\mathcal{E}] \ar[r,"\mathrm{id}"] & \freeTop[r][\mathcal{E}] \ar[r,"\Gamma"] & \mathcal{E} \end{tikzcd}\]
Now for any \(X \in \mathcal{E}\) and cover \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1\) in \((\freeTop[r][\mathcal{E}])_X\) (i.e. map \(A : X \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \EATinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}{\mathop{\mathrm{ob}}} \mathrel{\mid}x \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1][\freeTop[r][\mathcal{E}]])\), its interpretation in \(({\mathcal{E}} \mathbin{\downarrow} {\Gamma})\) amounts (by 1) to data in \((\freeTop[r][\mathcal{E}])_X\) and \(\mathcal{E}/X\) of the form \[\begin{tikzcd} A \ar[d,->>] & & \HOLinterp[A]_1 \ar[r] \ar[d,->>] & \Gamma(A) \ar[d] \\ 1 & & \mathllap{1 = {}}\HOLinterp[1]_1 \ar[r] & \Gamma(1) \mathrlap{{}=1} \end{tikzcd}\] In \(\mathcal{E}\) itself, this amounts to: \[\begin{tikzcd} & \EATinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}{\mathop{\mathrm{ob}}} \mathrel{\mid}x \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1][\freeTop[r][\mathcal{E}]] \ar[d] & \HOLinterp[A]_1 \ar[r] \ar[d,->>] & A^*\EATinterp[ x, s \mathrel{\mid}s : 1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} x][\freeTop[r][\mathcal{E}]] \ar[d] \\ X \ar[ur,"A"] \ar[r,"1"] & \mathop{\mathrm{ob}}\freeTop[r][\mathcal{E}] & X \ar[r,"\mathrm{id}"] & X \end{tikzcd}\] This exhibits a global section of \(A\) after reindexing along the cover \(\HOLinterp[A]_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} X\), just as required for projectivity by 1. ◻
We need just one last ingredient to give the main result:
Definition 31. Let \(\mathcal{E}\) be an arithmetic universe. By the internalisation of syntax to \(\mathcal{E}\), we mean the unique \(\mathcal{E}\)-indexed \(r\)-logical functor \(\left\ulcorner \kern-0.1em - \kern-0.1em \right\urcorner : \freeTop[r] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \freeTop[r][\mathcal{E}]\) (provided by 1).
Proposition 1. Let \(\mathcal{E}\) be a topos. Then internalisation of syntax to \(\mathcal{E}\), followed by the internal standard interpretation, yields the interpretation of actual syntax into \(\mathcal{E}\). That is, the following triangle of \(\mathcal{E}\)-indexed \(r\)-logical functors commutes up to canonical isomorphism:
\[\begin{tikzcd}[row sep=small] \freeTop[r] \ar[dr,"\left\ulcorner \kern-0.1em - \kern-0.1em \right\urcorner"'] \ar[drrr,bend left=20,"\HOLinterp"{description,pos=0.45}] & & \\ \;& \freeTop[r][\mathcal{E}] \ar[rr,"\HOLinterp"{pos=0.45}] & & \mathcal{E} \end{tikzcd}\]
Proof. Immediate by bi-initiality of \(\freeTop[r]\). ◻
Theorem 6. The natural numbers object of the free topos \(\freeTop\) is projective.
Proof. By 1, it is equivalent to show this for the free \(\infty\)-ranked topos \(\freeTop[\infty]\). By compactness (1 1), any cover over \(N\) in \(\freeTop[\infty]\) is the image of such a cover in \(\freeTop[r]\) for some finite \(r\). So it suffices to show: for any \(r \in \mathbb{N}\), any cover \(e : A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} N\) in \(\freeTop[r]\), and any topos \(\mathcal{E}\), \(\HOLinterp[e]^\mathcal{E}\) has a section in \(\mathcal{E}\).
Given such \(r\), \(e\), \(\mathcal{E}\), consider the internalisation \(\left\ulcorner \kern-0.1em e \kern-0.1em \right\urcorner : \left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} \left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner\) in \(\freeTop[r][\mathcal{E}]\); this is a cover since \(\left\ulcorner \kern-0.1em - \kern-0.1em \right\urcorner\) is regular. The projectivity of \(1\) in \(\freeTop[r][\mathcal{E}]\), 5, tells us by way of 1 that taking \(\mathcal{E}\)-enriched global sections preserves covers; so \(\freeTop[r][\mathcal{E}](\left\ulcorner \kern-0.1em e \kern-0.1em \right\urcorner) : {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}} \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner)_{\mathcal{E}}\) is a cover in \(\mathcal{E}\). Pulling this back along the numeral map \(\mathop{\mathrm{num}}: N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner)_{\mathcal{E}}\) gives the square \[\begin{tikzcd} \mathop{\mathrm{num}}^*( {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}}) \ar[r] \ar[d,->>] \ar[dr,drpb] & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}} \dar[->>] \\ N \rar["\mathop{\mathrm{num}}"] & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner)_{\mathcal{E}} \end{tikzcd}\] The whole pullback lifts to \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\), so \(\mathop{\mathrm{num}}^*({\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}})\) is enumerable and we may take by 1 some section of the left-hand map (picking the Gödel-number-minimal witnessing term); equivalently, a map \(s : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}}\) over \({\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner)_{\mathcal{E}}\).
This then yields the desired section of \(\HOLinterp[e] : \HOLinterp[A] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} N\) in \(\mathcal{E}\), just by applying the standard interpretation functor \(\HOLinterp : \freeTop[r][\mathcal{E}] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \mathcal{E}\) of 1 and the internalisation-interpretation isomorphism of 1: \[\begin{tikzcd}[column sep = small] & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner)_{\mathcal{E}} \ar[r] \ar[d,cover] & \mathcal{E}_{1}(\HOLinterp[1],\HOLinterp[\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner])_{\mathcal{E}} \ar[r,"\cong"] \ar[d,cover] & \HOLinterp[\left\ulcorner \kern-0.1em A \kern-0.1em \right\urcorner] \ar[d,cover] \ar[r,"\cong"] & \HOLinterp[A] \ar[d,cover] \\ N \ar[ur, "s", dashed] \rar & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner)_{\mathcal{E}} \rar & \mathcal{E}_{1}(\HOLinterp[1],\HOLinterp[\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner])_{\mathcal{E}} \rar["\cong"] & \HOLinterp[\left\ulcorner \kern-0.1em N \kern-0.1em \right\urcorner] \rar["\cong"] & N \end{tikzcd}\] The bottom composite is \(\mathrm{id}_N\) since each step is an \((0,S)\)-algebra map. ◻
Corollary 5. Intuitionistic higher-order logic admits the rule of countable choice: \[\inferrule*[right=\mathrm{RC}_{\omega}] { \vdash\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \\exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \\varphi(n,x) } { \vdash\exists\mkern 2mu f \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X^N \\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \\varphi(n,f(n)) }\]
Indeed, if \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ \varphi(n,x)\)”, there is some \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)-definable function \(f \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X^N\) for which \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \varphi(n,f(n))\)”.
Proof. Provability of \(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ \varphi(n,x)\) amounts precisely to the projection \(\pi_0 : \HOLinterp[ n\mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N,\, x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \mid \varphi(n,x) ] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} N\) being a cover in \(\freeTop\) [2, p. II.6.1(b)].
Projectivity of \(N\) provides a section \(s\) for \(\pi_0\); but by conservativity of the interpretation [2, p. II.14.3], \(s\) amounts precisely to a definable function \(f : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} X\) such that \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\vdash\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \varphi(n,f(x))\), as required for \(\mathrm{RC}_{\omega}\). ◻
In fact, this may be strengthened to a rule of dependent choice: \[\inferrule*[right=\mathrm{RC}_{\mathrm{dep}}] { \vdash\exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \\varphi(x) \\ \vdash\forall\mkern 1mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \\left( \varphi(x) \Rightarrow\exists\mkern 2mu y \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \\left( \varphi(y) \land \rho(x,y) \right) \right) } { \vdash\exists\mkern 2mu f \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X^N \\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \\left( \varphi(f(n)) \land \rho(f(n),f(n+1))\right) }\]
Categorically, this is most clearly formulated in terms of graphs.
Definition 32.
A graph \(\mathrm{G}\) in a category \(\mathcal{E}\) is just a parallel pair \(s, t : G_1 \parpair{}{} G_0\).
A graph is simple if \(s,t\) are jointly monic, and (assuming \(\mathcal{E}\) regular) total if \(s : G_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} G_0\) and \(G_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1\) are covers.
Assuming a natural numbers object \((N,0,S)\) in \(\mathcal{E}\), a branch in \(\mathrm{G}\) is a pair of maps \(f_0 : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} G_0\), \(f_1 : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} G_1\) with \(s f_1 = f_0\), \(t f_1 = f_0 S\).
When \(\mathcal{E}\) interprets sufficient logic, the premises of \(\mathrm{RC}_{\mathrm{dep}}\) precisely describe a simple total graph in \(\mathcal{E}\) \[\HOLinterp[ x,y \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \mathrel{\mid}\varphi(x) \land \varphi(y) \land \rho(x,y)] \;\parpair[2em]{}[][cover,yshift=0.2ex]{}[][yshift=-0.2ex] \; \HOLinterp[ x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \mathrel{\mid}\varphi(x) ] \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \quad\ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1,\] and its conclusion asserts (internal) existence of a branch. As with \(\mathrm{RC}_{\omega}\), we get the slightly stronger conclusion (equivalent since \(1\) is projective) of external/global existence:
Theorem 7. Every total graph in \(\freeTop\) has a branch; so \(\freeTop\) validates \(\mathrm{RC}_{\mathrm{dep}}\).
Proof. By compactness as in 6, any total graph in \(\freeTop\) lifts to some \(\freeTop[r]\), so it suffices to show: for any \(r \in \mathbb{N}\), any total graph \(\mathrm{G}\) in \(\freeTop[r]\), and any topos \(\mathcal{E}\), \(\HOLinterp[ \mathrm{G}]^\mathcal{E}\) has a branch in \(\mathcal{E}\).
Again, we next internalise \(\mathrm{G}\) to a total graph \(\left\ulcorner \kern-0.1em \mathrm{G} \kern-0.1em \right\urcorner\) in \(\freeTop[r][\mathcal{E}]\). Taking (\(\mathcal{E}\)-enriched) global sections, the resulting graph \({\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em \mathrm{G} \kern-0.1em \right\urcorner)_{\mathcal{E}}\) is still total by \(\mathcal{E}\)-indexed projectivity of \(1\) in \(\freeTop[r][\mathcal{E}]\).
We know \({\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em \mathrm{G} \kern-0.1em \right\urcorner)_{\mathcal{E}}\) lifts to \({(\operatorname{Pred}\mathcal{E})}_{\mathrm{ex/lex}}\), so denoting its canonical cover by \(p : \overline{G}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em G_0 \kern-0.1em \right\urcorner)_{\mathcal{E}}\), we can pull the arrows \({\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em G_1 \kern-0.1em \right\urcorner)_{\mathcal{E}}\) back along \(p \times p\) to obtain a graph \(\overline{\mathrm{G}}\), again total and with \(\overline{G}_1\) enumerable, but now also with \(\overline{G}_0\) (the object of “terms of type \(\left\ulcorner \kern-0.1em G_0 \kern-0.1em \right\urcorner\)”) strictly enumerable.
The covers \(\overline{s} : \overline{G}_1 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} \overline{G}_0\) and \(\overline{G}_0 \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} 1\) now admit by 1 some splittings \(k\), \(a\); these give a branch in \(\overline{\mathrm{G}}\) (with \(f_0 : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} \overline{G}_0\) specified by \(f_0 0 = a\), \(f_0 S = \bar{t}kf_0\)), and mapping this across through the internal standard interpretation gives the required branch in \(\HOLinterp[\mathrm{G}][\mathcal{E}]\): \[\begin{tikzcd}[baseline=(\tikzcdmatrixname-3-1.base)] \;\! \overline{G}_1\!\!\: \ar[dr,drpb] \ar[r] \ar[d,cover,"\bar{s}" description] \ar[d,shift left=2,"\bar{t}"] & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em G_1 \kern-0.1em \right\urcorner)_{\mathcal{E}} \ar[d,cover,shift right] \ar[d,shift left] \ar[r,"\HOLinterp"] & \mathcal{E}_{}(1,\HOLinterp[\left\ulcorner \kern-0.1em G_1 \kern-0.1em \right\urcorner])_{\mathcal{E}} \ar[r,"\cong"] \ar[d,cover,shift right] \ar[d,shift left] & \HOLinterp[G_1][\mathcal{E}] \ar[d,cover,shift right,"s"'] \ar[d,shift left,"t"] \\ \, \overline{G}_0\! \ar[r,cover] \ar[d,cover] \ar[u,bend left,dashed,"k"] & {\freeTop[r][\mathcal{E}]}_{}(1,\left\ulcorner \kern-0.1em G_0 \kern-0.1em \right\urcorner)_{\mathcal{E}} \ar[d,cover] \ar[r,"\HOLinterp"] & \mathcal{E}_{}(1,\HOLinterp[\left\ulcorner \kern-0.1em G_0 \kern-0.1em \right\urcorner])_{\mathcal{E}} \ar[r,"\cong"] \ar[d,cover] & \HOLinterp[G_0][\mathcal{E}] \ar[d,cover] \\ 1 \ar[u,bend left,dashed,"a"] & 1 & 1 & 1 \end{tikzcd} \qedhere\] ◻
Corollary 6. The rule of dependent choice \(\mathrm{RC}_{\mathrm{dep}}\) is admissible for \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\). Indeed, whenever \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ \varphi(x)\)” and “\(\forall\mkern 1mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ ( \varphi(x) \Rightarrow \exists\mkern 2mu y \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}X \ ( \varphi(y) \land \rho(x,y) ))\)”, there is some \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)-definable function \(f : X^N\) for which \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) proves “\(\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \ \left( \varphi(f(n)) \land \rho(f(n),f(n+1))\right)\)”. 0◻
The present development differs in several respects from the treatment in Makkai’s manuscript [1].
Most significantly, Makkai makes use throughout of the correspondence between \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) (presented in a traditional syntax) and elementary toposes, while we work purely categorically, referring to \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) occasionally for intuition, but never formally until the final 5. For instance, Makkai defines an \(r\)-topos as a Heyting category with subobject classifier that admits interpretations of all \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)-types of rank \(\leq r\): he ranks the syntax, not its categorical interpretation. Similarly, he presents free (\(r\)-)toposes using the syntax of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) (along similar lines to [2]), and their internalisations using the Gödel-number encoding of this syntax. By contrast, we avoid encoding details by appealing to the general existence of free structures in arithmetic universes, and correspondingly using a finitely-presented essentially algebraic notion of \(r\)-topos.
A more inessential difference, but perhaps of interest, is that where we have used indexed/fibred categories to mediate between external and internal categories, Makkai uses enriched categories instead.
The early history of work on \(\mathrm{RC}_{\omega}\) is somewhat murky, with more folklore than published literature; the following is the best understanding we have been able to reach, based in part on correspondence with Phil Scott and conversations with Michael Makkai. For now we survey this just in outline, deferring discussion of technicalities to 4.5
The first proof of admissibility of \(\mathrm{RC}_{\omega}\) was for second-order arithmetic (\(\mathrm{HAS}\)), in Troelstra [29], couched in traditional proof-theoretic language (and with a technical error corrected by Hayashi [30]).5
Following the splash of Freyd’s elegant categorical proof of \(\mathrm{EP}\) and \(\mathrm{DP}\) for toposes, there was a general interest in extending categorical methods to other proof-theoretic results; in particular, proposals for adapting \(\mathrm{RC}_{\omega}\) to \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) were presented at least by Joyal, Makkai, and Friedman and Scedrov. However, this work of Joyal and Makkai never made it into print, while that of Friedman and Scedrov appeared as [32], including several related results but not \(\mathrm{RC}_{\omega}\).
On the non-categorical side, it has been suggested to us that \(\mathrm{RC}_{\omega}\) for some second- or higher-order system appears in work of Hayashi, but we have been unable to locate it there. [30] builds on and corrects the methods of [29], giving various derived rules for a variant of \(\mathrm{HAS}\), using approaches somewhat analogous to those of the present proof (formalising \(\mathrm{EP}\) and satisfaction for fragments of \(\mathrm{HAS}\) within \(\mathrm{HAS}\)), and outlining how to adapt the results to a higher-order system; but it does not consider \(\mathrm{RC}_{\omega}\) or similar principles. It thus seems likely to us that Hayashi, too, may have presented a proof of \(\mathrm{RC}_{\omega}\) during this period that was never published.
Subsequent work using the technique of realizability with truth has shown admissibility of the full rule of choice for various constructive systems, mainly \(\mathrm{HA}^\omega\) and close variants [33], including just the finite types (that is, iterated exponentials of \(N\)). Recent work of Frittaion, Nemoto, and Rathjen [34] extends this method to constructive set theories, but retains the type restriction in the rule considered: Thm. 8.2 there shows that a range of theories including CZF and IZF admit the “rule of choice at finite types”: \[\inferrule*[right=\mathrm{RC}_{\mathrm{FT}},left=\textrm{(\sigma, \tau finite types)}] { \vdash\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}\sigma \\exists\mkern 2mu x \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}\tau \\varphi(n,x) } { \vdash\exists\mkern 2mu f \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}\tau^\sigma \\forall\mkern 1mu n \mspace{2 mu plus 1mu minus 1mu}\mathord{:}\mspace{2 mu plus 1mu minus 1mu}N \\varphi(n,f(n)) }\] These results are thus neither more or less general than \(\mathrm{RC}_{\omega}\) for systems with power-types/-sets: the domain type of the choice is more general, but the target type is restricted, and in particular cannot involve power-types.
In the introduction we outlined the argument in terms of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\); then we actually proved it entirely categorically, and extracted the \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) version as a corollary. As usual, the categorical treatment could be compiled down into a more traditionally proof-theoretic treatment working syntactically in \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\), along the lines of the introductory sketch.
In such a development, our reflection theorems (4) would turn out essentially like Lemmas 4.5.8–9 of [29], and our endgame much like the proof of Thm. 4.5.12 there (all adapted from \(\mathrm{HAS}\) to \(\mathrm{HAH}\)/\(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)). The most substantial difference from Troelstra/Hayashi’s approach is that they obtain \(\mathrm{EP}\) by normalisation techniques, where we used Freyd’s gluing argument. As shown in Scedrov and Scott [35], Freyd’s gluing topos corresponds on the syntactic side to a variant of the Kleene slash due to Friedman6 ; our proof thus corresponds to suitable internalisations of the Friedman slash for fragments of \(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\)/\(\mathrm{HAH}\).
How does such a treatment compare with the present version? Purely proof-theoretic approaches can be more elementary, and in many respects intuitively and expositorily simpler. However, the bureaucratic encoding required for internalisation of syntax, and the subsequent internalisation of arguments, is typically given by hand just as required — hard to write and worse to read, so almost always suppressed. As Troelstra writes [29]: “We sketch the argument: full details are long and tedious, and hardly instructive.”
Categorical presentations cannot fully avoid these encoding details, but they allow them to be organised more uniformly, and given in clearer generality. So the tedious work can be done once and for all, with a precise and broad scope of applicability.
Overall, the picture is a common one: The categorical framework entails some extra overhead, not so much of technical work as of intuition. In return, however, it permits a more modular presentation, with more of the work packaged into general, broadly applicable results, and less ad hoc calculation.
Most fruitful of all, however, is the flexibility to pass freely back and forth, with the categorical framework to handle higher-level structural results, but dropping back into syntax for more elementary work as convenient, as we did for the low-level constructions of [sec:universes] [sec:internal-free-models].
Here we lay out, for reference and overview, the notational conventions we aim to follow in the paper.
\(2\)-categories of large categories: \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\), \(\mathcal{\uppercase{REG}}\@ifnotmtarg{}{_{}}\), \(\LOG\), \(\LOG[r]\); of indexed cats, \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{\mathcal{B}}{\mkern-3.5mu}}}\@ifnotmtarg{\mathcal{B}}{_{\mathcal{B}}}\), etc.
\(2\)-categories of small categories: \(\mathcalit{C{\mkern-2mu}at}\@ifnotmtarg{}{_{}}\), \(\@ifnotmtarg{}{\text{-}}\mathcalit{L{\mkern-2mu}og}\), \(\@ifnotmtarg{r}{r\text{-}}\mathcalit{L{\mkern-2mu}og}\); of indexed cats, \(\mathcalit{C{\mkern-2mu}at}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}\) etc.; of internal cats, \(\mathrm{Cat}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\) etc.
Specific large (\(1\)-)categories, e.g. of small or internal algebraic structures: \(\mathrm{Cat}_\mathit{str}\@ifnotmtarg{\mathcal{E}}{(\mathcal{E})}\), \(\strLog[r]\), \(\mathrm{Mod}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}}(\mathsf{T})\)
Arbitrary potentially-large categories: \(\mathcal{E}\) (typically when logically-structured), \(\mathcal{C}\)
Specific logical free/syntactic categories (small, but nonetheless important citizens of the world of possibly-large categories): \(\freeTop[r][\mathcal{E}]\), \(\mathrm{C}_{\mathsf{T}}\)
Arbitrary small categories: \(\mathrm{E}\) (esp.if logical), \(\mathrm{C}\)
Arbitrary internal categories: \(\mathrm{E}\) (esp.if logical), \(\mathrm{C}\)
Interpretations of logical languages in categories:
\(\mathrm{IHOL}_{N}\@ifnotmtarg{}{^{}}\) (or similar) in a topos: \(\HOLinterp[ X^N][\mathcal{E}]\).
Internal language of an AU: \(\AUinterp[ N\times N][\mathcal{E}]\).
EAT in a model: \(\EATinterp[ X ][M]\).
Indexed hom-objects: \(\mathcal{E}_{X}(A,B)_{}\).
Arrows testing: \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} B\), \(A \rightarrow B\), \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->,inj] (a.south west) -- (a.south east);} \mkern-1mu} B\), \(A \hookrightarrow B\), \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle \ \,}; \draw[cd-arrow-style,->>] (a.south west) -- (a.south east);} \mkern-1mu} B\) \(A \twoheadrightarrow B\).
Parallel pairs: \(A \parpair[2em]{s}[xshift=-0.2em][cover]{t} B\), \(A \parpair{}{} B\)
Check how inline arrows affect line spacing: testing paragraph and enough test to fill out a line of words text filling out the line like a long and rather stupid sentence. Now some text again to get onto the next line and then \(A \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} B\) let’s see how it raises the line height compared to the other lines, and what about the depth as well. Now what about if we put a parallel pair in in the style above: \(A \parpair{s}{t} B\) what does that look like? Good; not too much effect on the line spacing now!
Fonts testing:
\(\mathbf{CAT}\), \(\mathbf{Cat}\), \(\mathbf{REG}\), \(\mathbf{Reg}\), \(\mathbf{LOG}\), \(\mathbf{Log}\)
\(\mathscr{CAT}\), \(\mathscr{Cat}\), \(\mathscr{REG}\), \(\mathscr{Reg}\), \(\mathscr{LOG}\), \(\mathscr{Log}\)
\(\mathcalit{CAT}\), \(\mathcalit{Cat}\), \(\mathcalit{REG}\), \(\mathcalit{Reg}\), \(\mathcalit{LOG}\), \(\mathcalit{Log}\)
\(\mathbfcalit{CAT}\), \(\mathbfcalit{Cat}\), \(\mathbfcalit{REG}\), \(\mathbfcalit{Reg}\), \(\mathbfcalit{LOG}\), \(\mathbfcalit{Log}\)
\(\mathfrak{CAT}\), \(\mathfrak{Cat}\), \(\mathfrak{REG}\), \(\mathfrak{Reg}\), \(\mathfrak{LOG}\), \(\mathfrak{Log}\)
Testing scale-matching between fonts/alphabets:
ABQabxgf\(ABQabxgf\) \(\mathcalit{ABQabxgf}\) \(\mathfrak{ABQabxgf}\) ABQabxgf ABQabxgf ABQabxgf
Kerning testing, for mathcal category names: \[\begin{array}{rccccccccc} 0\textrm{mu} & \mathcalit{C{\mkern 0mu} AT} & \mathcalit{C{\mkern 0mu} at} & \mathcalit{L{\mkern 0mu} og} & \mathcalit{R{\mkern 0mu} eg} & \mathcalit{L{\mkern 0mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern 0mu}_{\mathcal{E}} & \mathcalit{LE{\mkern 0mu}XT} & \mathcalit{PRET{\mkern 0mu}OP} \\ -0.5\textrm{mu} & \mathcalit{C{\mkern-0.5mu} AT} & \mathcalit{C{\mkern-0.5mu} at} & \mathcalit{L{\mkern-0.5mu} og} & \mathcalit{R{\mkern-0.5mu} eg} & \mathcalit{L{\mkern-0.5mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-0.5mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-0.5mu}XT} & \mathcalit{PRET{\mkern-0.5mu}OP} \\ -1\textrm{mu} & \mathcalit{C{\mkern-1mu} AT} & \mathcalit{C{\mkern-1mu} at} & \mathcalit{L{\mkern-1mu} og} & \mathcalit{R{\mkern-1mu} eg} & \mathcalit{L{\mkern-1mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-1mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-1mu}XT} & \mathcalit{PRET{\mkern-1mu}OP} \\ -1.5\textrm{mu} & \mathcalit{C{\mkern-1.5mu} AT} & \mathcalit{C{\mkern-1.5mu} at} & \mathcalit{L{\mkern-1.5mu} og} & \mathcalit{R{\mkern-1.5mu} eg} & \mathcalit{L{\mkern-1.5mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-1.5mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-1.5mu}XT} & \mathcalit{PRET{\mkern-1.5mu}OP} \\ -2\textrm{mu} & \mathcalit{C{\mkern-2mu} AT} & \mathcalit{C{\mkern-2mu} at} & \mathcalit{L{\mkern-2mu} og} & \mathcalit{R{\mkern-2mu} eg} & \mathcalit{L{\mkern-2mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-2mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-2mu}XT} & \mathcalit{PRET{\mkern-2mu}OP} \\ -2.5\textrm{mu} & \mathcalit{C{\mkern-2.5mu} AT} & \mathcalit{C{\mkern-2.5mu} at} & \mathcalit{L{\mkern-2.5mu} og} & \mathcalit{R{\mkern-2.5mu} eg} & \mathcalit{L{\mkern-2.5mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-2.5mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-2.5mu}XT} & \mathcalit{PRET{\mkern-2.5mu}OP} \\ -3\textrm{mu} & \mathcalit{C{\mkern-3mu} AT} & \mathcalit{C{\mkern-3mu} at} & \mathcalit{L{\mkern-3mu} og} & \mathcalit{R{\mkern-3mu} eg} & \mathcalit{L{\mkern-3mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-3mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-3mu}XT} & \mathcalit{PRET{\mkern-3mu}OP} \\ -3.5\textrm{mu} & \mathcalit{C{\mkern-3.5mu} AT} & \mathcalit{C{\mkern-3.5mu} at} & \mathcalit{L{\mkern-3.5mu} og} & \mathcalit{R{\mkern-3.5mu} eg} & \mathcalit{L{\mkern-3.5mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-3.5mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-3.5mu}XT} & \mathcalit{PRET{\mkern-3.5mu}OP} \\ -4\textrm{mu} & \mathcalit{C{\mkern-4mu} AT} & \mathcalit{C{\mkern-4mu} at} & \mathcalit{L{\mkern-4mu} og} & \mathcalit{R{\mkern-4mu} eg} & \mathcalit{L{\mkern-4mu} ex} & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}{\mkern-4mu}_{\mathcal{E}} & \mathcalit{LE{\mkern-4mu}XT} & \mathcalit{PRET{\mkern-4mu}OP} \\ \hline \text{best} & 1.5? & 2? & 2? & 2? & 2? & -3.5? & -1? & -3? \\ & \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}& \mathcalit{C{\mkern-2mu}at}\@ifnotmtarg{}{_{}}& \@ifnotmtarg{}{\text{-}}\mathcalit{L{\mkern-2mu}og}& \mathcalit{R{\mkern-2mu}eg}\@ifnotmtarg{}{_{}}& \mathcalit{L{\mkern-2mu}ex}\@ifnotmtarg{}{_{}}& \mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{\mathcal{E}}{\mkern-3.5mu}}}\@ifnotmtarg{\mathcal{E}}{_{\mathcal{E}}} & \mathcal{\uppercase{LE{\mkern-1mu}XT}}\@ifnotmtarg{}{_{}}& \mathcal{\uppercase{PRET{\mkern-3mu}OP}}\@ifnotmtarg{}{_{}} \end{array}\]
Any opinions, findings and conclusions are those of the authors and do not necessarily reflect the views of the United States Air Force.↩︎
In most literature, topos is defined without NNO by default, but the free topos means the free topos-with-NNO. In light of the latter, we take the version with NNO as fundamental.↩︎
In fact the limits in \(\mathcal{\uppercase{C{\mkern-1.5mu}AT\@ifnotmtarg{}{\mkern-3.5mu}}}\@ifnotmtarg{}{_{}}\) and \(\mathcal{\uppercase{LFP}}\@ifnotmtarg{}{_{}}\) should always coincide; but we have not been able to find a reference for this, and checking that both conditions hold when we apply the lemma is easier than proving the general case.↩︎
Predicates are usually defined assuming just finite products and an NNO, using the idempotent \(\min (1,-) : N \mathrel{\mkern-1mu \tikz[baseline={([yshift=-0.58ex]a.south)}]{ \node[minimum width=1em,align=center,inner xsep=0.5ex,inner ysep=0.15ex] (a) {\scriptstyle }; \draw[cd-arrow-style,->] (a.south west) -- (a.south east);} \mkern-1mu} N\) to simulate \(2 = \{0,1\}\) as a formal retract of \(N\).↩︎
This erratum merits a little explanation, as the descriptions in [30] and [31] are slightly obscure: they strengthen Lemma 4.5.8 of [29], but do not mention where the strengthening is required. The issue is that Lemmas 4.5.8 and 4.5.9 can each be stated in two forms: with an external quantification over actual formulas, or an internal quantification over (Gödel-codes of) formulas in \(\mathrm{HAS}\). [29] gives both in their external forms, which indeed suffice for subsequent applications there. However, the proof of Lemma 4.5.9 involves an internal induction over (codes of) proofs, so needs its statement to range over arbitrary internal formulas, and thus requires the stronger, internal version of Lemma 4.5.8.↩︎
In fact many normalisation arguments can also be fruitfully analysed as gluing constructions [36], as can realizability with truth [37].↩︎
Remark 1. This is one of the places where the crude definition of \(r\)-toposes (rank just for objects, not maps) weakens a result unnecessarily: with a good map-based definition of rank, I think this shouldn’t require \(F\) to be rank-preserving. Probably should consolidate remarks about this point somewhere.