Hi all,

In trying to solve exercise 4.2.1 in Typeclassopedia, I’ve come up with the following:

To prove:
pure f <*> x = pure (flip ($)) <*> x <*> pure f

Proof:

pure (flip ($)) <*> x <*> pure f     = (interchange)
pure (flip ($)) <*> pure ($ f) <*> x = (homomorphism)
pure (flip ($) ($ f)) <*> x          = (definition of flip)
pure ($ ($ f)) <*> x                 = (interchange)
x <*> pure ($ f)                     = (interchange) (Is this step valid?)
pure f <*> x
Is the last step in my proof valid?

Thanks,
-db