Some free constructions in realizability and proof theory (Q1903677): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q1250099 |
Changed an Item |
||
Property / reviewed by | |||
Property / reviewed by: Marta C. Bunge / rank | |||
Normal rank |
Revision as of 23:04, 22 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Some free constructions in realizability and proof theory |
scientific article |
Statements
Some free constructions in realizability and proof theory (English)
0 references
19 June 1996
0 references
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.
0 references
effective topos
0 references
free colimit construction
0 references
exact completion
0 references
lex category
0 references
stack completion
0 references
full reflective subcategory
0 references
polymorphism
0 references
stable factorization systems
0 references
regular category
0 references