This section shows how each new type (generated arbitrarily from comprehension and powers of products) may be expressed as a subtype (by a single comprehension) of a type in the original calculus. This is like expressing any set in Zermelo set theory as a subset of an iterated powerset, as in the von Neumann hierarchy. It will relate back to the categorical construction in Section 4, where every new object of S is a formal equaliser in S.
The structure maps in this isomorphism are, of course, terms to be defined, but they behave like the constructors i, I and admit of the comprehension calculus. That is, the lemmas that we have to prove towards this isomorphism are like the β and ηrules of the calculus, and will therefore be presented and named as such. This is not a serious overloading of the i and I notations, as the old use has two subscripts.
Remark 9.1
Given any λcalculus (such as ours) with all of the
usual structural rules, the corresponding category has products simply
because they are concatenations of contexts.
The problem with products
that was a central concern in the two categorical constructions
does not, unfortunately, go away so easily:
we have merely pushed it into the exponents.
A power type is Σ^{(−)} applied to (the product of) a list of types, and λabstraction and application involve the list operations of push and pop (or cons and (head,tail)) on types. The normalisation process for types must therefore also deal with lists. This could be formalised by introducing metavariables to denote either lists of types, or powers of lists. However, as this complication does not have any impact on the real issues in the argument, we leave the interested reader to carry this through for themselves, and simply consider the case of lists of length two. We take Σ^{Y× Z} to mean (Σ^{Z})^{Y}, a typical term of which is λ y.φ, where y:Y and φ:Σ^{Z}. In this sense, Σ contains the empty list.
The main technical question with products then manifests itself in this situation as the choice between I_{Z}^{ Y }· I_{Y}^{Z} and the other term that could serve as i_{ΣY× Z}.
Extended notation
Notation 9.2
By structural recursion on the type X, we define a type X , terms
and the idempotent E_{X} on Σ^{ X }. The base cases are 1, Σ and ℕ, for which these maps are identities. So X erases the comprehensions from X, and i_{X} embeds X as a subspace of X . This has the subspace topology because of I_{X}.
Lemma 10.10 shows that E_{{Y ∣ E}}= E , where the translation E for terms is defined in the next section.
The normalised type
Lemma 9.3
The Σ^{{}}η rule,
Σ^{iX}· I_{X}=id_{ΣX} or
φ:Σ^{X}, x:X⊢(I_{X}φ)(i_{X} x)=φ x,
is valid.
Proof By structural induction on the type X. If X≡Σ^{Y× Z} then

If X≡{Y ∣ E} then

Lemma 9.4
The Σ^{{}}β rule, I_{X}· Σ^{iX}=E_{X}, is valid.
Proof By structural induction on the type X. If X≡Σ^{Y× Z} then

If X≡{Y ∣ E} then

Proposition 9.5
{ X ∣ E_{X}} is a well formed type,
with structure i_{X} and I_{X}.
Proof E_{X} on X is a nucleus (Definition 8.7), by the same argument as we used in Corollary 4.13. ▫
The other rules for the extended notation
Lemma 9.6
The {}E_{0} rule is well formed and
the {}E_{1} rule is valid.
Proof There is no issue of wellformedness, as i_{X} at any type is built using i_{Y,E} and I_{Y,E} but not admit_{Y,E} from the comprehension calculus. Now let x:X and φ:Σ^{ X }. From Lemmas 9.3 and 9.4 we have
Σ^{iX}· E_{X} = Σ^{iX}· I_{X}·Σ^{iX} = Σ^{iX}, 
so φ(i_{X} x) = Σ^{iX}φ x = (Σ^{iX}· E_{X})φ x = E_{X}φ(i_{X} x) . ▫
Lemma 9.7 The {}I rule is well formed,
and the {}β rule is valid, at type X≡Σ^{Y× Z}.
Proof In the introduction rule, admit_{X}φ = Σ^{iY× iZ}φ with no issue of wellformedness, as this expression does not use admit from the comprehension calculus. Also,

So φ=i_{X}admit_{X}φ by T_{0}. ▫
Lemma 9.8
If X≡{Y ∣ E} then E_{X}⊂_{ Y }E_{Y}
in the sense of Notation 4.4.
Proof E_{X}=E_{{Y ∣ E}}=I_{Y} · E · Σ^{iY}, whilst E_{Y}=I_{Y}· Σ^{iY} by Lemma 9.4. Then
E_{Y}· E_{X} = I_{Y} · Σ^{iY} · I_{Y} · E · Σ^{iY} = I_{Y} · E · Σ^{iY} = E_{X} = I_{Y} · E · Σ^{iY} · I_{Y} · Σ^{iY} = E_{X} · E_{Y} 
by Lemma 9.3 (Σ^{{}}η for Y). ▫
Lemma 9.9
The {}I rule is well formed,
and the {}β rule is valid, at all types.
Proof By structural induction on the type X, with Y≡ℕ or Σ^{Z} as the base case (even when Z is itself a product or comprehension type), so consider X≡{Y ∣ E}.
First, φ a ⇔ E_{X}φ a ⇔ (E_{Y}· E_{X}) φ a ⇔ E_{Y} φ a using the given sidecondition twice, and since E_{X}⊂E_{Y}. Hence b≡ admit_{Y} a:Y is well formed, and i_{Y} b=a by the induction hypothesis, {}β for Y.
For the whole expression to be well formed, we need ψ:Σ^{Y}⊢ψ b⇔ Eψ b. Put φ≡ I_{Y}ψ:Σ^{ Y }. Then

Finally, i_{X}(admit_{X} a) = i_{Y,E}(i_{Y}(admit_{Y}(admit_{Y,E} a))) = i_{Y,E}(admit_{Y,E} a) by the induction hypothesis, but this is a by {}β for {Y ∣ E}. ▫
Lemma 9.10
The {}η rule, admit_{X}· i_{X}=id_{X}, is valid.
Proof The expression is well formed by Lemmas 9.6 and 9.9. We prove the equation by structural induction on the type X. If X≡Σ^{Y× Z} then, as in Lemma 9.3,

If X≡{Y ∣ E} then admit_{X}· i_{X} = admit_{Y,E} · admit_{Y} · i_{Y} · i_{Y,E}, which is admit_{Y,E}· i_{Y,E} by the induction hypothesis, but this is id_{{Y ∣ E}} by {}η for {Y ∣ E}. ▫
The isomorphism
Proof For the two admitexpressions to be well formed, we need properties of the form E_{X}φ(i x) ⇔ φ(i x), where i x is either i_{X} x or i_{ X ,EX} x , cf. Lemma 8.10.
admit_{ X , EX}(i_{X} x) is well formed by Lemma 9.6 ({}E_{1} for X) and {}I for { X ∣ E_{X}}.
admit_{X}(i_{ X , EX} x ) is well formed by {}E_{1} for { X ∣ E_{X}} and Lemma 9.9 ({}I for X).
admit_{X}(i_{ X , EX}(admit_{ X , EX}(i_{X} x))) = admit_{X}(i_{X} x) by {}β for { X ∣ E_{X}}, but this is x by Lemma 9.10 ({}η for X).
admit_{ X , EX}(i_{X}(admit_{X}(i_{ X , EX} x ))) = admit_{ X , EX}(i_{ X , EX} x ) by Lemma 9.9 ({}β for X), but this is x by {}η for { X ∣ E_{X}}. ▫
Proposition 9.12 This induces
Proof φ(admit_{X}(i_{ X , EX} x )) ⇔ I_{X}φ(i_{X}(admit_{X}(i_{ X , EX} x ))) ⇔ I_{X}φ(i_{ X , EX} x ) because of Lemmas 9.3 and 9.9 (Σ^{{}}η and {}β for X).
θ(admit_{ X , EX}(i_{X} x)) ⇔ I_{ X , EX}θ(i_{ X , EX}(admit_{ X , EX}(i_{X} x))) ⇔ I_{ X , EX}θ(i_{X} x) by Σ^{{}}η and {}β for { X ∣ E_{X}}. ▫