There are many equivalent ways of defining the notion of compact space, but some require some kind of choice principle to prove their equivalence. For example, a classical result is that for $X$ to be compact, it is necessary and sufficient that every ultrafilter on $X$ converge to a point in $X$. The necessity is easy to prove, but the sufficiency requires a choice principle to the effect that every filter can be extended to an ultrafilter.
Some years ago I heard from a very good categorical topologist that many, perhaps most of the useful properties of compact spaces $X$ readily flow from the fact that for every space $Y$, the projection map $\pi: X \times Y \to Y$ is closed. Of course that is a very classical consequence of compactness which can be left as an exercise to beginners in topology, and I was struck by the topologist's assertion that you could in fact use this as a definition of compactness, and that this is a very good definition for doing categorical topology. (I am still not sure what he really meant by this, but that's not my question.)
My own proof that this condition implies compactness goes as follows. Let $Y$ be the space of ultrafilters on the set $X$ with its usual compact Hausdorff topology, and suppose the projection $\pi: X \times Y \to Y$ is a closed map. Let $R \subseteq X \times Y$ be the set of pairs $(x, U)$ where the ultrafilter $U$ converges to the point $x$. One may show that $R$ is a closed subset, so the image $\pi(R)$ is closed in $Y$. But every principal ultrafilter (one generated by a point) converges to the point that generates it, so every principal ultrafilter belongs to $\pi(R)$. Now principal ultrafilters are dense in the space of all ultrafilters, so $\pi(R)$ is both closed and dense, and therefore is all of $Y$. This is the same as saying that every ultrafilter on $X$ converges to some point of $X$, and therefore $X$ is compact.
I was at first happy with this proof, but later began to wonder if it's overkill. Certainly it uses heavily the choice principle mentioned above, and my question is whether the implication I just proved above really requires some form of choice like that.
Best Answer
Martin Escardó wrote a very nice note "Intersections of compactly many open sets are open" which you might want to read.