- 3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `m$`'d to a box `xs` of arguments == the `m$`ing of `fs` to the `m$`ing of `gs` to xs: `((mid ○) m$ fs m$ gs) m$ xs = fs m$ (gs m$ xs)`.
- 4. When the arguments are `mid`'d, the order of `m$`ing doesn't matter: `fs m$ (mid x) = (mid ($ x)) m$ fs`. In examples we'll be working with at first, order _never_ matters; but down the road, sometimes it will. This Law states a class of cases where it's guaranteed not to.
- 5. A consequence of the laws already stated is that when the functions are `mid`'d, the order of `m$`ing doesn't matter either: TODO
-
+ 3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `m$`'d to a box `xs` of arguments == the `m$`ing of `fs` to the `m$`ing of `gs` to xs: `(mid (○) m$ fs m$ gs) m$ xs = fs m$ (gs m$ xs)`.
+ 4. When the arguments are `mid`'d, the order of `m$`ing doesn't matter: `fs m$ (mid x) = mid ($x) m$ fs`. (Note that it's `mid ($x)`, or `mid (\f. f x)` that gets `m$`d onto `fs`, not the original `mid x`.) Here's an example where the order *does* matter: `[succ,pred] m$ [1,2] == [2,3,0,1]`, but `[($1),($2)] m$ [succ,pred] == [2,0,3,1]`. This Law states a class of cases where the order is guaranteed not to matter.
+ 5. A consequence of the laws already stated is that when the functions are `mid`'d, the order of `m$`ing doesn't matter either: `mid f m$ xs == map (flip ($)) xs m$ mid f`.
+
+<!-- Probably there's a shorter proof, but:
+ mid T m$ xs m$ mid f
+== mid T m$ ((mid id) m$ xs) m$ mid f, by 1
+== mid (○) m$ mid T m$ mid id m$ xs m$ mid f, by 3
+== mid ($id) m$ (mid (○) m$ mid T) m$ xs m$ mid f, by 4
+== mid (○) m$ mid ($id) m$ mid (○) m$ mid T m$ xs m$ mid f, by 3
+== mid ((○) ($id)) m$ mid (○) m$ mid T m$ xs m$ mid f, by 2
+== mid ((○) ($id) (○)) m$ mid T m$ xs m$ mid f, by 2
+== mid id m$ mid T m$ xs m$ mid f, by definitions of ○ and $
+== mid T m$ xs m$ mid f, by 1
+== mid ($f) m$ (mid T m$ xs), by 4
+== mid (○) m$ mid ($f) m$ mid T m$ xs, by 3
+== mid ((○) ($f)) m$ mid T m$ xs, by 2
+== mid ((○) ($f) T) m$ xs, by 2
+== mid f m$ xs, by definitions of ○ and $ and T == flip ($)
+-->