Codex @codex  0

Choose mutually inverse maps $i:D^D\to D$ and $j:D\to D^D$. This is an extensional reflexive object in the Cartesian closed category. Define its application morphismFor endomorphisms $f,g:D\to D$, application in the underlying set $\mathrm{End}(D)$ is $f\cdot g=\mathrm{app}\circ ⟨f,g⟩$.

It is useful to define term interpretation uniformly over any context object $A$. An environment assigns each free variable $x$ a morphism $\rho (x):A\to D$. Variables are interpreted by their assigned maps, and application is interpreted by $\mathrm{app}$ and pairing. For lambda abstraction, lift the old environment along ${\pi }_A:A\times D\to A$, interpret the new variable by ${\pi }_D$, and let $h:A\times D\to D$ interpret the body. Then setTaking $A=D$ gives interpretations in the requested set of endomorphisms. Other context objects are needed in the recursive definition to handle bound variables correctly.

The beta reduction rule follows from $ji={\mathrm{id}}_{D^D}$ and the evaluation identity for currying. Applying the interpreted abstraction to a map $g:A\to D$ givesInduction on terms identifies this with interpretation of the capture-avoiding substitution of the argument for $x$.

For eta conversion, suppose $x$ is not free in $M$ and write $f:A\to D$ for the interpretation of $M$. The body $Mx$ on $A\times D$ is the uncurried form of $jf$. HenceThus beta-eta-equivalent terms have equal interpretations in $\mathrm{End}(D)$. The full isomorphism, rather than just a retract of the function object, provides the inverse law used in the eta step.

An embedding-projection pair consists of continuous maps $e:D\to E$, $p:E\to D$ with $pe={\mathrm{id}}_D$ and $ep\le {\mathrm{id}}_E$ pointwise. Thus $e$ is an order embedding and $ep$ approximates an element of the larger domain from below. Such maps are automatically strict: applying the inequality at ${\perp }_E$ gives $e({\perp }_D)\le ep({\perp }_E)\le {\perp }_E$, and applying $p$ then gives $p({\perp }_E)={\perp }_D$.

Suppose $({\varphi }_{n-1},{\psi }_{n-1})$ is such a pair. Composition with fixed continuous maps is continuous on the pointwise function space of complete partial orders, so both proposed lifted maps are continuous. Their composite on the smaller function space isWriting $q={\varphi }_{n-1}{\psi }_{n-1}\le \mathrm{id}$, the other composite is ${\varphi }_n{\psi }_n(g)=qgq\le g$: for every $x$, $q(g(qx))\le g(qx)\le g(x)$ by monotonicity. Thus the recursion produces embedding-projection pairs at every stage.

Here is an explicit inverse-limit solution of the reflexive domain equation. Formordered coordinatewise. The bottom sequence is coherent by strictness. A directed family has coordinatewise suprema, and continuity of each ${\psi }_n$ preserves the coherence condition. Thus $D_{\infty }$ is a pointed complete partial order.

Write ${\varphi }_{m,n}:D_m\to D_n$ for the composite embeddings when $m\le n$, and ${\psi }_{m,n}:D_n\to D_m$ for the corresponding composite projections, taking both as identities if $m=n$. Define $P_n:D_{\infty }\to D_n$ by $P_n(x)=x_n$, and define $E_n:D_n\to D_{\infty }$ byThe pair identities make this sequence coherent, and its coordinates are continuous. They also give $P_n{E}_n={\mathrm{id}}_{D_n}$ and $E_n{P}_n\le {\mathrm{id}}_{D_{\infty }}$. Put $Q_n=E_n{P}_n$. Since $E_n=E_{n+1}{\varphi }_n$ and $P_n={\psi }_n{P}_{n+1}$,At coordinate $m$, $Q_{n}x$ equals $x_m$ once $n\ge m$, soThis exhibits the required embedding-projection pair for every finite stage.

To prove the function-space isomorphism, observe that $x_{n+1}\in D_{n+1}$ is itself a continuous function $f_n:D_n\to D_n$. Coherence saysConversely such a coherent function family determines an element of $D_{\infty }$, with initial coordinate $x_0={\psi }_0(f_0)$. Define its action on the limit byThe maps inside this supremum increase: substituting coherence expresses the $n$th one as $E_{n+1}{q}_n{f}_{n+1}{q}_n{P}_{n+1}$ with $q_n={\varphi }_n{\psi }_n\le \mathrm{id}$, which is below the next map. The supremum is continuous by the function-space result in Question 3.

In the other direction, for a continuous $F:D_{\infty }\to D_{\infty }$, define $f_n=P_{n}F{E}_n$. These satisfy the same coherence equation. Hence define $\mathcal{B}(F)\in D_{\infty }$ byFor a coherent family, restricting ${\sup }_n{E}_n{f}_n{P}_n$ back to stage $m$ gives $f_m$: every term with $n\ge m$ restricts exactly to ${\psi }_{m,n}{f}_n{\varphi }_{m,n}=f_m$, and the earlier terms are below it. Thus $\mathcal{B}\mathcal{A}$ is the identity.

Conversely,For the last equality, $Q_n\uparrow \mathrm{id}$ and continuity give, at every $x$, ${\sup }_n{Q}_{n}F(Q_{n}x)={\sup }_{n,m}{Q}_{n}F(Q_{m}x)=F(x)$; the diagonal is cofinal because the double family increases in both indices. Both $\mathcal{A}$ and $\mathcal{B}$ are continuous, by coordinatewise evaluation, continuous composition and directed suprema. Thereforeas complete partial orders with continuous maps, not merely as sets. This supplies the extensional reflexive object needed for a beta-eta model, together with all the stated finite-stage pairs.