Is $S^1\vee S^1$ an Eilenberg-Mac Lane Space to a Homotopy Purist? I believe that $S^1\vee S^1$ is the Eilenberg-Mac Lane space $K(\mathbb{Z}\ast\mathbb{Z},1)$. One can prove this by constructing its universal cover and observing that it is contractible.
My question is this:
Is there a simple homotopy-theoretic proof of this result that does not use connected covers?
I have never seen one appear in any text. Repeated attemps by myself to use the usual tools (Hilton-Milnor Theorem, examine the fibre of the inclusion $S^1\vee S^1\hookrightarrow S^1\times S^1$, etc...) to prove this elementary result have met with connectivity issues or similar problems.
 A: I think the following can be turned into a proof, but I haven't checked the details. 
By a result of Milnor, $\Omega (S^1 \vee S^1)$ coincides up to homotopy with $F(S^0 \vee S^0)$, the free group functor on the pointed set $S^0 \vee S^0$. By a version of the Hilton-Milnor theorem, the latter coincides up to homotopy with $F(S^0) \ast F(S^0)$, the latter being the free
product with amalgamation of simplicial free groups. But $F(S^0)$ coincides with $\Bbb Z$ up to homotopy. Hence, 
$\Omega (S^1 \vee S^1)$ coincides up to homotopy with $\Bbb Z \ast \Bbb Z$ (as a space). In particular, $\Omega (S^1 \vee S^1)$ is homotopically discrete, which gives the result you are after (in conjunction with the van Kampen theorem).
A: This is not really an answer. The inclusion of homotopy $1$-types into homotopy types has a left adjoint $\tau_{\le 1}$ given by truncation, and hence preserves homotopy limits (e.g. products). The question at hand is whether there is a homotopy-theoretic way to see that it also preserves certain homotopy colimits, namely a certain shape of homotopy pushout. 
One might ask more generally what happens when $1$ is replaced by $n$, and here I believe it's not true that the inclusion of homotopy $n$-types preserves homotopy pushouts; e.g. I don't believe it's true that the wedge sum of two homotopy $n$-types is another homotopy $n$-type. (The first counterexample that comes to mind only works rationally: rationally $S^2$ is a $2$-type, but $S^2 \vee S^2$ has rational homotopy in arbitrarily high degrees.)
So there's something special about the inclusion of homotopy $1$-types. At this point you might be happy to learn that it's possible to develop covering space theory for groupoids without any reference to topological spaces. I think this is already enough to prove the desired result, by a construction, at the level of groupoids, of the universal cover of $BG \vee BH$. In fact it ought to be possible to completely describe the covering theory of $BG \vee BH$ at the level of groupoids, leading to the Kurosh subgroup theorem. For some indication of how this might be done see this blog post, which has some pictures of the special case $G = C_2, H = C_3$. 
A: $\renewcommand{\deloop}{\mathbf{B}}\renewcommand{\sph}{\mathbb{S}} $ 
Ans 1: Calculate the homotopy fiber of the map $\sph^1\vee \sph^1\to \deloop F_2$ classifying the generators.  This (by distributivity/Mather's Cube Theorems) is the pushout of the two maps $\langle x,y\rangle \to \langle x,y\rangle/\langle x\rangle$ and $\langle x,y\rangle \to \langle x,y\rangle/\langle y\rangle$; that this pushout is contractible boils down to the combinatorial exercise that a word in $\{ x,y \}$  knows what its letters are.  (If you like, this is the homotopy reason for the connected cover story; it may also be what Qiaochu is getting at, but I'm not quite sure I can tell for sure)
Ans 2: The loopspace functor $\Omega$ from connected pointed spaces $\mathrm{Top}_{0,*}$ to (tame-enough) grouplike $A_\infty$-spaces has a homotopy  inverse $\mathbf{B}$.
In particular, $\deloop$ sends colimits to colimits, and $\deloop\mathbb{Z}\simeq\sph^1$.

Ans 2 may sound fancier than Ans 1, but they're actually built from the same tools.
