Now we develop a λcalculus for S, just as Section A 8 did for SS.
The new calculus is based on a typetheoretic presentation [Tay99, Section 2.2] of Zermelo’s original set theory, with Σ^{X} playing the role of the powerset (℘ X) and the object {X ∣ E} from Section 4 that of comprehension. Whereas comprehension is often presented in a way that allows each term to belong to many types, the new operators admit, i and I in our calculus, whilst perhaps being a little bureaucratic, ensure that each term has a unique type.
Writing D for the category obtained from the new calculus as explained in [Tay99, Sections 4.3 & 4.7] and more briefly in Remark A 2.7, we shall show in the following sections that S≃D. This will be done by means of a weak normalisation theorem, thereby showing that we have stated enough equations. It is a categorical equivalence, rather than the isomorphism that we had for SS, because we’re now manipulating types.
Remark 8.1 In the calculus that we have in mind for set theory,
the rules for the powerset ℘ X≡Ω^{X}
are those of the restricted λcalculus,
where ξ[a] means a∈{X ∣ ξ}.
Then comprehension has formation and introduction rules,
elimination rules,
x:{X ∣ ξ} ⊢ i_{X,ξ} x:X x:{X ∣ ξ} ⊢ ξ[i_{X,ξ} x] 
and β and ηrules
x:{X ∣ ξ} ⊢ x=admit( i_{X,ξ} x). 
The intent of these rules is to specify when there is a term admita that makes the triangle commute:
Notice that we have required ξ:℘ X to be a closed term (defined in the empty context), because we do not want to get involved in dependent types in this paper.
Remark 8.2 The rules that we give below for our own monadic situation
are not very pretty if seen as a piece of pure λcalculus.
But they are in the spirit of the treatment of comprehension above,
so long as we read the the typeformation rule as
where any predicate ξ:℘ X provides subtype data in set theory, and the nucleus E (Definition 4.3) does so for our own calculus. Similarly, the introduction rule means
where our admissibility condition is unfortunately more complicated and less intuitive than that in set theory.
You may think of
{X ∣ E} as {x:X ∣ ∀φ:Σ^{X}.Eφ x ⇔ φ x}, 
but this can only be internalised if Σ^{X} is compact (so ∀φ:Σ^{X} is meaningful) and Σ is discrete (so ⇔ is internal). These conditions (along with what is needed in Example 2.6(a) to define I_{X,E}θ in terms of ∃) would make S into a topos (Theorem C 11.12), and thereby bring the comprehension calculus back to that for Zermelo type theory.
Remark 8.3 As we have learned throughout this paper,
we need to be explicit about the subspace topology.
The elimination rule for elements ({}E_{0}) below
provides the restriction of an open subset φ
of X to the subspace {X ∣ E},
which we may reinterpret as the introduction rule for predicates,
For the corresponding elimination rule, we need a new operator I_{X,E} to expand an open subset θ of the subspace to the whole space.
For reference, we repeat Definition A 2.1,A 8.1,A 8.2 and 4.3.
Definition 8.4 The restricted λcalculus
has just the typeformation rules
1 type 
but with the normal rules for λabstraction and application,
together with the usual α, β and η rules.
Definition 8.5
Γ⊢ P:Σ^{ΣX} is prime if Γ, F:Σ^{3} X ⊢ F P ⇔
P(λ x.F(λφ.φ x)).
Definition 8.6 The sober λcalculus has the additional rules
focusI 
focusβ 
T_{0} 
Definition 8.7 φ:Σ^{Y}⊢ Eφ:Σ^{Y}
is called a nucleus if
F:Σ^{3} Y ⊢ E(λ y.F(λφ.Eφ y)) = E(λ y.F(λφ.φ y)). 
Definition 8.8 The {}rules of the monadic λcalculus
define the subspace itself.
 F 
 I 
x:{X ∣ E} ⊢ i_{X,E} x:X 
 E_{0} 
x:{X ∣ E}, φ:Σ^{X} ⊢ φ(i_{X,E} x) ⇔ Eφ(i_{X,E} x) 
 E_{1} 
 β 
x:{X ∣ E} ⊢ x=admit_{X,E}(i_{X,E} x) 
 η 
Definition 8.9 The Σ^{{}}rules say that it has the subspace topology,
where I_{X,E} expands open subsets of the subspace to the whole space.
θ:Σ^{{X ∣ E}} ⊢ I_{X,E}θ:Σ^{X} Σ 
 E 
The βrule says that the composite Σ^{X}↠Σ^{{X ∣ E}}↣Σ^{X} is E:
φ:Σ^{X} ⊢ I_{X,E}(λ x:{X ∣ E}.φ(i_{X,E} x)) = Eφ Σ 
 β 
Notice that this is the only rule that introduces E into the λexpressions. The ηrule, which we first saw in Remark 2.8, says that the other composite Σ^{{X ∣ E}}↣Σ^{X}↠Σ^{{X ∣ E}} is the identity:
θ:Σ^{{X ∣ E}}, x:{X ∣ E} ⊢ θ x ⇔ I_{X,E}θ(i_{X,E} x) Σ 
 η. 
In any type theory where terms are embedded in the definitions of types, we must check that, when two terms are equal according to the rules of the calculus, they give rise to interchangeable types. This result has the flavour of the normalisation proof that follows (Proposition 9.11), whilst being a lot simpler, so you may find it helpful to fill in the details of the verifications as a preparatory exercise.
Lemma 8.10
If E_{1}=E_{2} then
there is an isomorphism {X ∣ E_{1}}≅{X ∣ E_{2}}
that commutes with the structure (admit, i and I).
Proof The isomorphism for values is x_{1}↦admit_{2}(i_{1} x_{1}) and vice versa. This is well formed, i.e. the side condition for {}I is satisfied and justifies the use of admit_{2}, because of the equation E_{1}=E_{2}. The isomorphism for properties is θ_{1}↦Σ^{i2}(I_{1}θ_{1}). The equations for the isomorphisms and commutativity with the structure follow easily from the β and ηrules for the two sides. ▫
Before embarking on the main normalisation theorem, we investigate some of the interactions between the new admit operation and the underlying sober and recursive structures. The first result is the symbolic analogue of Remark 4.11, showing that admit does the same for a general Σsplit inclusion as focus does for η.
Lemma 8.11
The standard resolution defines an isomorphism
where E≡η_{ΣX}·Σ^{ηX}.
Proof The term x:X⊢admit(λφ.φ x) is well formed because of the unit law. The right hand side of Definition 8.5 is EF P, so the subspace {Σ^{2} X ∣ E} exactly captures the primes and
P:{Σ^{2} X ∣ E} ⊢ focus(i P):X 
is well formed. Then focus(i(admit(λφ.φ x))) = focus(λφ.φ x) = x by {}β and focusη. Conversely, admit(η_{X}(focus(i P))) = admit(i P) = P by focusβ and {}η. ▫
The interaction between admit and substitution, i.e. cut elimination, is as expected, cf. Lemma A 8.4.
Lemma 8.12
Let Γ⊢admit_{X,E} a:{X ∣ E} be a well formed term and
u:Δ→Γ a substitution [Tay99, Section 4.3].
Then Δ⊢admit_{X,E} u^{*}a:{X ∣ E} is also well formed, and
Δ ⊢ u^{*}(admit_{X,E} a) = admit_{X,E}(u^{*} a). 
Proof In the context [Δ, φ:Σ^{X}], since E and φ do not depend on Γ,
φ(u^{*} a) ≡ u^{*}(φ a) ⇔ u^{*}(Eφ a) ≡ Eφ(u^{*}a). 
This is consistent with the {}β and ηrules when we put u^{*}(i_{X,E}a) ⇔ i_{X,E}(u^{*}a), and with the Σ^{{}}rules since u^{*}(I_{X,E}θ) ⇔ I_{X,E}(u^{*}θ). ▫
Much of the business of Section A 8, which introduced the focus operation to handle sobriety, was to eliminate it. In particular, Proposition A 8.10 showed that focus is redundant for logical terms (i.e. of type Σ^{U}), whilst Section A 9–10 replaced it with descriptions for numerical terms (i.e. of type ℕ). The following result adds a new case to that reduction, for terms of type {Y ∣ E}, so focus can still be pushed to the outside of any term of the comprehension calculus, or eliminated altogether.
Lemma 8.13
If Γ⊢ P:Σ^{2} {Y ∣ E} is prime then
focus_{{Y ∣ E}} P = admit_{Y,E}(focus_{Y}(Σ^{2} i_{Y,E} P)). 
So {Y ∣ E} is sober, cf. Lemma 6.9.
Proof Since Γ⊢Σ^{2} i P:Σ^{2} Y is also prime (Lemma A 4.6), we may form
Γ ⊢ a ≡ focus_{Y}(Σ^{2} i P):Y, 
which satisfies

so we may then form Γ⊢admit_{Y,E}(focus_{Y}(Σ^{2} i P)). Applying θ:Σ^{{X ∣ E}},

whence the result follows by T_{0}. ▫
Finally, admit can also be moved to the outside of the term, although that is in fact the normalisation theorem to which the next two sections are devoted. Here we just consider the interaction with recursion, which is the symbolic analogue of Proposition 6.14.
[This proof requires equational hypotheses (Remark E 2.7).]
Lemma 8.14
Let X={Y ∣ E} with terms
Γ ⊢ n:ℕ, Γ ⊢ z:Y and Γ, m:ℕ, y:Y ⊢ s(m,y):Y 
such that Γ⊢admitz:X and Γ, m:ℕ, x:X⊢ admits(m,i x):X are well formed. Then
Γ ⊢ rec(n, admitz, λ m x.admits(m,i x)) = admitrec (n, z, λ m y.s(m, y)):X, 
omitting the subscripts on i_{Y,E} and admit_{Y,E}.
Proof Using the {}β and ηrules, the claim is equivalent to
Γ ⊢ i rec(n, admitz, λ m x.admits(m,i x)) = rec (n, z, λ m y.s(m, y)):Y 
and is valid for n=0. In order to use the rec ηrule to prove the claim, we have to check the same equation as for the induction step in an ordinary proof by induction, namely
