<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Hi all,<div><br></div><div>In trying to solve exercise 4.2.1 in <i>Typeclassopedia</i>, I’ve come up with the following:</div><div><br></div><div><div style="box-sizing: border-box; margin: 0px; font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif; font-size: 14px; line-height: 20px;"><strong style="box-sizing: border-box;">To prove:</strong></div><pre style="box-sizing: border-box; overflow: auto; font-size: 14px; padding: 0px; margin-right: 2em; margin-left: 2em; line-height: 20px; word-break: break-all; word-wrap: break-word; background-color: rgb(255, 255, 255); border: 0px; border-top-left-radius: 2px; border-top-right-radius: 2px; border-bottom-right-radius: 2px; border-bottom-left-radius: 2px; white-space: pre-wrap;"><code style="box-sizing: border-box; padding: 0px; border-top-left-radius: 0px; border-top-right-radius: 0px; border-bottom-right-radius: 0px; border-bottom-left-radius: 0px; border: 0px;">pure f <*> x = pure (flip ($)) <*> x <*> pure f
</code></pre><p style="box-sizing: border-box; margin: 1em 0px 0px; font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif; font-size: 14px; line-height: 20px;"><strong style="box-sizing: border-box;">Proof:</strong></p><pre style="box-sizing: border-box; overflow: auto; font-size: 14px; padding: 0px; margin-right: 2em; margin-left: 2em; line-height: 20px; word-break: break-all; word-wrap: break-word; background-color: rgb(255, 255, 255); border: 0px; border-top-left-radius: 2px; border-top-right-radius: 2px; border-bottom-right-radius: 2px; border-bottom-left-radius: 2px; white-space: pre-wrap;"><code style="box-sizing: border-box; padding: 0px; border-top-left-radius: 0px; border-top-right-radius: 0px; border-bottom-right-radius: 0px; border-bottom-left-radius: 0px; border: 0px;">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</code></pre><div>Is the last step in my proof valid?</div></div><div><br></div><div>Thanks,</div><div>-db</div><div><br></div></body></html>