# Can the Lawvere fixed point theorem be used to prove the Brouwer fixed point theorem?

The Lawvere fixed point theorem asserts that if $X, Y$ are objects in a category with finite products such that the exponential $Y^X$ exists, and if $f : X \to Y^X$ is a morphism which is surjective on points in the sense that the induced map $\text{Hom}(1, X) \to \text{Hom}(1, Y^X)$ is surjective, then $Y$ has the fixed point property: for every morphism $g : Y \to Y$ there exists a point $y : 1 \to Y$ such that $g \circ y = y$.

The Brouwer fixed point theorem asserts that the closed $n$-disks, all of which I will denote by $D$ for ease of notation, have the fixed point property as objects of $\text{Top}$.

Seeing these two theorems together, it is tempting to try to prove the latter from the former by finding a topological space $X$ such that the exponential $D^X$ exists, together with a surjective continuous map $X \to D^X$. Does there in fact exist such an $X$?

Edit, 4/13/17: I'm still interested in this question, and so are some people associated with MIRI (at least when $n = 1$); for some details about why see here.

• I guess I should mention, in passing, that Lawvere's is much more constructive than Brouwer's. So, if there is an implication that way, the space $X$ will have to contain a lot of non constructive data. (What is needed is essentially a choice of a point from every nonempty compact subspace of $\mathbb{R}$.) – François G. Dorais Jul 12 '13 at 20:54
• Hey! Next, let's prove the measure-theoretic Fubini theorem from the Category theory Fubini theorem! – Gerald Edgar Jul 12 '13 at 21:08
• Category theory seems to have the universal property of eliciting snarky remarks from those who don't have much taste for it. – Todd Trimble Jul 13 '13 at 11:20
• @user36938 : well, I see your point, but I think maybe you're being a little harsh ("does not belong on MO"). Even if we assume the question was a shade offhand (e.g., even if Qiaochu hadn't considered the constructivity aspects before posting), that's true of so many questions here; it's okay to kick it around for a few minutes before deciding that it's naive. It all comes under the heading of exploring. For a comparison: there are a lot of naive questions about logic here. But they usually don't elicit the same kinds of cracks, do they? No "logic corrupting the youth of today" trope. – Todd Trimble Jul 15 '13 at 6:22
• Well, I'm not sure. All I can say is that there are a lot more wise-cracks about category theory, and a lot of people think they understand it well enough to make pronouncements on (and jokes about) it. Happily, such jokes are becoming more and more pass\'e, as more and more people see that category theory is seriously useful stuff, and that professional category theorists are not in the business of "trying to get something from nothing". (Still, I can't think of any other field where people make such jokes. Can you?) – Todd Trimble Jul 15 '13 at 17:37

In my experience it is worth considering variants of Lawvere fixed point theorem. In the present case, I would split things up as follows, in order to circumvent the non-constructive nature of Brouwer's fixed point theorem.

Also, let me point out that we need not worry about exponentials too much, even though they do not exist in the category of topological spaces, unless the exponent is nice enough. We can move over to a cartesian-closed subcategory, such as teh compactly generated spaces, or to a cartesian closed supcategory, such as equilogical spaces.

Theorem: [Approximate Lawvere] Suppose $(B, d)$ is a metric space and $e : A \to B^A$ is a continuous map, such that for every continuous map $g : A \to B$ and $\epsilon > 0$ there is $a \in A$ such that $d(e(a)(a), g(a)) < \epsilon$. Then every continuous map $f : B \to B$ has approximate fixed points: for every $\epsilon > 0$ there is $b \in B$ such that $d(b, f(b)) < \epsilon$.

Proof. Given any $f$ and $\epsilon$ consider the map $g(a) = f(e(a)(a))$. there is $a \in A$ such that $d(e(a)(a), g(a)) < \epsilon$ and then $b = e(a)(a)$is an $\epsilon$-approximate fixed point of $f$. QED.

One way to use the theorem is via the sup metric (allowing infinite distance):

Corollary: If $e : A \to B^A$ has a dense image in the sup metric on $B^A$ then every endomap on $B$ has approximate fixed points.

Suppose we could apply the previous theorem to the closed ball $D^n$. Then we would know (constructively!) that every endomap on $D^n$ has approximate fixed points. then we just have another easy step, which contains all the classical reasoning needed:

Theorem: Suppose $X$ is compact and $f : X \to X$ has an $\epsilon$-approximate fixed point for every $\epsilon > 0$. Then $f$ has a fixed point.

Proof. By countable choice, for every $n$ there is $x_n \in X$ such that $d(x_n, f(x_n)) < 1/n$. Because $X$ is compact, $x_n$ has a subsequence converging to some $y \in X$. It is now easy to see that $y$ is a fixed point of $f$. QED.

But I do not see how to apply the approximate Lawvere to the closed ball, if that is even possible.

• We now have a bunch of results showing that the direct Lawvere fixed-point theorem is unlikely to succeed (see @ToddTrimble's answer). Can someone show that we can have $X \to [0,1]^X$ with a dense image? Or can we? – Andrej Bauer Apr 19 '17 at 21:36
• You can't have $e$ continuous w.r.t. the sup metric and have dense image, because that would give you a continuous surjection $\beta A \to B^{\beta A}$, where $\beta A$ is the Stone-Čech compactification, since $(B^A, \sup) \cong (B^{\beta A})$. You might be able to get $e$ continuous w.r.t. the exponential topology but have dense image w.r.t. the sup metric. Also, even though @ToddTrimble retracted his answer, you can't have a continuous surjection $A \to D^A$ with $A$ compact Hausdorff and $D$ a disk because $D^A$ would have the topology of the unit ball of a Banach space. – Sam Eisenstat Apr 22 '17 at 7:35

This is not an answer, but I will try to explain why I think that it is unlikely for such a space $X$ to exist.

If we replace $D$ by say, a sphere, then (using Lawvere's fixed point theorem and the fact that spheres do have fixed-point-free self-maps) such a space $X$ does not exist for the sphere. Now, I really don't see how to possibly use the fact that the disc is a disc in constructing the space $X$. So I am tempted to believe that your $X$ does not exist.

• Why can't we do an "Eilenberg swindle" where we take X to be a countable iterated exponential of disks? Something must go wrong because if that worked for disks, it would work for spheres too. Does such an iterated exponential not make sense? – Chris Schommer-Pries Jul 12 '13 at 20:56
• If such a swindle worked, it would work in the category of sets as well. It seems to me the basic problem is that there are no canonical maps between $X$ and $D^X$, so there's no obvious way to take a (co)limit of finite iterated exponentials to get an "infinite iterated exponential". – Eric Wofsey Jul 12 '13 at 21:19
• @Eric: this doesn't quite sink us. For example, as it turns out there is a canonical map $D \to D^D$ (constant functions) as well as a canonical map $D^{D^D} \to D^{D^{D^D}}$ (apply the functor $X \mapsto D^X$ to the previous map twice). These are the odd-numbered maps in a hypothetical diagram of shape $D \to D^D \to D^{D^D} \to ...$ that we would want. But it turns out that there are no canonical candidates for the even-numbered maps (in a precise sense; there are no such maps in the free cartesian closed category on $X$). We can "fix" this by considering a diagram of shape... – Qiaochu Yuan Jul 13 '13 at 4:37
• $D \to D^{D^D} \to D^{D^{D^{D^D}}} \to ...$, which does exist but which doesn't give us the kind of fixed point we would want (if the colimit exists and if the double dual functor $X \mapsto D^{D^X}$ preserves it then it's a fixed point of the double dual functor). – Qiaochu Yuan Jul 13 '13 at 4:38

Edit: Will Sawin has pointed out some difficulties with this answer. I'm going to leave this up for at least a while, in case anyone has any ideas about repairing it. Or perhaps this could be a cautionary tale?

My answer is that there is no space $X$ admitting a continuous surjection $X \to D^X$.

Following one of Andrej's suggestions, let's extend the context from $\text{Top}$ to the quasitopos $\text{Choq}$ of Choquet (aka pseudotopological) spaces. This is a convenient setting because quasitoposes are cartesian closed (so we never have to wonder about the existence of certain exponentials, as we would for $\text{Top}$), and moreover this won't alter the problem of the OP because the full inclusion $i: \text{Top} \to \text{Choq}$ preserves cartesian products and any exponentials that happen to exist in $\text{Top}$. A further convenience is that $\text{Choq}$ is concrete and even topological (over $\text{Set}$), and we may say that a map of Choquet spaces is surjective if its underlying function is, so that the inclusion $i$ also preserves surjective maps. (By concreteness, every surjective map is an epimorphism, and the converse is true in $\text{Choq}$.)

Suppose that there is a topological space $X$ such that $D^X$ exists in $\text{Top}$ and there is a surjective continuous map $\phi: X \to D^X$. In $\text{Choq}$ we get an induced map $D^\phi: D^{D^X} \to D^X$. The idea now is to construct a retraction to $D^\phi$ which might suggestively be denoted $\text{Ran}_\phi: D^X \to D^{D^X}$ (think "right Kan extension"), by exploiting the fact that $D = [0, 1]^n$ is an internal sup-lattice in $\text{Choq}$. Granting this possibility for the moment, and putting $Z = D^X$, we now have that $D^Z$ is a retract of $Z$ (to simplify notation, call the retraction $r: Z \to D^Z$ and the section $s: D^Z \to Z$), which opens the door to the argument given by Sam Eisenstat over at the related thread: Is there a topological space X homeomorphic to the space of continuous functions from X to [0, 1]?. In detail, for variables $z$ of type $Z$ and $g$ of type $D^D$, introduce the fixed-point combinator $Y: D^D \to D$ (which will live by the way in $\text{Top}$, since $D$ is an exponentiable space) by the formulas

$$H := \lambda g. s(\lambda z. g(r(z)(z)))$$

$$Y := \lambda g. (r(H(g)))(H(g))$$

and verify in the usual manner that $Y(g)$ of type $D$ is a fixed point of $g$. Then invoke Sam's argument that such continuous fixed-point combinators $Y$ can't exist. (Technically, he indicated the reason for the special case $D = I = [0, 1]$, but the problem for general $D$ can be reduced to the special case as follows. Supposing a fixed point combinator $Y: D^D \to D$ exists, choose a pair $\rho: D \to I, \sigma: I \to D$ that exhibits $I$ as a retract of $D$, and verify that the composition

$$I^I \stackrel{\sigma^\rho}{\to} D^D \stackrel{Y}{\to} D \stackrel{\rho}{\to} I$$

is a fixed point combinator, which is impossible by Sam's argument.) Contradiction.

The task now is to construct the retraction $\text{Ran}_\phi: D^X \to D^{D^X}$. As indicated before, the background of this construction is a theory of sup-lattices in quasitoposes, for which I know no literature reference, but at some point I can make some notes on this available on my nLab web. In fact I had begun a pretty deep dive into this theory here, but then luckily found some simplifications which circumvent a lot of this theory. I'll go into the simplified proof in the final section, after introducing some necessary definitions in the next section (for those not very categorically minded, the next section has the function of sparing us the terrible agony of verifying that certain "easily defined" functions between certain Choquet spaces really are continuous maps -- the abstract account which comes next does all that work for us).

A quasitopos $Q$ has a regular subobject classifier $\Omega$, which for $\text{Choq}$ is just a 2-point set $\{f, t\}$ equipped with the codiscrete (indiscrete) topology. (If $X$ is a Choquet space, then the points of $P X = \Omega^X$ are given by subspaces of $X$, i.e., subsets of $X$ with the subspace pseudotopology, or just the subspace topology if $X$ is a topological space.) Next, each map in $Q$ has a (unique) epi-(regular mono) factorization, due to the very useful fact that a quasitopos is not just regular but coregular ($Q^{op}$ is regular); see Johnstone's Elephant, Corollary A.2.6.3. The mono part will be called the regular image of $f$. This permits us to define, for a map $f: X \to Y$, the direct image mapping $\exists_f: \Omega^X \to \Omega^Y$ that in the case $Q = \text{Choq}$ takes a subspace $U$ of $X$ to the subspace $f(U)$ of $Y$. Formally, $\exists_f$ is defined by starting with the canonical regular subobject $\in_X \hookrightarrow X \times \Omega^X$ that is classified by the evaluation mapping $X \times \Omega^X \to \Omega$, then taking the regular image of the composite

$$\in_X \hookrightarrow X \times \Omega^X \stackrel{f \times 1}{\to} Y \times \Omega^X,$$

then forming the classifying map $Y \times \Omega^X \to \Omega$ of the regular image, and then currying that to get $\exists_f: \Omega^X \to \Omega^Y$.

Next, let us define a poset in $Q$ to be an object $X$ together with a regular subobject $i: X_1 \hookrightarrow X \times X$ satisfying standard axioms. If $X, Y$ are two posets, we can define their internal hom $[X, Y]$ as the pullback of an evident diagram

$$\begin{array}{ccccc} & & & & Y_1^{X_1} \\ & & & & \downarrow j^{X_1} \\ Y^X & \stackrel{sq}{\to} & (Y \times Y)^{X \times X} & \stackrel{(Y \times Y)^i}{\to} & (Y \times Y)^{X_1} \end{array}$$

where $sq(f) := f \times f$. The pullback of the regular mono $j^{X_1}$ along the bottom composite is again a regular mono $[X, Y] \to Y^X$. Of course $\Omega$ has a standard ordering $f \leq t$ and the points of $[X, \Omega]$ are given by regular upward-closed subobjects of $X$; for the quasitopos $\text{Choq}$ I'll just call them "up-sets", and similarly the points of $[X^{op}, \Omega]$ are "down-sets".

We will want to consider $[X^{op}, \Omega]$ as a free posetal cocompletion of $X$, so let's say a few words on that. The "Yoneda embedding" $y_X: X \to [X^{op}, \Omega]$ is obtained by letting $\chi_{X_1}: X \times X \to \Omega$ classify the regular subobject $X_1 \hookrightarrow X \times X$, and then appropriately currying to a map $X \to \Omega^X$, and noting this factors through a map $X \to [X^{op}, \Omega]$ by the poset axioms. We form a cocompletion functor $\mathbf{P}$ which takes a poset $X$ to $[X^{op}, \Omega]$. For a poset map $f: X \to Y$, the map $\mathbf{P}f: [X^{op}, \Omega] \to [Y^{op}, \Omega]$ is to take a down-set $U$ of $X$ to the down-set generated by the direct image $\exists_f(U)$ in $Y$. Formally: if the poset $Y$ is given by a span $Y \stackrel{\pi_1}{\leftarrow} Y_1 \stackrel{\pi_2}{\to} Y$, then the composite

$$\Omega^Y \stackrel{\pi_2^\ast}{\to} \Omega^{Y_1} \stackrel{\exists_{\pi_1}}{\to} \Omega^Y$$

has as its regular image the inclusion $[Y^{op}, \Omega] \hookrightarrow \Omega^Y$ we constructed earlier. This map maps a regular subobject to the down-set it generates. Denoting its epi-(regular mono) factorization as

$$\Omega^Y \stackrel{e}{\to} [Y^{op}, \Omega] \hookrightarrow \Omega^Y$$

we now define $\mathbf{P}f: \mathbf{P}X \to \mathbf{Y}$ to be the composite

$$[X^{op}, \Omega] \hookrightarrow \Omega^X \stackrel{\exists_f}{\to} \Omega^Y \stackrel{e}{\to} [Y^{op}, \Omega].$$

The functor $\mathbf{P}$ thus defined on the category of internal posets carries a monad structure whose unit is the Yoneda embedding $y$ (i.e., the component at $X$ is the principal down-set map $y_X: X \to [X^{op}, \Omega]$ we constructed earlier), and the multiplication turns out to be given by

$$\text{mult}_X := [y_X^{op}, \Omega]: [[X^{op}, \Omega]^{op}, \Omega] \to [X^{op}, \Omega].$$

Officially, a sup-lattice is a $\mathbf{P}$-algebra. It can also be described as a poset $X$ whose Yoneda embedding $y_X: X \to \mathbf{P}X$ has a left adjoint (which will then be the algebra structure $\mathbf{P}X \to X$: there can be only one, as $\mathbf{P}$ is a lax idempotent or KZ monad).

What seems to simplify matters greatly is to introduce another concept which, I'm pretty darned sure, is equivalent to the concept of sup-lattice. (See the post Retractions of Yoneda are reflectors, i.e., left adjoints? for some explanation why.)

Definition: An s-lattice is a poset $X$ whose Yoneda embedding admits a retraction. We let $\sup_X$ generically denote a chosen retraction (although as I suggest, I think there can be at most one!).

Here is the seed example. In $\text{Choq}$, the poset $I = [0, 1]$ is an s-lattice. The poset of down-sets $[I^{op}, \Omega]$ may be identified with $I \times \{f \leq t\}$ under the lexicographic order, topologized by the order topology. (One should check that the compact-open topology is in fact this order topology.) The Yoneda embedding takes $x \in I$ to $(x, t)$. The retraction is just the projection map $I \times \{f, t\} \to I$.

Lemma 1: If $L$ is an s-lattice, then so is $L^X$ for any object $X$.

Proof: Regard $X$ as an internal discrete poset (both maps of the span being $1_X$). There is an evident identification $\mathbf{P}(L \times X) = (\mathbf{P}L)^X$. Now examine the diagram

$$\begin{array}{cccccc} L^X & \stackrel{y^X}{\to} & \mathbf{P}(L \times X) & & & & \\ y \downarrow & & y \downarrow & \searrow^{id} & & & \\ \mathbf{P}(L^X) & \underset{\mathbf{P}(y^X)}{\to} & \mathbf{PP}(L \times X) & \underset{\text{mult}}{\to} & \mathbf{P}(L \times X) & \underset{\sup_L^X}{\to} & L^X \end{array}$$

(the square commutes by naturality of $y$, and the triangle commutes by a unit equation for the monad $\mathbf{P}$), and use the fact $\sup_L^X \circ y_L^X = 1_{L^X}$. Thus the bottom composite retracts $y_{L^X}$. $\Box$

For example, $D = I^n$ is an s-lattice in $\text{Choq}$. It follows further that any $D^X$ is an s-lattice.

Recall that if $A, B$ are posets and $f: A \to B$ is a poset map, then $f$ is an embedding if $a \leq a'$ in $A$ whenever $f(a) \leq f(a')$ in $B$. It is easy to see that embeddings are monomorphisms.

Lemma 2: If $f: X \to Y$ is a surjection in $\text{Choq}$ and $D$ is a poset, then $D^f: D^Y \to D^X$ is an embedding.

This is pretty obvious. $D^f(g) := g \circ f$, so $D^f(g) \leq D^f(g')$ means $g f \leq g' f$. This implies $g \leq g'$ by surjectivity of $f$.

Lemma 3: If $h: A \to B$ is a poset embedding in $\text{Choq}$, then $[h^{op}, \Omega]$ retracts $\mathbf{P}h$.

Proof: It suffices to check this at the level of underlying sets, by concreteness of $\text{Choq}$ over $\text{Set}$. Let $U \in \mathbf{P}A$ be a down-set of $A$. Then $\mathbf{P}h(U) = \{b \in B: \exists_{a \in A} a \in U \wedge b \leq h(a)\}$. The function $[h^{op}, \Omega]$ sends this down-set to $\{a' \in A: \exists_{a \in A} a \in U \wedge h(a') \leq h(a)\}$. Since $h$ is an embedding, this is the same as $\{a' \in A: \exists_{a \in A} a \in U \wedge a' \leq a\}$, but this is just $U$ since $U$ is downward-closed. $\Box$

Our task is completed with the following result.

Theorem: If $f: X \to Y$ is a continuous surjection in $\text{Choq}$ and $D$ is an s-lattice, then $\text{Ran}_f := \sup_{D^Y} \circ [(D^f)^{op},\Omega] \circ y_{D^X}$ retracts $D^f$.

Proof: We have

$$\begin{array}{ccc} 1_{D^Y} & = & \sup_{D^Y} \circ y_{D^Y} \\ & = & \sup_{D^Y} \circ [(D^f)^{op}, \Omega] \circ \mathbf{P}(D^f) \circ y_{D^Y} \\ & = & \sup_{D^Y} \circ [(D^f)^{op}, \Omega] \circ y_{D^X} \circ D^f \end{array}$$

where the first equation uses Lemma 1, the second uses Lemmas 2 and 3, and the third uses naturality of $y$. $\Box$

• How can the compact-open topology on $[I^{op}, \Omega]$ be the order topology when $\Omega$ has the indiscrete topology? – Will Sawin Apr 19 '17 at 21:35
• It seems to me like a retract of $D^f$ does not exist for an arbitrary continuous map $f$. To admit a retract, a map to a Hausdorff space must have closed image, as the image is exactly the locus where the composition of the retract with the original map is equal to the identity. If we take $X$ as the interval with the discrete topology, $Y$ with the interval with the usual topology, and $f$ the obvious map, then $I^X$ is the space of $I$-valued functions on $I$ with the topology of pointwise convergence, which is clearly Hausdorff, but within which the continuous functions are not closed. – Will Sawin Apr 19 '17 at 21:39
• @WillSawin Thanks for your comments. Yeah, something seems fishy, but I'm not quite sure where the real root of the problem is. Thinking... – Todd Trimble Apr 19 '17 at 22:31
• If it helps, I think the map $sup_L^X$ from ${\mathbf P}(L \times X)$ to $L^X$ is not well-defined, because it does not always produce continuous maps. From an arbitrary downward-closed subset of $L \times X$, by taking the supremum, we can produce an arbitrary function from $X$ to $L$ and not just a continuous function. – Will Sawin Apr 19 '17 at 22:38
• Sorry for the delay in responding. Actually, the root of the problem is that I badly misidentified the topology on $\mathbf{P}D$ (it's codiscrete, which seems painfully obvious in retrospect), and in fact $D$ is not an internal sup-lattice as defined here. Except for that, I believe the rest was correctly argued. I'm still investigating possible repairs... – Todd Trimble Apr 23 '17 at 17:43

Here is a sort of partial solution. I doubt it will be very helpful, but anyone who wants to read it is free to do so.

Let $I$ be any space with the fixed point property. We will construct a space $X$ and a map $X \to I^X$ such that many interesting maps lie in its image, including all maps that can be defined in a language consisting of $e$, continuous functions from finite powers of $I$ to itself, and constant symbols in $X$ (which are all that is needed to prove the Lawvere fixed point theorem).

To accomplish this we will inductively construct for each natural number $n$ a space $X_n$, a map $e_n: X_n \times X_n \to I$, and a map $i_n: X_n \to X_{n+1}$, such that $e_{n+1}(i_n(x_1),i_n(x_2))=e_n(x_1,x_2)$. We will also use auxiliary spaces $Y_n,Z_n$ along the way.

After this we set $X$ to be the forward limit of $X_n$ along $i_n$ and let $e: X\times X \to I$ be the limit of the $e_n$.

The significance of the spaces $Y_n$ and $Z_n$ is that $Z_n$ is the set of continuous $I$-valued functions of $x \in X$ that depend only on $e(x,x), e(x,t)$ for $t \in X_n$. $Y_n$ is the space of possible values of the pair $e(x,x), e(x,t)$, so that $Z_n$ is the space of functions on $Y_n$. Then $X_{n+1}$ is constructed so that it maps surjectively to $Z_n$, so all functions of $Z_n$ come from elements of $X_n$, and maps to $Y_n$, so that all functions of $Z_n$ can be extended to functions on $X_n$. For simplicity and canonicality, we define $X_{n+1}$ to be a subset of $Y_n \times Z_n$, defined by coherence condition to ensure the desired relationship between $Y_n$ and $e$. Then we can freely add also the functions $e(t,x)$ for $t\in X_n$ to $Z_n$, as they are already continuous functions of $e(x,x)$, $e(x,t)$ by construction of $X_n$.

To begin, let $X_0$ be the empty set.

Inductively, assume we have defined $X_{n-1}, Y_{n-1},Z_{n-1}, X_n$.

Let $Y_n$ be $I \times I^{X_n}$. Let $Z_n= I^{Y_n}$.

Let $X_{n+1}$ be the subset of $Y_n \times Z_n$ consisting of tuples $(b,c)\in Y_n, f\in Z_n$ satisfying the following two coherence conditions:

• $b= f(b,c)$

• For all $x$ in $X_n$, $c(x) = f( e_n(x,x), t \mapsto e_n(x,t))$

Let $i_n: X_n \to X_{n+1}$ send $x= ((b',c'),f)$ to $(e_n(x,x), t \mapsto e_n(x,t) ) , (\beta,\gamma)\mapsto f'(\beta, \gamma \circ i_{n-1} )$.

Let $e_{n+1}: X_{n+1} \times X_{n+1} \to I$ send $((b_1,c_1),f_1),((b_2,c_2),f_2)$ to $f_1(b_2,c_2)$.

Let us first check that for $x$ in $X_n$ corresponding to a tuple $(b,c),f$ in $Y_{n-1} \times Z_{n-1}$, $i_n(x)$ satisfies the coherence conditions.

For $x$ in $X_n$ which corresponds to a tuple $(b,c),f$, we need $e_n(x,x) = f( e_n(x,x), t \mapsto e_n(x, i_{n-1}(t))$, but $e_n(x)=f(b,c)$ so it is sufficient to check that $b=e_n(x,x)$ and $c= t \mapsto e_n(x, i_{n-1}(t))$, which are the coherence conditions of $X_n$.

Furthermore we need for $x'$ in $X_n$ corresponding to a tuple $(b',c'),f)$, $e_n(x,x') = f( e_n(x',x'),t \mapsto e_n(x',i_{n-1}(t)))$, which is true because by definition of $e_n$, $e_n(x,x') = f(b',c')$ and $b' = f'(b',c') =e_n(x',x')$ while $c'(t) = f'( e_{n-1}(t,t), s \mapsto e_{n-1}(s,t)) = e_n(x', i_{n-1}(t))$ by definition of $e_n$ and $i_{n-1}$.

Hence $i_n$ is actually a well-defined map from $X_n$ to $X_{n+1}$.

The fact that $e_{n+1}(i_n(x_1),i_n(x_2))=e_n(x_1,x_2)$ follows from unwinding the definitions.

Indeed, let $x_1 = ((b_1,c_1),f_1)$ and let $f_2=((b_2,c_2),f_2))$ and then $e_{n+1} (i_n ( x_1),i_n(x_2)) = f_1 ( e_n (x_2,x_2), t \mapsto e_n(x_2, i_{n-1}(t)) =f_1(b_2,c_2)= e_n(x_1,x_2)$ by the coherence conditions for $b_2,c_2$ and the definition of $e_n$, and then the definition of $e_n$.

Now we can define $X$ to be the forward limit of $X_n$ along $I_n$ and $e$ to be the forward limit of the maps $e_n$, which we have seen are compatible. Next we will characterize the image of the map $X \to I^X$ given by $x \mapsto (t \mapsto e(x,t))$. We will see that it this image can be viewed as the forward limit of $Z_n$ along the system of maps that we now define.

Consider the map $j_n: Y_{n+1} \to Y_{n}$ that sends $(b,c)$ to $( b, c \circ i_n)$. Consider also the map $k_n: Z_{n} \to Z_{n+1}$ by exponentiating $j_n$.

I claim that if $i_{n} ((b,c),f)= ((b',c'),f')$ then $j_n(b',c') = (b,c)$ and $k_n(f)=f'$.

The first statement is simply the fact that $b=e_n(x,x), c(t)= t \mapsto e_n(x,i_{n-1}(t))$, which follow from the definition of $e_n$ and the coherence conditions for $b$ and $c$ respectively.

The second statement follows immediately from the construction of $i_n$, which forces $f' ( \beta,\gamma) = f( \beta , \gamma \circ i_n) = \alpha(x)$ which is exactly $f \circ k_n$.

So we have verified the claim.

Let $Y$ be the inverse limit of $Y_n$ along $j_n$ and let $Z$ be the inverse limit of $Z_n$ along $k_n$, so that there is a natural map $Y \times Z \to I$. The compatibilities of $i_n$ with $j_n$ and $k_n$ respectively imply that there are map $X \to Y$ and $X \to Z$, and $e: X \times X \to I$ is simply the composition of these two with the map $Y \times Z \to I$.

Hence the map $X \to I^X$ induced by $e$ factors as $X \to Z \to I^Y \to I^X$. I can't prove that this composition is surjective but I can prove that the first map, $X \to Z$ is surjective.

To do this, it is sufficient to prove that the projection map $X_n \to Z_n$ is surjective. In other words, given $f: Y_n \to I$, construct $(b,c) \in Y_n$ satisfying the coherence conditions. Clearly we must have $c(x) = f( e_n(x,x), t \mapsto e_n(x,t))$. Then we can take $b$ to be any fixed point of $f(b,c)$.

What maps can we construct this way? We get all the maps defined by elements of $Z_n$ for all $n$. These, in turn, are all continuous maps that depend only on the data in $Y_n$. By the coherence conditions and the definition of $e$, the projection of $x \in X_n$ to $Y_n$ encode $e(x,x),t\mapsto e(x,t)$ for $t$ in $X_{n-1}$. Using the definition of $e$ and the compatibility of $e$ with $i_{n-1}$, one can see that it also encodes $t \mapsto e(t,x)$ for $t \in Y_{n-1}$. The compatibility of $i_n$ with $e$ and with $j_n$ ensure that $Y_n$ continues to encode this data for all $x$. Hence all continuous functions that depend only on $t\mapsto e(t,x),e(x,x),t\mapsto e(x,t)$, which seem to me to be all the "obvious" ones that we construct, are in the image of the constructed map $X \to I^X$.

The definability statement from earlier follows from the fact that any finite set of elements of $X$, such as the constant symbols appearing in the formula, must lie in $X_n$ for some $n$. Any function that depends only on $e$ evaluated with these constant symbols will then lie in $Z_n$.

• For clarity $X_0 = \emptyset$, $Y_0 = I$, $Z_0 = I^I$, $X_1$ is the space of pairs of a continuous map $I \to I$ and a fixed point of that map. $Y_1$ is the space of pairs of $b$ an element of $I$ and $c$ a pair of a map $I\to I$ and a fixed point, with $a$ forced to be the evaluation map that takes a map $I \to I$ (with a fixed point) to the evaluation of that map at $b$. – Will Sawin Apr 14 '17 at 5:50