Some free constructions in realizability and proof theory (Q1903677): Difference between revisions

In this paper, the ``effective topos'' [cf. \textit{J. M. E. Hyland}, in: The L. E. J. Brower Centen. Symp., Stud. Logic Found. Math. 110, 165-216 (1982; Zbl 0522.03055)]\ is revisited as a free colimit construction, basically as done by \textit{E. Robinson} and \textit{G. Rosolini} [J. Symb. Logic 55, No. 2, 678-689 (1990; Zbl 0713.18003)]. Explicitly, the effective topos arises as the exact completion of the lex category \({\mathcal F}\) obtained from \({\mathcal S}ets\) by freely adjoining sums indexed by subsets of the natural numbers object \(N\), but only allowing morphisms between such sums to be encoded by restrictions of partial recursive endomorphisms of \(N\). Thus construction is here compared with that of gluing sets along the inclusion of the small category \(\mathcal R\) of subsets of \(N\) and restrictions of partial recursive endomorphisms of \(N\). The author then shows that the stack completion of the exact completion of the lex category \({\mathcal R}\) mentioned above, is a full reflective subcategory of the effective topos which is cocomplete, the latter using properties of the reflector. This treatment of the (alas, still unanswered) question of the possible existence, within a realizability topos such as the effective topos, of a small complete category in which to model polymorphism, is to be contrasted with that of \textit{J. M. E. Hyland}, \textit{E. P. Robinson} and \textit{G. Rosolini} [Proc. Lond. Math. Soc., III. Ser. 60, No. 1, 1-36 (1990; Zbl 0703.18002)]. To the latter, the authors begin by considering an obviously complete (yet not obviously small or not small) full subcategory of the effective topos, namely a suitable category \(orth(A)\), of objects orthogonal to a regular projective well supported object \(A\), and then carving out, within it, a small category whose externalization has \(orth(A)\) as stack completion. The paper being reviewed is highly readable as well as instructive in matters related to free completions and to the connection between stack completions and stable factorization systems arising from a full reflective subcategory of a regular category.