@FabricioOlivetti, sure thing! It was a good exercise to spell everything out. As we see, there are a lot of implied details in the compact statements of category theory.

I need to do a couple more steps to complete the proof.