Finding morphisms beetwen formulas in category

43 Views Asked by At

Let two formulas A and B are isomorphic when there are $f:A\vdash B$ and $g:B\vdash A$ such that the compositions $g\circ f$ and $f\circ g$ are equal respectivly to the identity derivations on A and B. I want to find these morphisms $f$ and $g$ in the case of two formulas $(A\land B)\rightarrow C$ and $B\rightarrow (A\rightarrow C)$. Using adjunction (conjunction and implication as the left and the right adjoint), I see the following: $$((A\land B)\rightarrow C,B\rightarrow (A\rightarrow C))\simeq (B\land ((A\land B)\rightarrow C),A\rightarrow C)\simeq (A\land (B\land ((A\land B)\rightarrow C)),C)$$, then natural isomorphism and counit of adjunction. I just need a help for explicit defining morphisms $f$ and $g$ which compositions will be identities.