title: Proving Composition Applicative law for ((->) r) type
body: <p>The Composition Applicative Law is as follows:</p>
  
  <pre><code>pure (.) &lt;*&gt; u &lt;*&gt; v &lt;*&gt; w = u &lt;*&gt; (v &lt;*&gt; w)
  </code></pre>
  
  <p>Here's my attempt at proving the Composition law for the <code>((-&gt;) r)</code> type:</p>
  
  <p>RHS:</p>
  
  <pre><code>u &lt;*&gt; (v &lt;*&gt; w)
  u &lt;*&gt; ( \y -&gt; v y (w y) )
  \x -&gt; u x ( (\y -&gt; v y (w y)) x )
  \x -&gt; u x ( v x (w x)) -- (A)
  </code></pre>
  
  <p>LHS: </p>
  
  <pre><code>pure (.) &lt;*&gt; u &lt;*&gt; v &lt;*&gt; w
  const (.) &lt;*&gt; u &lt;*&gt; v &lt;*&gt; w
  (\f -&gt; const (.) f (u f)) &lt;*&gt; v &lt;*&gt; w
  (\f -&gt; (.) (u f)) &lt;*&gt; v &lt;*&gt; w
  (\g -&gt; (\f -&gt; (.) (u f)) g (v g)) &lt;*&gt; w
  \x -&gt; (\g -&gt; (\f -&gt; (.) (u f)) g (v g)) x (w x)
  -- Expanding labmda by applying to x
  \x -&gt; ((\f -&gt; (.) (u f)) x (v x)) (w x)
  \x -&gt; (( (.) (u x)) (v x)) (w x)
  
  \x -&gt; ((u x) . (v x)) (w x) -- (B)
  </code></pre>
  
  <p>I don't think (A) &amp; (B) are equivalent, so where did I make a mistake? I would appreciate any help or suggestions. </p>