Revise the solution to I.5.8

[BillXWB]

We are talking about an abitrary category here, so it is better to avoid things related to elements.

[hooyuser]

(The format of my comments looks weird because some hacks are necessary to work around the bugs of Github markdown for now)

Thanks for your effort! I agree about the problematic steps in this original proof you've pointed out, which seem to resort to the $\mathsf{Set}$ category subconsciously.

---

As for the revision, I tend to avoid asserting

$\mathsf{C}_{A, B}$

and $\mathsf{C}_{B, A}$ are actually the same

because of the tricky part of set theory that may be concerned.

Someone picky can argue the two categories are not the same because technically the triple $(C,f_1,f_2)$ is different from

$(C,f_2,f_1)$ in the sense of set theory. And that's exactly one of the reasons why we turn to an arrow-theory language.

---

If using the hint, I believe one can just show that $(B\times A,\pi_2,\pi_1)$ is final in $\mathsf{C}_{A,B}$ given that $(B\times A,\pi_1,\pi_2)$ is final in

$\mathsf{C}_{B,A}\ .$ This should be straightforward by checking the universal property.