Preface |
|
v | |
Introduction |
|
ix | |
|
Partial Combinatory Algebras |
|
|
1 | (48) |
|
|
1 | (4) |
|
Pairing, Booleans and Definition by Cases |
|
|
5 | (1) |
|
|
5 | (6) |
|
Further properties; recursion theory |
|
|
11 | (4) |
|
|
11 | (4) |
|
|
15 | (9) |
|
|
15 | (1) |
|
|
15 | (1) |
|
|
15 | (2) |
|
|
17 | (1) |
|
|
18 | (2) |
|
|
20 | (1) |
|
|
21 | (1) |
|
|
22 | (1) |
|
|
22 | (1) |
|
|
23 | (1) |
|
|
23 | (1) |
|
|
23 | (1) |
|
|
24 | (6) |
|
Applicative morphisms and S-functors |
|
|
30 | (5) |
|
Decidable applicative morphisms |
|
|
35 | (5) |
|
|
40 | (9) |
|
Realizability triposes and toposes |
|
|
49 | (66) |
|
|
49 | (15) |
|
Preorder-enriched categories |
|
|
49 | (2) |
|
Triposes: definition and basic properties |
|
|
51 | (4) |
|
Interpretation of languages in triposes |
|
|
55 | (4) |
|
|
59 | (5) |
|
The tripos-to-topos construction |
|
|
64 | (5) |
|
Internal logic of C[ P] reduced to the logic of P |
|
|
69 | (4) |
|
The `constant objects' functor |
|
|
73 | (9) |
|
|
82 | (16) |
|
Geometric morphisms of toposes |
|
|
82 | (4) |
|
Geometric morphisms of triposes |
|
|
86 | (6) |
|
Geometric morphisms between realizability triposes on Set |
|
|
92 | (3) |
|
Inclusions of triposes and toposes |
|
|
95 | (3) |
|
Examples of triposes and inclusions of triposes |
|
|
98 | (11) |
|
|
98 | (1) |
|
|
98 | (1) |
|
Set as a subtopos of RT(A) |
|
|
99 | (1) |
|
|
100 | (1) |
|
Order-pcas with the pasting property |
|
|
101 | (1) |
|
Extensional realizability |
|
|
102 | (1) |
|
|
102 | (1) |
|
|
103 | (3) |
|
|
106 | (1) |
|
|
107 | (2) |
|
|
109 | (2) |
|
|
111 | (4) |
|
|
115 | (140) |
|
Recapitulation and arithmetic in 僃 |
|
|
115 | (17) |
|
Second-order arithmetic in 僃 |
|
|
125 | (6) |
|
Third-order arithmetic in 僃 |
|
|
131 | (1) |
|
Some special objects and arrows in 僃 |
|
|
132 | (22) |
|
Closed and dense subobjects |
|
|
132 | (1) |
|
Infinite coproducts and products |
|
|
133 | (1) |
|
Projective and internally projective objects, and choice principles |
|
|
134 | (4) |
|
僃 as a universal construction |
|
|
138 | (2) |
|
|
140 | (3) |
|
Discrete and modest objects |
|
|
143 | (5) |
|
Decidable and semidecidable subobjects |
|
|
148 | (6) |
|
|
154 | (8) |
|
|
155 | (2) |
|
Specker sequences and singular coverings |
|
|
157 | (2) |
|
|
159 | (3) |
|
Discrete families and Uniform maps |
|
|
162 | (31) |
|
Weakly complete internal categories in 僃 |
|
|
178 | (15) |
|
|
193 | (21) |
|
The McCarty model for IZF |
|
|
193 | (18) |
|
The Lubarsky-Streicher-Van den Berg model for CZF |
|
|
211 | (1) |
|
Well-founded trees and W-Types in 僃 |
|
|
212 | (2) |
|
Synthetic Domain Theory in 僃 |
|
|
214 | (16) |
|
|
215 | (3) |
|
|
218 | (1) |
|
Elements of Synthetic Domain Theory |
|
|
219 | (9) |
|
|
228 | (2) |
|
Synthetic Computability Theory in 僃 |
|
|
230 | (4) |
|
General Comments about the Effective Topos |
|
|
234 | (21) |
|
Analogy between and the Yoneda embedding |
|
|
235 | (4) |
|
Small dense subcategories in 僃 |
|
|
239 | (6) |
|
Idempotence of realizability |
|
|
245 | (10) |
|
|
255 | (36) |
|
Extensional Realizability |
|
|
255 | (8) |
|
|
262 | (1) |
|
|
263 | (5) |
|
|
268 | (6) |
|
|
274 | (3) |
|
|
277 | (6) |
|
Realizability toposes over other toposes |
|
|
283 | (8) |
|
|
283 | (4) |
|
A sheaf model of realizability |
|
|
287 | (4) |
Bibliography |
|
291 | (14) |
Index |
|
305 | |