Example 3.8 in Awodey's Category Theory

Question

Here is the Example 3.8:

What I don't understand is how the equivalence relation is constructed. I appreciate it if someone here can help me clear this painfully written example by Awodey.

Answer 1

Natural deduction inference rules from logic such as $i_2$ above are not arrows strictly speaking, for example, you have 2 different proofs for arrow $q: \psi \rightarrow \theta$ simply when $\theta=\psi$. You can prove via detour of applying $[p,q]$ (disjunction elimination ) after $i_2$ (disjunction introduction), but you can also directly use reiteration rule or even law of excluded middle to arrive at same conclusion. So without defining additional equivalence relation, equation (3.3) cannot hold which is required to further define coproduct objects. Once we mentally identify different but equivalent proofs, then equation (3.3) or (3.4) makes unique sense (like up to isomorphism) and thus strictly holds.

Category theory is all about spotting universal property, and usually we need to add some equivalence relation to achieve so.