<div dir="ltr"><div>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`?</div><div><br></div><div>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`.</div><div>Equivalently, `g . second h == second h . g` (where `second h (a,b) = (a, h b)`).</div><div><br></div><div>Thanks,  -- Conal</div></div>