In https://www.cs.ox.ac.uk/ralf.hinze/LN.pdf
On page 10, equations (13) and (14) it seems to me that outl on the left of the equations is not the same outl as on the right (likewise for outr).
I believe the outl on the left goes from some object AxB to A, while the outl on the right goes from A’xB’ to A’, where k1 goes from A to A’. So, the equations maybe should have been written
k1 . outl = outl’ . (k1xk2)
I am traveling and on a phone so please forgive the lack of a diagram. If anyone can confirm that the two appearances of outl (and similarly outr) are actually not (necessarily) the same morphism, that would be great. I interjected necessarily since the diagram should still make sense if k1: A->A and k2: B->B, but I believe the purpose of the equations was for general k1: A->A’ and k2: B->B’.
Thank you.
Yes, you are right. outl and outr are natural transformations, and here the writers abuse notation to use them as arrows, while instead they should be specific components at the right types.
This confusion probably comes from how this is implemented in functional programming languages like Haskell, where outl :: (a, b) -> a is regular function.