Interpreting proofs in $LJ_{\wedge}$ Consider the sequent of $LJ_{\wedge}$ for which you have already found proofs for (which I have)


*

*$A\wedge B \vdash B \wedge A$

*$A\wedge B \vdash B\wedge B$

*$A\wedge(B\wedge C) \vdash (A\wedge B)\wedge C$
Suppose we are given a categorical interpretation $[[-]]:\underline{Syn}(LJ_{\wedge})\rightarrow \underline{Set}$. 
Where $\underline{Syn}(LJ_{\wedge})$ is the syntactic category of $LJ_{\wedge}$. And $\underline{Set}$ is the category of sets. 
Take a guess as to the functions in $\underline{Set}$ which interpret these proof and verify your guess by working through the definition of the categorical interpretation. 
I would like an answer to (i) (or any one you please) so that I may attempt the rest on my own. I vaguely get what I need to do. I have a proof for (i) as follows 
$\cfrac{ B\vdash B \hspace{24pt} A\vdash A \hspace{12pt} (\wedge R)}
{\cfrac{B,A \vdash B\wedge A \hspace{12pt}(exch)}{\cfrac{A,B \vdash B\wedge A\hspace{12pt}(\wedge L)}
{A\wedge B \vdash B\wedge A}}}$
The things in brackets show which inference rules have been used to proceed to the next line of the proof. 
I would start the first line as $\operatorname{id}_{[[B]]}:[[B]]\rightarrow [[B]]$ and $\operatorname{id}_{[[A]]}:[[A]]\rightarrow [[A]]$. Then I would write the next line as $[[B]]\times [[B]]\rightarrow [[B\wedge B]]$...Is what I am doing right. Would liek to see an example to see "how it's written" and what needs to be done. 
 A: You can think of $A \vdash B$ as being represented by* $\text{Hom}([\![A]\!],[\![B]\!])$, then a rule is essentially a function from a product of homsets to a homset.  $\cfrac{}{A \vdash A}$ is a function from the empty product, i.e. an element of $\text{Hom}([\![A]\!],[\![A]\!])$ which is indeed witnessed by $id_A$.
If by definition $[\![A\land B]\!] \stackrel{\varphi}{\cong} [\![A]\!]\times[\![B]\!]$ then
$\land R$ is then the function $$\text{Hom}([\![A]\!],[\![B]\!])\times\text{Hom}([\![C]\!],[\![D]\!])\to\text{Hom}([\![A]\!]\times[\![C]\!],[\![B]\!]\times[\![D]\!])$$ which comes from the functorial action of categorical products often written $(f,g)\mapsto f\times g$ followed by $\varphi^{-1}$. $exch$ is just precomposition with $\sigma_{AB} : [\![A]\!]\times [\![B]\!]\to [\![B]\!]\times [\![A]\!]$. $\land L$ is just precomposition by the above isomorphism.  The arrow corresponding to your proof is then the composition of these functions, which gives: $$\varphi^{-1}\circ (id\times id) \circ \sigma\circ \varphi : [\![A\land B]\!]\to[\![B\land A]\!]$$ $id\times id = id$ so we can simplify and if we identify $[\![A \land B]\!]$ with $[\![A]\!]\times[\![B]\!]$ then $\varphi$ (and its inverse) become $id$ as well and the whole thing just simplifies to $\sigma$.
If we don't identify $[\![A \land B]\!]$ and $[\![A]\!]\times[\![B]\!]$ up to (natural) isomorphism by definition, then $\land L$ is still precomposition by $\varphi$, but $\varphi$ is no longer a priori an isomorphism.  Similarly, $\land R$ can be defined the same way but $\varphi^{-1}$ is no longer a priori the inverse of $\varphi$ or an inverse of anything, call it $\psi$ instead. (If you like, you can combine it with $-\times -$ into a single binary operation representing $\land R$.)  The end result is the same: $$\psi\circ \sigma\circ \varphi : [\![A\land B]\!]\to[\![B\land A]\!]$$
Given the rules for $\land$ you can derive that $\varphi$ and $\psi$ are mutually inverse and unique.  That is, you can show that $[\![A \land B]\!]$ satisfies the universal property of the categorical product.  As a side note, it's Yoneda's lemma that lets us identify certain rules as pre-/post-composition with some arrow, e.g. $\land L$. At any rate, the above probably doesn't exactly correspond to the definition of categorical interpretation you have, so you will need to adjust as appropriate.
* In more complex cases, this needs a bit more finesse.
