
23 Jul
2018
23 Jul
'18
12:29 a.m.
Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f a, b)`), perhaps as a free theorem for the type of `g`? Note that `(A,)` and `(B,)` are functors and that `g` is a natural transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`. Equivalently, `g . second h == second h . g` (where `second h (a,b) = (a, h b)`). Thanks, -- Conal