X compact iff projection is closed I've seen this exercise around to motivate the definition for complete variety, but I seem to have trouble proving it (and can't find any hints). 
The statement I want to show is: $X$ is compact if and only if the projection $X \times Y \to Y$ is closed for any space $Y$.
I'm stuck on both directions, though assuming $X$ is compact and $Y$ is Hausdorff the projection is clearly closed, but the statement says it must hold for all $Y$ so I'm a bit thrown off. In fact, I might be missing a simple example, but I'm having trouble thinking of a closed subset $A \times B \subseteq X \times Y$ such that $B$ is not closed in $Y$ (which must exist for any $X$ noncompact...). Is there a straightforward example for this?
Thanks.
 A: Corrected
One direction is just the tube lemma.
For the other direction, suppose that $X$ is not compact; we want to find a space $Y$ such that the projection $\pi:X\times Y\to Y$ is not closed. Let $\mathscr{U}$ be an open cover of $X$ that has no finite subcover.


*

*Show that we may without loss of generality assume that $\mathscr{U}$ is closed under finite unions, i.e., that if $\mathscr{U}_0$ is a finite subset of $\mathscr{U}$, then $\bigcup\mathscr{U}_0\in\mathscr{U}$.


Let $\mathscr{F}=\{X\setminus U:U\in\mathscr{U}\}$.


*

*Verify that $\mathscr{F}$ is a family of non-empty closed sets, that $\mathscr{F}$ is closed under finite intersections, and that $\bigcap\mathscr{F}=\varnothing$.


Let $p$ be a point not in $X$, and let $Y=\{p\}\cup X$. Let
$$\tau=\wp(X)\cup\big\{\{p\}\cup F\cup A:F\in\mathscr{F}\text{ and }A\subseteq X\big\}\;.$$


*

*Show that $\tau$ is a topology on $Y$, and that $X$ is an open subspace of $Y$ with this topology.


(As an aid to intuition, note that the open nbhds of $p$ in $Y$ are precisely the subsets of $Y$ that contain $p$ and some element of $\mathscr{F}$.)
Let $D=\{\langle x,x\rangle\in X\times Y:x\in X\}$, and let $C=\operatorname{cl}_{X\times Y}D$; clearly $C$ is closed in $X\times Y$. Suppose, to get a contradiction, that the projection $\pi:X\times Y\to Y$ is closed.


*

*Show that $p\in\pi[C]$, so that there must be some $x\in X$ such that $\langle x,p\rangle\in C$.  

*Get a contradiction by finding an open nbhd $U$ of $\langle x,p\rangle$ in $X\times Y$ that is disjoint from $D$. (HINT: Use the fact that $\mathscr{U}$ covers $X$.)

A: For variety, here's a proof in a dramatically different style.  This is using synthetic topology.  "Synthetic" approaches in general are about working in an internal language, in this case a simply typed lambda calculus, where the structural properties we care about hold by construction, in this case continuity, and often the internal language is a conservative extension giving further nice properties, in this case that function spaces "do the right thing".  Being conservative extensions, any "classical" theorem we prove is true classically even if we use techniques that aren't valid classically.  Building all this and proving the correspondence theorems is a lot of work.  Using the end results, though, is quite easy.  Enough introduction, onward!
A core space in topology is the Sierpiński space which is the set $\Omega=\{\bot,\top\}$ with the open sets $\{\{\},\{\top\},\{\bot,\top\}\}$.  It's importance is that there is a bijection between continuous functions $X \to \Omega$ and the open sets of $X$.  So, in our synthetic context, we take it as axiomatic that $U\subseteq X$ is an open set if and only if there exists a (continuous) function $\chi_U : X \to \Omega$ where $\chi_U(x) = \top \iff x\in U$.  (In our context, all functions we can write down, that is, which are $\lambda$-definable, are continuous.  We can't define $\chi_U$ in general but we can manipulate it once we assume its existence.)  A closed set is the usual thing, i.e. a set whose complement is open.  Explicitly, $F \subseteq X$ is closed iff $\chi_{F^c} : X \to \Omega$ exists, i.e. $\chi_{F^c}(x) = \top \iff x\notin F$. A function is closed if it takes closed sets to closed sets.  In our parlance, a function $f : X \to Y $ is closed if for every $\chi_{F^c} : X \to \Omega$ there's a $\chi_{f[F]^c} : Y \to \Omega$ where $f[F]$ is the direct image.
A subset $Q \subseteq X$ is compact iff there exists a function $\forall_Q : \Omega^X \to \Omega$ where $\forall_Q(p) = \top \iff \forall x\in Q. p(x) = \top$.  $\Omega^X$ is the space of functions $X \to \Omega$, i.e. it is for us the space of open sets on $X$.  I'll talk about how this matches the classical definition later.
Now our theorem.  $X$ is compact iff $\pi_2 : X\times Y \to Y$ is closed for any space $Y$.  Note, the proof below requires that $\Omega^X$ behaves in a way that it may not classically, which means, taken naively this proof only holds for such $X$.  As I mentioned in the introduction, we can systematically show that such side-conditions are unnecessary.
Proof: For the $\Rightarrow$ direction, we have $\forall_X : \Omega^X \to \Omega$ and we need to show that if we are given a $\chi_{F^c} : X\times Y \to \Omega$ we can build a $\chi_{\pi_2[F]^c} : Y \to \Omega$.  We have
$$\begin{align}
\chi_{\pi_2[F]^c}(y) = \top & \iff y \notin \pi_2[F] \\
                            & \iff \forall x\in X. (x,y)\notin F \\
                            & \iff \forall_X(\lambda x. \chi_{F^c}(x,y)) = \top
\end{align}$$
And that's the proof for that direction.  $\chi_{\pi_2[F]^c} \equiv \lambda y.\forall_X(\lambda x.\chi_{F^c}(x,y))$.
For the $\Leftarrow$ direction, set $Y = \Omega^X$.  Then $\chi_U = \lambda (x,p).p(x)$ shows that $U = \{(x,p)\ |\ p(x) = \top \}$ is an open subset of $X\times\Omega^X$.  (That $\chi_U$ is continuous is what is not necessarily true classically.)  Since $\pi_2$ is closed, we have $\forall_X \equiv \chi_{\pi_2[U^c]^c} : \Omega^X\to\Omega$.  Now we show it has the desired properties.
$$\begin{align}
\chi_{\pi_2[U^c]^c}(p) = \top & \iff p \notin \pi_2[U^c] \\
                              & \iff \forall x\in X. (x,p)\notin U^c \\
                              & \iff \forall x\in X. (x,p)\in U \\
                              & \iff \forall x\in X. p(x) = \top
\end{align}$$ $\square$
That concludes the whole proof.  I want to take a bit of time to connect this characterization of "compact" to the usual "every open cover has a finite subcover" definition.  First, you may have noticed that the type of $\forall_Q$ means that it is picking out an open set in the space of open sets.  In particular,
$$\begin{align}
\forall_Q(\chi_U) = \top & \iff \forall x\in Q.\chi_U(x) = \top \\
                         & \iff \forall x\in Q. x\in U \\
                         & \iff Q \subseteq U
\end{align}$$
In other words, $Q \subseteq X$ is compact if and only if its open neighborhoods, $\{ U\in \mathcal{O}X\ |\ Q \subseteq U \}$, is an open set in the space of open sets, $\mathcal{O}X$.  This is the significance of compactness.  Where the "finite subcover" stuff comes in is the topology on open sets (and from there on function spaces in general), namely the Scott topology.  A set of open sets, $H$, is Scott-open iff the following two conditions hold.  First, if $U \in H$ and $U \subseteq V$ then $V \in H$.  Second, if $(\bigcup \mathcal{U})\in H$ where $\mathcal{U}$ is a directed subset of $\mathcal{O}X$ then $\exists V\in\mathcal{U}.V \in H$.  The latter condition is equivalent for arbitrary $\mathcal{U}$ rather than directed ones, to the existence of a finite union of $V\in\mathcal{U}$ being in $H$.  (We just build a directed set from $\mathcal{U}$ by taking all finite unions.)  If we set $H = \{ U \in \mathcal{O}X\ |\ Q \subseteq U \}$, we get the usual "every open cover has a finite subcover" definition of a compact set.
In conclusion, the synthetic perspective can be a powerful tool for proving results, but even sticking to classical topology the synthetic perspective can clarify much of what's happening.  For example, a space is discrete iff $=:X\times X\to \Omega$ is continuous, and it is Hausdorff iff $\neq:X\times X \to\Omega$ is continuous.  (Here's another little prooflet: if $X$ is Hausdorff and $Q\subseteq X$ is compact, then $Q$ is closed. Proof: $\chi_{Q^c} = \lambda x.\forall_Q(\lambda y.x\neq y)\square$.) There's a classically invisible notion called overtness which is dual to compactness, namely $\exists_O : \Omega^X\to\Omega$ such that $\exists_O(p) = \top \iff \exists x\in O.p(x)=\top$ means $O$ is an overt subset of $X$.  All classical spaces are overt because arbitrary unions of open sets are open.  Another nice aspect of synthetic topology is that it is directly related to computer science and can serve as a bridge between topologists and computer scientists.  You can actually run these proofs!  The first link to Martin Escardo's work has some examples.
