title: What does the Naturality law for Traversables mean?
body: <p>The Naturality law states that:</p>
  
  <pre><code>t . traverse f == traverse (t . f) -- for every applicative transformer t
  </code></pre>
  
  <p>Now for the RHS of the law, if f has the type <code>Applicative a =&gt; x -&gt; a y</code>, then t has to be of the type <code>(Applicative a, Applicative b) =&gt; a y -&gt; b y</code>, due to the function composition.</p>
  
  <p>For the LHS, traverse f has the type <code>(Applicative a, Traversable c) =&gt; c x -&gt; a (c y)</code>. But since traverse f is composed with t . traverse f, t has to be of the type (c x -> a (c y)) -> b y.</p>
  
  <p>Now, for the LHS, t has the type a (c y) -> b y, but from the RHS it has the type a y -> b y. How is the law sound from a type perspective?</p>
  
  <p>Edit: Fixed the type t in LHS</p>