Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.
Fix the set ℕ and write 𝑎 ⋅𝑏 for the value of the 𝑎-th partial recursive function at 𝑏, when that value is defined. Call a subset 𝑝 ⊆ℕ a proposition and an element of 𝑝 a realizer of it, and put 𝑝→𝑞:={𝑎∈ℕ∣𝑎⋅𝑏 is defined and lies in 𝑞, for every 𝑏∈𝑝}. For a set 𝐼 let P𝐼 be the set of functions 𝜑 :𝐼 →P(ℕ), and declare 𝜑 ≤𝜓 when one number realizes the implication everywhere: 𝜑≤𝜓whenthere is 𝑎∈ℕ with 𝑎∈𝜑(𝑖)→𝜓(𝑖) for every 𝑖∈𝐼.
This is a hyperdoctrine in the sense of definition 143.8, and exercise 143.4 already met a construction of the same shape. The base category is still 𝐒𝐞𝐭: its objects are bare sets, and the computational content of (144.2) lives only in the fibers. A morphism 𝐼 →𝐽 of the base is an arbitrary function, computable or not.
The construction of this chapter changes that. Its objects are sets equipped with a P-valued equality, and its morphisms are equivalence classes of predicates rather than functions. The result is a category in which the object of natural numbers has exactly the total recursive functions as endomorphisms (theorem 144.23), and in which the whole of intuitionistic higher-order logic can be interpreted. Two ingredients are needed that definition 143.8 did not require: a generic predicate, which makes the fibers into objects of the base; and the observation that the fibers are preorders and not posets, so that a predicate carries more information than the set of predicates below it.
Triposes
A Heyting pre-algebra is a preorder with finite meets, finite joins, and a Heyting implication in the sense of definition 143.1. Its operations are determined only up to the equivalence 𝑎 ⊣⊢𝑏, meaning 𝑎 ≤𝑏 and 𝑏 ≤𝑎.
Referenced from 3 locations
Antisymmetry is deliberately absent. In (144.2) two different functions 𝜑 ≠𝜓 may satisfy 𝜑 ≤𝜓 ≤𝜑 while carrying different realizers; identifying them would destroy the generic predicate of definition 144.2(iii), which requires the predicates over 𝐼 to be indexed by functions 𝐼 →Σ.
A tripos P consists of
for each set 𝐼 a Heyting pre-algebra (P𝐼, ≤𝐼);
for each function 𝑓 :𝐼 →𝐽 a monotone map P𝑓 :P𝐽 →P𝐼, written 𝑓∗, together with monotone ∃𝑓,∀𝑓 :P𝐼 →P𝐽, such that
∃𝑓 ⊣𝑓∗ ⊣∀𝑓;
𝑓∗ preserves ⇒;
P is pseudo-functorial: id∗𝐼 ⊣⊢idP𝐼 and (𝑔 ∘𝑓)∗ ⊣⊢𝑓∗ ∘𝑔∗ for 𝑓 :𝐼 →𝐽, 𝑔 :𝐽 →𝐾;
the Beck–Chevalley condition of definition 143.7 holds for ∀, up to ⊣⊢, on every pullback square in 𝐒𝐞𝐭;
a generic predicate: a set Σ, an element 𝜎 ∈PΣ, and for each 𝐼 a chosen map { −}𝐼 :P𝐼 →𝐒𝐞𝐭(𝐼,Σ) with 𝜑 ⊣⊢{𝜑}∗𝐼(𝜎).
Referenced from 10 locations
This is Definition 1.2 of Hyland, Johnstone and Pitts, Tripos theory, physical page 3 of the author archive copy (article page 207), with Definition 1.1 on the same page. Two clauses differ from definition 143.8 and the difference is exactly the subject of this chapter. Clause (ii)(b) is an assumption here: as the source records on the following page, preservation of ⇒ cannot be deduced from Beck–Chevalley, because the meet is not given by a pullback in the base. Clause (iii) has no counterpart at all in definition 143.8.
Let P be a tripos and let ――P𝐼 be the poset reflection of P𝐼, that is, its quotient by ⊣⊢. Then ――P is a hyperdoctrine over 𝐒𝐞𝐭 in the sense of definition 143.8.
Referenced from 4 locations
Proof of Proposition 144.3 — A tripos presents a hyperdoctrine
Proof. ⊣⊢ is an equivalence relation, and every operation named in definition 144.2 is monotone, hence descends to the quotient and remains monotone there. Each ――P𝐼 is a Heyting algebra, because a meet, join or implication is determined up to ⊣⊢ by its universal property and therefore uniquely in the quotient. Clause (ii)(c) becomes strict functoriality, since two elements related by ⊣⊢ have the same class: ―――――(𝑔∘𝑓)∗ =―――𝑓∗ ∘―――𝑔∗ and ―――id∗ =id. Adjunctions and the Beck–Chevalley equations pass to the quotient for the same reason, the latter now as equalities. 𝐒𝐞𝐭 has finite products. ◻
Proposition 144.3 is what licenses the use of theorem 143.24 below: a formula of intuitionistic first-order logic interpreted in P by the clauses of definition 143.22 is sound, because it is sound in ――P and the interpretation of a formula in P is determined up to ⊣⊢. Higher-order features are added in section 144.3 using the generic predicate, which the reflection does not see.
P𝐼:=P(𝐼) with the structure of example 143.10, Σ:={0,1} and 𝜎:={1} ∈P(Σ). For 𝜑 ⊆𝐼 let {𝜑}𝐼 be its characteristic function; then {𝜑}−1𝐼({1}) =𝜑, so clause (iii) holds with equality rather than merely ⊣⊢. The fibers are posets, so this tripos is its own poset reflection.
Referenced from 3 locations
A partial applicative structure is a set 𝐴 with a partial binary operation (𝑎,𝑏) ↦𝑎 ⋅𝑏 for which there are 𝑒,𝑘,𝑠 ∈𝐴 with 𝑒⋅𝑎≍𝑎,(𝑘⋅𝑎)⋅𝑏≍𝑎,((𝑠⋅𝑎)⋅𝑏)⋅𝑐≍(𝑎⋅𝑐)⋅(𝑏⋅𝑐) for all 𝑎,𝑏,𝑐 ∈𝐴, where 𝑥 ≍𝑦 means that one side is defined exactly when the other is and then they are equal.
Referenced from 3 locations
Let 𝐴 be a partial applicative structure. Put P𝐼:=P(𝐴)𝐼 with → defined by (144.1) and ≤𝐼 by (144.2), both read with 𝐴 in place of ℕ. For 𝑓 :𝐼 →𝐽 put 𝑓∗𝜑:=𝜑 ∘𝑓, and (∀𝑓𝜑)(𝑗):=⋂𝑖∈𝐼([[𝑓(𝑖)=𝑗]]→𝜑(𝑖)),[[𝑓(𝑖)=𝑗]]:={𝐴,𝑓(𝑖)=𝑗,∅,otherwise, with the corresponding definition of ∃𝑓. The generic predicate is Σ:=P(𝐴) with 𝜎:=idP(𝐴) and {𝜑}𝐼:=𝜑. This is the structure of Hyland, Johnstone and Pitts, §1.7, physical page 7 (article page 211); the choice 𝐴 =ℕ with Kleene application gives the recursive realizability tripos of their §1.8(ii).
Referenced from 4 locations
In example 144.6, ≤𝐼 is reflexive and transitive.
Referenced from 2 locations
Proof of Proposition 144.7 — The realizability preorder
Proof. Reflexivity. For every 𝑏 ∈𝜑(𝑖) we have 𝑒 ⋅𝑏 ≍𝑏 ∈𝜑(𝑖), so 𝑒 ∈𝜑(𝑖) →𝜑(𝑖) for every 𝑖, and the single element 𝑒 witnesses 𝜑 ≤𝐼𝜑.
Transitivity. Suppose 𝑎 ∈𝜃(𝑖) →𝜑(𝑖) and 𝑏 ∈𝜑(𝑖) →𝜓(𝑖) for all 𝑖. Let 𝑐 ∈𝜃(𝑖). Then 𝑎 ⋅𝑐 ∈𝜑(𝑖) and 𝑏 ⋅(𝑎 ⋅𝑐) ∈𝜓(𝑖). Now ((𝑠⋅(𝑘⋅𝑏))⋅𝑎)⋅𝑐≍((𝑘⋅𝑏)⋅𝑐)⋅(𝑎⋅𝑐)≍𝑏⋅(𝑎⋅𝑐), using the 𝑠-equation and then the 𝑘-equation, so the single element (𝑠 ⋅(𝑘 ⋅𝑏)) ⋅𝑎 realizes 𝜃(𝑖) →𝜓(𝑖) for every 𝑖. ◻
The number produced in that proof does not depend on 𝑖. That is the whole force of (144.2): entailment in a realizability tripos is uniform realizability, one algorithm for all indices, and it is strictly stronger than pointwise entailment.
Let 𝐴 be an infinite Heyting algebra and let P𝐼 be the set of maps 𝐼 →𝐴 with finite image, with the pointwise structure. Clauses (i) and (ii) of definition 144.2 hold. A generic predicate would be a set Σ and 𝜎 ∈PΣ, that is, a map 𝜎 :Σ →𝐴 with finite image, such that every 𝜑 :𝐼 →𝐴 with finite image factors as 𝜎 ∘{𝜑}𝐼 up to ⊣⊢; taking 𝐼 =𝐴 and 𝜑 a map with image of cardinality larger than that of the image of 𝜎 makes the factorization impossible. So clause (iii) is not a consequence of the others. This is §1.6(iii) of the source, physical page 7.
Referenced from 2 locations
★☆☆ In the recursive realizability tripos compute 𝑝 →𝑞 for 𝑝 =∅ and for 𝑞 =∅, 𝑝 ≠∅. Which is all of ℕ and which is empty?
Referenced from 2 locations
★★☆ The source remarks that the simpler formula (∀𝑓𝜑)(𝑗)=⋂{𝜑(𝑖)∣𝑓(𝑖)=𝑗} fails to be right adjoint to 𝑓∗ when 𝑓 is not surjective (§1.8(i), physical page 8). Take 𝑓 :∅ →{ ∗} and exhibit the failure by computing both sides of the adjunction at 𝜑 the empty family.
Referenced from 2 locations
★☆☆ Verify that the powerset tripos of example 144.4 satisfies clause (ii)(b): 𝑓∗ preserves ⇒. Which proposition of chapter 143 was this?
Referenced from 2 locations
P-valued sets
Fix a tripos P. A first-order language is interpreted in P by the clauses of definition 143.22. A sort goes to a set; a relation symbol of sort (𝑋1,…,𝑋𝑛) goes to an element of the fiber over the product of those sets; the connectives and quantifiers go to the operations of definition 144.2. Write ⊢P𝜑 for validity, meaning ⊤ ≤[[𝜑]] in the fiber over the interpreted context. By proposition 144.3 and theorem 143.24, every derivable sequent of intuitionistic logic is valid. Every verification below appeals to that one fact.
A P-valued set is a pair (𝑋, =) consisting of a set 𝑋 and an element [[𝑥 =𝑥′]] ∈P(𝑋 ×𝑋) such that ⊢P∀𝑥,𝑥′(𝑥=𝑥′⇒𝑥′=𝑥),⊢P∀𝑥,𝑥′,𝑥″(𝑥=𝑥′∧𝑥′=𝑥″⇒𝑥=𝑥″). Its existence predicate is [[𝑥 ∈𝑋]]:=[[𝑥 =𝑥]] ∈P𝑋.
Referenced from 6 locations
Reflexivity is not required. An element 𝑥 of the underlying set with [[𝑥 =𝑥]] =⊥ is present in the set-theoretic carrier and absent from the object it presents; the carrier is scaffolding, and the predicate [[𝑥 ∈𝑋]] says how much of it survives. This is Definition 2.2 of Hyland, Johnstone and Pitts, physical page 11 (article page 215).
In the recursive realizability tripos take 𝑋:=ℕ and [[𝑛 =𝑚]]:={𝑎 ∣𝑎 =⟨𝑛,𝑚⟩} if 𝑛 and 𝑚 are related by a fixed partial equivalence relation 𝑅 on ℕ, and ∅ otherwise, where ⟨ −, −⟩ is a recursive pairing. Symmetry and transitivity of [[ ⋅ = ⋅]] hold with uniform realizers computing the pair swap and the composition of pairs, so this is a P-set exactly when 𝑅 is symmetric and transitive. Its existence predicate is inhabited at 𝑛 exactly when 𝑛𝑅𝑛, that is, on the domain of 𝑅. The reflexivity that definition 144.10 omits is the reflexivity that a partial equivalence relation omits.
Referenced from 4 locations
Let (𝑋, =) and (𝑌, =) be P-sets, with the product 𝑋 ×𝑌 made into a P-set by [[(𝑥,𝑦) =(𝑥′,𝑦′)]]:=[[𝑥 =𝑥′]] ∧[[𝑦 =𝑦′]]. An element 𝑅 ∈P𝑋 is a relation on (𝑋, =) when ⊢P∀𝑥,𝑥′ (𝑥 =𝑥′ ∧𝑅(𝑥) ⇒𝑅(𝑥′)), and it is strict when in addition ⊢P∀𝑥 (𝑅(𝑥) ⇒𝑥 ∈𝑋). A relation 𝐹 on 𝑋 ×𝑌 is functional when it is strict and ⊢P∀𝑥,𝑦,𝑦′(𝐹(𝑥,𝑦)∧𝐹(𝑥,𝑦′)⇒𝑦=𝑦′)(single-valued),⊢P∀𝑥(𝑥∈𝑋⇒∃𝑦𝐹(𝑥,𝑦))(total). Two functional relations 𝐹,𝐺 are equivalent when ⊢P∀𝑥,𝑦 (𝐹(𝑥,𝑦) ⇔𝐺(𝑥,𝑦)).
Referenced from 6 locations
Equivalence of functional relations is an equivalence relation by soundness. For the transitivity of the relation itself one needs only that ⇔ is intuitionistically transitive.
𝐒𝐞𝐭[P] has the P-sets as objects and, as arrows (𝑋, =) ⟶(𝑌, =), the equivalence classes of functional relations on 𝑋 ×𝑌. The identity on (𝑋, =) is the class of [[𝑥 =𝑥′]], and the composite of the classes of 𝐹 on 𝑋 ×𝑌 and 𝐺 on 𝑌 ×𝑍 is the class of [[∃𝑦(𝐹(𝑥,𝑦)∧𝐺(𝑦,𝑧))]]∈P(𝑋×𝑍).
Referenced from 4 locations
Hyland, Johnstone and Pitts write P-𝐒𝐞𝐭 for this category; the notation 𝐒𝐞𝐭[P] follows Pitts’s thesis, where the base is allowed to vary.
Definition 144.13 is well posed: the composite of two functional relations is functional, its class depends only on the two classes, the identities are two-sided units, and composition is associative.
Referenced from 3 locations
Proof of Lemma 144.14 — [ P] is a category
Proof. Every clause is an intuitionistic deduction from the defining formulas, valid by soundness.
The composite is functional. Strictness: from 𝐹(𝑥,𝑦) strict, 𝐹(𝑥,𝑦) ∧𝐺(𝑦,𝑧) ⇒𝑥 ∈𝑋 ∧𝑧 ∈𝑍. Single-valuedness: from ∃𝑦(𝐹(𝑥,𝑦) ∧𝐺(𝑦,𝑧)) and ∃𝑦′(𝐹(𝑥,𝑦′) ∧𝐺(𝑦′,𝑧′)), single-valuedness of 𝐹 gives 𝑦 =𝑦′; 𝐺 is a relation, so 𝐺(𝑦′,𝑧′) and 𝑦 =𝑦′ give 𝐺(𝑦,𝑧′); then single-valuedness of 𝐺 gives 𝑧 =𝑧′. Totality: from 𝑥 ∈𝑋, totality of 𝐹 gives some 𝑦 with 𝐹(𝑥,𝑦); strictness of 𝐹 gives 𝑦 ∈𝑌; totality of 𝐺 gives some 𝑧 with 𝐺(𝑦,𝑧).
Independence of representatives. If 𝐹 ⇔𝐹′ and 𝐺 ⇔𝐺′ then ∃𝑦(𝐹 ∧𝐺) ⇔∃𝑦(𝐹′ ∧𝐺′) by congruence of the connectives.
Units. The composite of [[𝑥 =𝑥′]] with 𝐹 is ∃𝑥′(𝑥 =𝑥′ ∧𝐹(𝑥′,𝑦)). From 𝑥 =𝑥′ and 𝐹(𝑥′,𝑦) and the fact that 𝐹 respects equality in its first argument, 𝐹(𝑥,𝑦) follows; and conversely 𝐹(𝑥,𝑦) gives 𝑥 ∈𝑋 by strictness, hence 𝑥 =𝑥, hence the existential with witness 𝑥. The other unit law is the same argument on the second argument.
Associativity. Both composites are equivalent to ∃𝑦∃𝑧 (𝐹(𝑥,𝑦) ∧𝐺(𝑦,𝑧) ∧𝐻(𝑧,𝑤)), by the intuitionistic equivalence ∃𝑧(∃𝑦(𝐹∧𝐺)∧𝐻)⇔∃𝑦(𝐹∧∃𝑧(𝐺∧𝐻)), which holds because 𝐹 does not contain 𝑧 and 𝐻 does not contain 𝑦. ◻
Lemma 144.14 is Lemma 2.5 of the source, physical pages 12–13. Its proof is reproduced here rather than cited because every later verification in this chapter has the same shape: write the set-theoretic definition as a formula, and check it intuitionistically.
★★☆ Show that the unit law fails if strictness is dropped from definition 144.12: exhibit a P-set and a single-valued total relation 𝐹 that does not satisfy 𝐹(𝑥,𝑦) ⇒𝑥 ∈𝑋, for which ∃𝑥′(𝑥 =𝑥′ ∧𝐹(𝑥′,𝑦)) is not equivalent to 𝐹(𝑥,𝑦).
Referenced from 2 locations
★★☆ Continue example 144.11. For two partial equivalence relations 𝑅,𝑆 on ℕ, describe the functional relations from (ℕ,𝑅) to (ℕ,𝑆) concretely, and show that each is realized by a partial recursive function tracking 𝑅-classes to 𝑆-classes.
Referenced from 2 locations
The topos
𝐒𝐞𝐭[P] has a terminal object, binary products, and equalizers, hence all finite limits by theorem 142.15.
Referenced from 3 locations
Proof of Lemma 144.15 — Finite limits
Proof. Terminal object. Let 1 be a one-element set with [[ ∗ = ∗]]:=⊤. For any (𝑋, =) the existence predicate [[𝑥 ∈𝑋]], read as an element of P(𝑋 ×1), is strict, single-valued (its second component has one value) and total, so it is functional. If 𝐹 is any functional relation 𝑋 →1 then totality gives 𝑥 ∈𝑋 ⇒𝐹(𝑥, ∗) and strictness gives 𝐹(𝑥, ∗) ⇒𝑥 ∈𝑋, so 𝐹 is equivalent to it.
Products. The product P-set is the one named in definition 144.12. The projections are the classes of [[𝑥=𝑥′∧𝑦∈𝑌]]∈P(𝑋×𝑌×𝑋),[[𝑥∈𝑋∧𝑦=𝑦′]]∈P(𝑋×𝑌×𝑌), and the pairing of 𝑓 :𝑍 ⟶𝑋 and 𝑔 :𝑍 ⟶𝑌 is the class of [[𝐹(𝑧,𝑥) ∧𝐺(𝑧,𝑦)]]. Functionality and the two equations of (142.2) are intuitionistic deductions from definition 144.12; for uniqueness, a functional 𝐻 on 𝑍 ×𝑋 ×𝑌 whose composites with the projections are 𝐹 and 𝐺 satisfies 𝐻(𝑧,𝑥,𝑦) ⇔𝐹(𝑧,𝑥) ∧𝐺(𝑧,𝑦), the direction from left to right by composing and the converse by single-valuedness of 𝐻 together with totality.
Equalizers. Let 𝑓,𝑔 :𝑋 ⟶𝑌 with representatives 𝐹,𝐺. Let 𝐸 have underlying set 𝑋 and [[𝑥∈𝐸]]:=[[∃𝑦(𝐹(𝑥,𝑦)∧𝐺(𝑥,𝑦))]],[[𝑥=𝐸𝑥′]]:=[[𝑥=𝑋𝑥′∧𝑥∈𝐸∧𝑥′∈𝐸]], and let ℎ :𝐸 ⟶𝑋 be the class of [[𝑥 ∈𝐸 ∧𝑥 =𝑋𝑥′]]. Then [[ ⋅ =𝐸 ⋅]] is symmetric and transitive because [[ ⋅ =𝑋 ⋅]] is, and ℎ is functional. From the definition of 𝐸, 𝑓 ∘ℎ =𝑔 ∘ℎ. Let 𝑘 :𝑍 ⟶𝑋 satisfy 𝑓 ∘𝑘 =𝑔 ∘𝑘, so that ⊢P∀𝑧,𝑥,𝑦(𝐾(𝑧,𝑥)∧𝐹(𝑥,𝑦)⇒𝐺(𝑥,𝑦)). Since 𝐹 is total, 𝐾(𝑧,𝑥) ⇒∃𝑦(𝐹(𝑥,𝑦) ∧𝐺(𝑥,𝑦)), that is, 𝐾(𝑧,𝑥) ⇒𝑥 ∈𝐸. So 𝐾 is still strict as a relation on 𝑍 ×𝐸, hence functional there, and defines the unique factorization ¯𝑘 :𝑍 ⟶𝐸 with ℎ ∘¯𝑘 =𝑘. ◻
An arrow 𝑓 :𝑋 ⟶𝑌 of 𝐒𝐞𝐭[P] is a monomorphism in the sense of definition 141.28 if and only if ⊢P∀𝑥,𝑥′,𝑦(𝐹(𝑥,𝑦)∧𝐹(𝑥′,𝑦)⇒𝑥=𝑥′) for some, equivalently any, representative 𝐹.
Referenced from 3 locations
Proof of Lemma 144.17 — Monomorphisms
Proof. Suppose the displayed formula holds and let 𝑢,𝑣 :𝑍 ⟶𝑋 with 𝑓 ∘𝑢 =𝑓 ∘𝑣, that is, ∃𝑥(𝑈(𝑧,𝑥) ∧𝐹(𝑥,𝑦)) ⇔∃𝑥(𝑉(𝑧,𝑥) ∧𝐹(𝑥,𝑦)). Let 𝑈(𝑧,𝑥). By strictness 𝑥 ∈𝑋, by totality of 𝐹 there is 𝑦 with 𝐹(𝑥,𝑦), so the left side holds; hence there is 𝑥′ with 𝑉(𝑧,𝑥′) and 𝐹(𝑥′,𝑦), and the hypothesis gives 𝑥 =𝑥′. Since 𝑉 respects equality, 𝑉(𝑧,𝑥). By symmetry of the argument 𝑈 ⇔𝑉, so 𝑢 =𝑣.
Conversely suppose 𝑓 is a monomorphism. Let 𝑃 be the P-set with underlying set 𝑋 ×𝑋 and [[(𝑥1,𝑥2) ∈𝑃]]:=[[∃𝑦(𝐹(𝑥1,𝑦) ∧𝐹(𝑥2,𝑦))]], with equality inherited from 𝑋 ×𝑋 and restricted to 𝑃 as in the equalizer construction. The two projections 𝑃 ⟶𝑋 are functional, and composing either with 𝑓 gives the same arrow, by the definition of 𝑃. Monicity forces the two projections to be equal, which is exactly the displayed formula. ◻
Let 𝐴 be a strict relation on a P-set (𝑋, =𝑋). Let ‖𝐴‖ be the P-set with underlying set 𝑋, [[𝑥 ∈‖𝐴‖]]:=[[𝐴(𝑥)]] and [[𝑥 =𝐴𝑥′]]:=[[𝑥 =𝑋𝑥′ ∧𝑥 ∈‖𝐴‖ ∧𝑥′ ∈‖𝐴‖]], and let 𝑚𝐴 :‖𝐴‖ ⟶𝑋 be the class of [[𝑎 ∈‖𝐴‖ ∧𝑎 =𝑋𝑥]].
Referenced from 3 locations
Every monomorphism 𝑓 :𝑌 ⟶𝑋 of 𝐒𝐞𝐭[P] factors as 𝑚𝐴 ∘¯𝑓 with ¯𝑓 an isomorphism, where [[𝐴(𝑥)]]:=[[∃𝑦 𝐹(𝑦,𝑥)]]. Moreover, for 𝑓 :𝑌 ⟶𝑋 and a strict relation 𝐴 on 𝑋, the square with vertical arrows 𝑚𝑓−1𝐴 and 𝑚𝐴, where [[𝑓−1𝐴(𝑦)]]:=[[∃𝑥 (𝐹(𝑦,𝑥) ∧𝐴(𝑥))]], is a pullback.
Referenced from 4 locations
Proof of Lemma 144.19 — Subobjects are canonical
Proof. 𝐴 is strict because 𝐹 is. The relation 𝐹, read on 𝑌 ×‖𝐴‖, is functional in both directions: it is functional from 𝑌 by hypothesis, and single-valued in the other direction by lemma 144.17, total by the definition of 𝐴; so it is an isomorphism ¯𝑓 with 𝑚𝐴 ∘¯𝑓 =𝑓. For the second claim, 𝑓−1𝐴 is strict because 𝐹 is, the top arrow of the square is the restriction of 𝑓, represented by [[𝐹(𝑦,𝑥) ∧𝐴(𝑥)]], and the pullback property is the intuitionistic statement that a 𝑧 mapping into 𝑋 through 𝑚𝐴 and into 𝑌 compatibly is exactly a 𝑧 mapping into ‖𝑓−1𝐴‖. ◻
These are Lemmas 2.9–2.11 of the source, physical pages 14–15. The factorization is called canonical rather than unique on purpose: if ⊢P∀𝑥 (𝐴(𝑥) ⇔𝐵(𝑥)) then ‖𝐴‖ and ‖𝐵‖ are isomorphic over 𝑋 without being equal, which is again remark 144.16.
Let (𝑋, =) be a P-set and let Σ be the index set of the generic predicate. Define P𝑋 to have underlying set Σ𝑋, with [[𝑅∈P𝑋]]:=[[∀𝑥,𝑥′(𝑥∈𝑋𝑅∧𝑥=𝑥′⇒𝑥′∈𝑋𝑅)]]∧[[∀𝑥(𝑥∈𝑋𝑅⇒𝑥∈𝑋)]],[[𝑅=P𝑋𝑆]]:=[[𝑅∈P𝑋∧𝑆∈P𝑋∧∀𝑥(𝑥∈𝑋𝑅⇔𝑥∈𝑋𝑆)]], where ∈𝑋 ∈P(𝑋 ×Σ𝑋) is the membership predicate ev∗𝑋(𝜎) for the evaluation map ev𝑋 :𝑋 ×Σ𝑋 →Σ. Then P𝑋 is a P-set and there is a bijection, natural in 𝑌, hom𝐒𝐞𝐭[P](𝑌,P𝑋)≅Sub(𝑋×𝑌), where Sub denotes the set of subobjects.
Referenced from 4 locations
Proof of Theorem 144.20 — Power objects
Proof. Symmetry and transitivity of =P𝑋 follow from those of ⇔. Let 𝐸 ∈P(𝑋 ×P𝑋) be [[𝑅 ∈P𝑋 ∧𝑥 ∈𝑋𝑅]], a strict relation, and let ‖𝐸‖ ⟶𝑋 ×P𝑋 be the associated canonical monomorphism. Sending 𝑓 :𝑌 ⟶P𝑋 to the subobject ‖(id𝑋 ×𝑓)−1𝐸‖ is natural in 𝑌 by lemma 144.19, so it remains to prove bijectivity.
Surjectivity. Let a subobject of 𝑋 ×𝑌 be given; by lemma 144.19 it is ‖𝐴‖ for a strict relation 𝐴 on 𝑋 ×𝑌. Clause (iii) of definition 144.2, applied in the form of the membership predicate, supplies a function 𝑔 :𝑌 →Σ𝑋 in 𝐒𝐞𝐭 with (id𝑋 ×𝑔)∗( ∈𝑋) ⊣⊢𝐴 in P(𝑋 ×𝑌). Put [[𝐹(𝑦,𝑅)]]:=[[𝑦∈𝑌∧𝑔(𝑦)=P𝑋𝑅]]. Because 𝐴 is strict, 𝑦 ∈𝑌 ⊢P𝑔(𝑦) ∈P𝑋, and 𝐹 is then functional, so it represents an arrow 𝑓 :𝑌 ⟶P𝑋. Unfolding, 𝐴(𝑥,𝑦) ⇔∃𝑅 (𝐹(𝑦,𝑅) ∧𝐸(𝑥,𝑅)), so ‖𝐴‖ is the subobject assigned to 𝑓.
Injectivity. Suppose 𝑓,𝑓′ are assigned the same subobject. Then ∃𝑅(𝐹(𝑦,𝑅) ∧𝐸(𝑥,𝑅)) ⇔∃𝑅(𝐹′(𝑦,𝑅) ∧𝐸(𝑥,𝑅)). Fix 𝑦 ∈𝑌; totality gives 𝑅 with 𝐹(𝑦,𝑅) and 𝑅′ with 𝐹′(𝑦,𝑅′), and the displayed equivalence gives ∀𝑥 (𝑥 ∈𝑋𝑅 ⇔𝑥 ∈𝑋𝑅′). Both lie in P𝑋, so 𝑅 =P𝑋𝑅′, and since 𝐹′ respects equality, 𝐹(𝑦,𝑅) ⇒𝐹′(𝑦,𝑅). By symmetry 𝐹 ⇔𝐹′, so 𝑓 =𝑓′. ◻
𝐒𝐞𝐭[P] has finite limits and power objects, hence is an elementary topos. Its subobject classifier is the P-set Ω with underlying set Σ and [[𝑝 =Ω𝑞]]:=[[𝑝 ⇔𝑞]], and the exponential 𝑌𝑋 has underlying set Σ𝑋×𝑌 with [[𝐹 ∈𝑌𝑋]] the formula asserting that 𝐹 is a functional relation and [[𝐹 =𝐺]]:=[[𝐹 ∈𝑌𝑋 ∧𝐺 ∈𝑌𝑋 ∧∀𝑥,𝑦 ((𝑥,𝑦) ∈𝐹 ⇔(𝑥,𝑦) ∈𝐺)]].
Referenced from 7 locations
Proof of Corollary 144.21 — [ P] is a topos
Proof. Lemma 144.15 and theorem 144.20 give the two clauses of the definition of an elementary topos. The subobject classifier is the power object of the terminal P-set: taking 𝑋 =1 in theorem 144.20 gives Σ1 =Σ and the displayed equality, and the bijection becomes hom𝐒𝐞𝐭[P](𝑌,Ω) ≅Sub(𝑌). The exponential is obtained from the power object of 𝑋 ×𝑌 by restricting along the strict relation asserting functionality, which is definition 144.18 applied to that relation. ◻
Corollary 144.21 is Theorem 2.13 and item 2.14 of the source, physical pages 16–17. Nothing about Grothendieck toposes, sheaves or sites is used or claimed; “topos” here means exactly finite limits plus power objects, and the two constructions above are the only ones this chapter exports.
One object of the realizability topos
Fix 𝐴 =ℕ with Kleene application and let P be the recursive realizability tripos of example 144.6. Fix a recursive pairing ⟨ −, −⟩ with recursive inverses fst,snd, and record the three operations used below, each stated up to ⊣⊢: (𝜑∧𝜓)(𝑖)={⟨𝑎,𝑏⟩∣𝑎∈𝜑(𝑖), 𝑏∈𝜓(𝑖)},(𝜑⇒𝜓)(𝑖)=𝜑(𝑖)→𝜓(𝑖)as in (144.1),(∃𝑝𝜑)(𝑛)=⋃𝑚𝜑(𝑛,𝑚)for the projection 𝑝:ℕ2→ℕ.
Let 𝑁 have underlying set ℕ and [[𝑛=𝑚]]:={{𝑛},𝑛=𝑚,∅,𝑛≠𝑚.
Referenced from 4 locations
𝑁 is a P-set: symmetry is realized by 𝑒, since [[𝑛 =𝑚]] and [[𝑚 =𝑛]] are the same set; transitivity is realized by the recursive function 𝑝 ↦fst 𝑝, because a realizer of the conjunction is a pair ⟨𝑛,𝑚⟩ with 𝑛 =𝑚 =𝑘 and the required realizer of 𝑛 =𝑘 is 𝑛. Its existence predicate is [[𝑛 ∈𝑁]] ={𝑛}, which is inhabited for every 𝑛.
The arrows 𝑁 ⟶𝑁 of 𝐒𝐞𝐭[P] are in bijection with the total recursive functions ℕ →ℕ.
Referenced from 5 locations
Proof of Theorem 144.23 — Endomorphisms of N
Proof. From a recursive function to an arrow. Let 𝑢 be total recursive. Put [[𝐹𝑢(𝑛,𝑚)]]:={⟨𝑛,𝑚⟩} if 𝑢(𝑛) =𝑚 and ∅ otherwise. It is strict: from ⟨𝑛,𝑚⟩ the identity computes a realizer of 𝑛 ∈𝑁 ∧𝑚 ∈𝑁, which is the same pair. It is single-valued: if [[𝐹𝑢(𝑛,𝑚)]] and [[𝐹𝑢(𝑛,𝑚′)]] are both inhabited then 𝑚 =𝑢(𝑛) =𝑚′, and from the realizer ⟨⟨𝑛,𝑚⟩,⟨𝑛,𝑚′⟩⟩ of the conjunction the recursive function 𝑞 ↦snd(fst 𝑞) returns 𝑚, a realizer of [[𝑚 =𝑚′]]. It is total: by (144.3) a realizer of ∃𝑚 𝐹𝑢(𝑛,𝑚) at 𝑛 is any element of ⋃𝑚[[𝐹𝑢(𝑛,𝑚)]] ={⟨𝑛,𝑢(𝑛)⟩}, and the recursive function 𝑛 ↦⟨𝑛,𝑢(𝑛)⟩ produces one uniformly.
From an arrow to a recursive function. Let 𝐹 be functional. Strictness gives a number 𝑠 with 𝑠⋅𝑐∈[[𝑛∈𝑁]]×[[𝑚∈𝑁]]coded as ⟨𝑛,𝑚⟩,for every 𝑐∈[[𝐹(𝑛,𝑚)]], so from any realizer of 𝐹(𝑛,𝑚) the recursive operation 𝑐 ↦snd(𝑠 ⋅𝑐) returns 𝑚. Totality gives a number 𝑎 with 𝑎 ⋅𝑛 ∈⋃𝑚[[𝐹(𝑛,𝑚)]] for every 𝑛; in particular 𝑎 ⋅𝑛 is defined for every 𝑛. Define 𝑢𝐹(𝑛):=snd(𝑠⋅(𝑎⋅𝑛)). This is a composition of total operations, hence total recursive. The set [[𝐹(𝑛,𝑢𝐹(𝑛))]] is inhabited, and 𝑢𝐹(𝑛) is the only value with that property. For suppose [[𝐹(𝑛,𝑚)]] is inhabited. Then single-valuedness produces a realizer of 𝑚 =𝑢𝐹(𝑛), and by definition 144.22 that set is nonempty only for 𝑚 =𝑢𝐹(𝑛).
The two passages are mutually inverse. Given 𝐹, the relations 𝐹 and 𝐹𝑢𝐹 are equivalent: the direction 𝐹(𝑛,𝑚) ⇒𝐹𝑢𝐹(𝑛,𝑚) is realized by 𝑐 ↦𝑠 ⋅𝑐, which returns ⟨𝑛,𝑚⟩ and is applicable exactly when [[𝐹(𝑛,𝑚)]] is inhabited, in which case 𝑢𝐹(𝑛) =𝑚; the converse direction is realized by 𝑞 ↦𝑎 ⋅(fst 𝑞), which from ⟨𝑛,𝑚⟩ with 𝑢𝐹(𝑛) =𝑚 returns an element of [[𝐹(𝑛,𝑚)]]. Conversely 𝑢𝐹𝑢 =𝑢, since [[𝐹𝑢(𝑛,𝑚)]] is inhabited exactly when 𝑚 =𝑢(𝑛).
Finally the assignment is injective on total recursive functions: if 𝑢 ≠𝑢′, choose 𝑛 with 𝑢(𝑛) ≠𝑢′(𝑛); then [[𝐹𝑢(𝑛,𝑢(𝑛))]] is inhabited and [[𝐹𝑢′(𝑛,𝑢(𝑛))]] is empty, so no realizer of ∀𝑛,𝑚 (𝐹𝑢 ⇔𝐹𝑢′) exists. ◻
The base category of the tripos was 𝐒𝐞𝐭, whose arrows ℕ →ℕ are all functions. The category built from it has, at the same underlying set, exactly the computable ones. That is the sense in which the construction internalizes realizability: the computational content of (144.2) has moved from the fibers into the arrows.
The universal property, as an import
The construction P ↦𝐒𝐞𝐭[P] has a characterization, and this chapter states it without proving it, because its proof needs the theory of geometric morphisms and partial-map classifiers, which this book does not develop.
Let C be a finitely complete category, E a topos, and Δ :C →E a left exact functor. The following are equivalent.
Δ is equivalent over C to ΔP :C →C[P] for some C-tripos P.
For each object 𝐴 of E there are an object ˆ𝐴 of C and a map 𝛽𝐴 :Δˆ𝐴 ⟶˜𝐴 in E, where ˜𝐴 is the partial-map classifier of 𝐴, such that every 𝑓 :Δ𝑋 ⟶˜𝐴 factors as 𝛽𝐴 ∘Δ𝑔 for some 𝑔 :𝑋 ⟶ˆ𝐴 in C; and every 𝛽𝐴 is an epimorphism.
Referenced from 5 locations
This is Theorem 3.10 of Pitts, The theory of triposes, PhD thesis, University of Cambridge 1981, physical page 43 of the author archive copy (thesis page 39); the accompanying Proposition 3.11, physical pages 44–45, adds that under the same hypotheses there is a hyperconnected geometric morphism E ⟶C[P] for P =SubE ∘Δop. What theorem 144.25 supplies here is a criterion: a topos arises from a tripos over C exactly when every object is a subquotient of something in the image of Δ, uniformly. What is proved locally in this chapter is corollary 144.21 and theorem 144.23; nothing in theorem 144.25 is used to prove either.
Suggested first pass.
Begin with exercise 144.6 and exercise 144.7, then complete exercise 144.10.
★☆☆ Show that in 𝐒𝐞𝐭[P] the P-set with empty underlying set is initial, and that the P-set with underlying set { ∗} and [[ ∗ = ∗]] =⊥ is isomorphic to it. Which clause of definition 144.10 permits the second object at all?
Referenced from 3 locations
★★☆ In the recursive realizability tripos compute the underlying set of the subobject classifier Ω of corollary 144.21 and its equality predicate. Then exhibit two subsets 𝑝,𝑞 ⊆ℕ with [[𝑝 =Ω𝑞]] =∅ although 𝑝 and 𝑞 are both nonempty, and explain what this says about the arrows 1 ⟶Ω.
Referenced from 3 locations
★★★ Show that Ω in the recursive realizability topos is not the two-element object: exhibit a subobject of 𝑁 that is not complemented, using a set 𝑇 ⊆ℕ that is recursively enumerable but not recursive. State precisely which of ⊤ ≤𝑝 ∨¬𝑝 fails and at which index, and check that your failure is a failure of uniform realizability rather than of pointwise inhabitation.
Referenced from 2 locations
★★★ Prove that the object 𝑁 of definition 144.22 is a natural numbers object: exhibit arrows 𝑧 :1 ⟶𝑁 and 𝑠 :𝑁 ⟶𝑁 and show that for every 𝑋 with 𝑥0 :1 ⟶𝑋 and 𝑡 :𝑋 ⟶𝑋 there is exactly one ℎ :𝑁 ⟶𝑋 with ℎ ∘𝑧 =𝑥0 and ℎ ∘𝑠 =𝑡 ∘ℎ. Use primitive recursion to produce the realizer for ℎ, and identify where single-valuedness is needed for uniqueness.
Referenced from 2 locations
★★★ Practical project.tripos-functional-relation-checker Implement a checker for functional relations over a finite partial applicative structure. The input is: a finite carrier 𝐴 given as a list; a partial application table for 𝐴, given as a list of triples (𝑎,𝑏,𝑐) meaning 𝑎 ⋅𝑏 =𝑐, with absent pairs undefined; nominated elements 𝑒,𝑘,𝑠; two finite P-sets (𝑋, =𝑋) and (𝑌, =𝑌), each given by its underlying finite set together with a table assigning a subset of 𝐴 to every pair of elements; and a candidate relation 𝐹 given as a table assigning a subset of 𝐴 to every pair in 𝑋 ×𝑌.
Invariant. Before any logical check, the program verifies that the nominated 𝑒,𝑘,𝑠 satisfy the three equations of definition 144.5 on the given table, and that =𝑋 and =𝑌 are symmetric and transitive in the sense of definition 144.10 with uniform realizers, that is, with a single element of 𝐴 witnessing the implication at every index. It rejects the input if either check fails, naming the failing equation or index.
Concrete result. The program prints, for each of the three clauses of definition 144.12 — strict, single-valued, total — either realized together with a witnessing element of 𝐴, or unrealized together with the index at which every candidate element fails. It then prints functional or not functional.
Acceptance test. Take 𝐴 ={0,1,2} with a table making 0 act as the identity on all of 𝐴 and 1,2 nowhere defined, and 𝑒 =𝑘 =𝑠 =0; take 𝑋 =𝑌 ={ ∙} with [[ ∙ = ∙]] ={0} in both. The relation 𝐹( ∙, ∙) ={0} must print realized three times and functional; the relation 𝐹( ∙, ∙) =∅ must print unrealized for totality, with index ∙, and not functional. Then repeat with 𝑋 of two elements whose equality predicate is {0} on the diagonal and ∅ off it, and a relation sending both elements of 𝑋 to the same element of 𝑌; it must print functional. A run that reports totality realized for the empty relation has quantified the realizer inside the index rather than outside it, which is the distinction of (144.2).
Referenced from 3 locations
Sources. Triposes, P-valued sets, and the construction of the associated topos are due to J. M. E. Hyland, P. T. Johnstone and A. M. Pitts, Tripos theory, Mathematical Proceedings of the Cambridge Philosophical Society 88 (1980), 205–232. Definition 144.1 and definition 144.2 are their Definitions 1.1 and 1.2 (physical page 3 of the author archive copy); the realizability tripos is their §1.7 (physical page 7) and the recursive case their §1.8(ii) (physical page 8); the example without a generic predicate is their §1.6(iii) (physical page 7). Definition 144.10 through corollary 144.21 follow their §2: Definitions 2.2–2.4 and Lemma 2.5 on physical pages 11–13, finite limits and the choice caveat in Lemma 2.6 and Remark 2.7 on physical pages 13–14, the monomorphism and canonical-subobject lemmas 2.9–2.11 on physical pages 14–15, the power object in Proposition 2.12 and the topos theorem 2.13 on physical page 16, and the exponential and subobject classifier in 2.14 on physical page 17. The longer development, with the universal characterization quoted as theorem 144.25, is A. M. Pitts, The theory of triposes, PhD thesis, University of Cambridge 1981, Theorem 3.10 and Proposition 3.11 on physical pages 43–45. The effective topos and its realizability objects are developed by Hyland [Hyl82]; the step-by-step decomposition of the tripos-to-topos passage is Pasquali [Pas14]; a proof-bearing modern route through realizability, categorical structure and PER models is De Jong [dJ25], and the fibrational background is Jacobs [Jac99].