A = o→o→o —————————————————————————

[figure: o→o→o; λx^{o}λy^{o}; o; x; y]

A = α→((o→β)→α)→β→α —————————————————————————

[figure: α→((o→β)→α)→β→α; λa^{α}λf^{(o→β)→α}λb^{β}; α; f; a; o→β; λy^{o}; β; b]

A = ((α→β)→α)→α —————————————————————————

[figure: ((α→β)→α)→α; λF^{(α→β)→α}; α; F; α→β; λx^{α}; β]

This type, corresponding to Peirce’s law, does not have any inhabitants.

A = 1→o→o —————————————————————————

[figure: 1→o→o; λf^{1}λx^{o}; f  o; x]

We get the Church’s numerals λfλx.f^{n}x.

A = 1→1→o→o —————————————————————————

[figure: 1→1→o→o; λf^{1}λg^{1}λx^{o}; f  o  g; x]

Inhabitants of this type represent words over the alphabet Σ = {f, g}, for example

λf^{1}g^{1}x^{o}.fgffgfggx,

where we have to insert parentheses associating to the right.

A = (α→β→γ)→β→α→γ —————————————————————————

[figure: (α→β→γ)→β→α→γ; λf:α→β→γλb:βλa:α; γ; a; α; f; β; b]

A = 3 —————————————————————————

\xymatrix{3 \ar[d]_{λF^{2}} \\ o \ar[d] \ar[r]^{F} & 1 \ar[l]^{λx^{o}} \\ x}

This type 3 has inhabitants having more and more binders:

λF^{2}.F (λx_{0}^{o}.F (λx_{1}^{o}.F (⋯ (λx_{n}^{o}.x_{i})))).

The novel phenomenon that the binder λx^{o} may go round and round forces us to give new incarnations λx_{0}^{o}, λx_{1}^{o}, … each time we do this (we need a counter to ensure freshness of the bound variables).

[figure: 3→o→o; λΦ^{3}λc^{o}; f  o; Φ; 2; λf^{1}; c]

This type, called the monster M, does have a potential infinite amount of binding, having as terms e.g. λΦ^{3}c^{o}.Φλf_{1}^{1}.f_{1}Φλf_{2}^{1}.f_{2}f_{1}Φ … λf_{n}^{1}.f_{n} … f_{2}f_{1}c A = 1_{2}→o→o —————————————————————————

\xymatrix{1_{2}→o→o \ar[r]^{λp^{1_{2}}λc^{o}} & o \ar[d] \ar[r] & c \\  & p \ar[u] \ar[u]}

λp^{1_{2}}c^{o}.c and λp^{1_{2}}c^{o}.pc(pcc).

A = 1_{2}→2→o —————————————————————————

\xymatrix{ & 1 \ar[d]^{λx^{o}} \\ 1_{2}→2→o \ar[r]^{λF^{1_{2}}λG^{2}} & o \ar[u]^{G} \ar[d] \ar[r] & x \\  & F \ar[u] \ar[u]}

This is the type L corresponding to untyped lambda terms. For example the untyped terms ω ≡ λx.xx and Ω ≡ (λx.xx)(λx.xx) can be translated to (ω)^{t} ≡ λF^{1_{2}}G^{2}.G(λx^{o}.F xx) and

(Ω)^{t} ≡ λF^{1_{2}}G^{2}.F (G(λx^{o}.F xx))(G(λx^{o}.F xx))
=_{β} λF G.F ((ω)^{t}F G)((ω)^{t}F G)
=_{β} (ω)^{t} ·_{L} (ω)^{t},

where for M, N∈L one defines M ·_{L} N = λF G.F (MF G)(NF G).