Two equivalent definitions of weak equivalences of simplicial sets In and André Joyal and Myles Tierney their Notes on Simplicial Homotopy, two different definitions of a weak equivalence are given, which they say are equivalent (p. 59). I, however, only see why the one implies the other and would like some help in showing the converse direction. The definitions are:

Definition 1. A morphism $f : X \rightarrow Y$ is a weak equivalence if for every Kan complex $K$, the induced map 
  $$
[f, K] : [Y, K] \rightarrow [X, K]
$$
  of morphisms up-to-homotopy is a bijection. 

and

Definition 2. A morphism $f : X \rightarrow Y$ is a weak equivalence if for every square of the form 
  $\require{AMScd}$
  \begin{CD}
    X @>x>> \overline X\\
    @V f V V @VV \overline f V\\
    Y @>>y> Y
\end{CD}
  where $x, y$ are anodyne, $\overline X, \overline Y$ are Kan, the induced diagonal filler $\overline f$ is a homotopy equivalence. 

To see that Definition 1 implies Definition 2, suppose that $f$ is a Definition-1-weak-equivalence and we are given a square as above. Then by 3-for-2 of Definition 1 (which I know how to show), we have that $yf$ is a weak equivalence, and thus also that $\overline f x$ is. By the same property, it follows that $\overline f$ is a weak equivalence. Now $\overline f$ is a weak equivalence between Kan complexes, which using Definition 1, can easily be shown to be a homotopy equivalence.
The only idea that I have for the converse direction is that we could try to show that $K^f : K^Y \rightarrow K^X$ is a homotopy equivalence, from which Definition 1 directly follows. However, I wouldn't know how to build anodyne maps from $X \rightarrow K^Y$ and from $Y \rightarrow K^X$. 
Can anyone help me show that Definition 2 implies Definition 1?
Note: I also don't know how to show 3-for-2 for Definition 2. In particular, I'm not able to prove that $gf$ is a w.e. whenever $f$ and $g$ are. So, if you use that property in your answer I would appreciate it if you also explain that step.
 A: This is a bit tough because it depends on the context and I'm not deeply familiar with these notes. Here is a suggestion: consider a Kan complex $K$ and now consider the map $K^Y \to K^X$. Build a square $\require{AMScd}$
\begin{CD}
    X @>x>> \overline X\\
    @V f V V @VV \overline f V\\
    Y @>>y> \overline Y
\end{CD}
where $X\to \overline X$ is anodyne and $\overline X$ is Kan, this exists by Theorem 3.1.1, similarly for $Y$. It follows from Definition 2 that $\overline f$ is a homotopy equivalence. Now, we obtain a dual diagram:
\begin{CD}
    K^X @<K^x<< K^\overline X\\
    @AK^fAA @AA K^\overline f A\\
    K^Y @<<K^y< K^\overline Y
\end{CD}
It follows from Theorem 3.2.1 that $K^x$ and $K^y$ are trivial fibrations between Kan complexes and by Prop 3.2.5, they are homotopy equivalences. Since $\overline f$ is a homotopy equivalence, it follows that $K^\overline f$ is a homotopy equivalence (try to prove this, it is stated but I think not proved in the notes). Thus, $K^f$ is a homotopy equivalence between Kan complexes and hence we get Definition 1.
