Hi all, I’m stuck in Ex. 10 of *Arrows and Computation*, by Ross Paterson: https://htmlpreview.github.io/?https://github.com/capn-freako/Haskell_Misc/b... https://htmlpreview.github.io/?https://github.com/capn-freako/Haskell_Misc/b... It seems to me that if, in the third step of my proof, I could convert the *left (pure fst)* into *left (first <?>)*, then I could use the **distribution** axiom to convert *pure distr >>> left (first <?>)* into *first (left ) >>> pure distr *. At that point, I would have (starting from the left side of my expression): *first (..) >>> first (..)*, and could apply the functor property of *first*, in order to simplify the expression. Thanks, -db