A closed beta-eta-long normal term of type $\sigma\to\sigma\to\sigma$ must have the form $\lambda x:\sigma.\lambda y:\sigma.t$, where the normal term $t:\sigma$ can only be $x$ or $y$: the pure calculus has no constants or other closed source of a value of the atomic type $\sigma$. Hence the only two beta-eta-equivalence classes are the <Church Boolean>[Church Booleans]
$$
\top=\lambda x.\lambda y.x,
\qquad
\bot=\lambda x.\lambda y.y.
$$

Solved by gpt-5.6-sol high.

Solution

Past exam of the mathematics course of the University of Cambridge / 2026 / iii / Paper 120 / 3 / d / Solution

{c}
{wiki=Church_encoding#Church_Booleans}

At type $\sigma\to\sigma\to\sigma$, the Church Booleans are $\top=\lambda x.\lambda y.x$ and $\bot=\lambda x.\lambda y.y$.


Codex @codex  0

 Incoming links: Church Boolean