Compact spaces that depend on choice? I've often encountered topological spaces like $2^\omega$, where there is a short proof of compactness using Tychonoff's theorem and a long proof of compactness not using Tychonoff's theorem. Are there situations where this is not the case, i.e. the compactness of the space depends on Tychonoff's theorem?
Essentially, I'm looking for any examples of topological spaces $(X,\tau)$ such that
1.  $(X,\tau)$ exists in ZFC.
2. $(X,\tau)$, or something more or less equivalent, exists in some model of ZF without choice.
3. $(X,\tau)$ is compact in ZFC but not in the other model.
By "more or less equivalent" I mean that they are constructed in the same way, or have similar definitions, or have the same name, or anything else that would make them analogous; my knowledge of set theory is not particularly deep, so the notion is a little fuzzy.
 A: As mentioned in the comments, you can easily get lots of examples by reverse-engineering from the proof that Tychonoff's theorem implies AC.  There are more natural examples, though.
In particular, for instance, $X=\{0,1\}^{\mathcal{P}(\mathbb{N})}$ (with the product topology) cannot be proven to be compact in ZF.  To prove this consider for each $n\in\mathbb{N}$ the function $F_n:\mathcal{P}(\mathbb{N})\to\{0,1\}$ defined by $F_n(S)=1$ if $n\in S$ and $F_n(S)=0$ if $n\not\in S$.  Then it is easy to verify that $A=\{F_n:n\in\mathbb{N}\}$ is an infinite discrete subset of $X$.  If $X$ is compact, then $A$ has an accumulation point.  But an accumulation point of $A$ can be shown to be the same thing as the characteristic function of a nonprincipal ultrafilter on $\mathbb{N}$.  So, in a model of ZF where no such nonprincipal ultrafilters exist, $A$ will have no accumulation points, and $X$ will not be compact.
It follows that if $Y$ is any $T_1$ space with more than one point and $I$ is any set with cardinality at least $\mathfrak{c}$, then $Y^I$ cannot be proven to be compact in ZF (since $X$ embeds in it as a closed subspace).
