Y combinator as an application of Lawvere's fixed point theorem Lawvere's fixed point theorem states that that in a cartesian closed category, if there is a morphism $ϕ: A \to B^A$ which is point-surjective (i.e., for every point $q : 1 \to B^A$ there exists a point $p : 1 \to A$ such that $ϕp = q$), then every endomorphism $f : B \to B$ has a fixed point.
The fixed point of $f$ is obtained as $ϕ(p)(p)$ where $p : 1 \to A$ is the point of $A$ such that $ϕp = q$ for $q : 1 \to B^A$ defined in lambda calculus notation as $q = λa:A.fϕ(a)(a)$.
I've seen it remarked several times that the existence of Y combinator in lambda calculus, i.e., $Y = λf.(λx.f(xx))(λx.f(xx))$, is an application of Lawvere's fixed point theorem, but the remark has always been made only in passing and I haven't been able to figure out precisely how to get from the one to the other.
Can someone help me out by making the application explicit?
 A: What Scott did with domain theory was construct a cartesian closed category with $\varphi:D\cong D^D$. More generally, we have an retraction, i.e. split epimorphism, $D\to D^D$. Isomorphisms/split-epimorphisms are clearly point-surjective: simply set $p = \varphi^{-1}\circ q$.
We can actually arrange for $\varphi=id_D$ for some models of the untyped lambda calculus. Then the fixed point of $f$ by the above statement would be $(p\,p)$ where $p=q=\lambda x.f(x\,x)$, i.e. $$\mathsf{fix}\,f = (\lambda x.f(x\,x))(\lambda x.f(x\,x))$$ which we, of course, lambda abstract to get $$\mathsf{fix}=\lambda f.(\lambda x.f(x\,x))(\lambda x.f(x\,x))$$
Not assuming $\varphi=id_D$ adds some noise but just as easily leads to the appropriate expression. For example, in Haskell if you wanted to model the untyped lambda calculus, you could use:
newtype D = D {unD :: D -> D}

The data constructor D corresponds to $\varphi^{-1}$ with unD corresponding to $\varphi$ witnessing D ≅ (D -> D). It's an easy enough exercise to insert the uses of D and unD, more or less guided by the types, into the expression for the $Y$ combinator to get a type checking version in Haskell. In practice, you'd probably want some kind of "base type" so you can actually observe something from these values. This would produce a type like:
data D b = Base b | Fun (D b -> D b)

Here Fun plays the role of $\varphi^{-1}$ and unFun (Fun f) = f plays the role of $\varphi$ and we only have a retraction. (To make unFun total you can make unFun send Base b to any value of D -> D, though bottom is a value and not so dismissable anyway given the context of the problem.)
A: Lawvere's Fixed Point Theorem:
$X\times X\xrightarrow{f} Y\\
\Delta\uparrow\qquad\;\;\downarrow\alpha\\
\;\;\;X\;\; \xrightarrow[g]\;\; Y$
For sets $X, Y$, functions $f: X\times X\to Y$, $\alpha: Y\to Y$, let $g := \alpha\circ f\circ\Delta$. If $g$ is representable by $f(-,\ulcorner g\urcorner)$, then $\alpha$ has a fixed point: $\alpha\big(f\left(\ulcorner g\urcorner,\ulcorner g\urcorner\right)\big)=g\left(\ulcorner g\urcorner\right)=f\left(\ulcorner g\urcorner,\ulcorner g\urcorner\right)$.
Now let's fit Curry's $Y$ combinator into Lawvere's schema.
$\Lambda\times \Lambda \xrightarrow{f} \Lambda \\
\Delta\uparrow\qquad\;\;\downarrow\alpha_y\\
\;\;\;\Lambda\;\; \xrightarrow[g]\;\; \Lambda$
where $\Lambda$ is the class of lambda terms, and $f:(x,y)\mapsto yx$, and $\alpha_y: x\mapsto yx$.
then $g=\lambda x.y(xx)$ is a fixed point of $\alpha_y$:
$gg=\alpha_y(gg)$
Curry's $Y$ combinator is
$Y := \lambda y.gg=\lambda y.(\lambda x.y(xx))(\lambda x.y(xx))$
If we let $f:(x,y)\mapsto \lambda v.yxv$, and $\alpha_y: x\mapsto yx$, then
$g=\lambda x.y(\lambda v.xxv)$
and $gg=\alpha_y(gg)$.
Now we get the call-by-value version of $Y$ combinator:
$\lambda y.gg=\lambda y.(\lambda x.y(\lambda v.xxv))(\lambda x.y(\lambda v.xxv))$
If we let $f:(x,y)\mapsto yx$, and $\alpha: x\mapsto\lambda y.y(xy)$, then
$g=\lambda xy.y(xxy)$
$gg=\alpha(gg)$
Now we get Turing's $\Theta$ combinator:
$\Theta := gg=(\lambda xy.y(xxy))(\lambda xy.y(xxy))$
The call-by-value version of $\Theta$ combinator is similar.
Let $f:(x,y)\mapsto yx$, and $\alpha: x\mapsto\lambda y.y(\lambda z.xyz)$.
$g=\lambda xy.y(\lambda z.xxyz)$
$gg=\alpha(gg)$
$gg=(\lambda xy.y(\lambda z.xxyz))(\lambda xy.y(\lambda z.xxyz))$
