\section{Formalising Categorial Semantics}\label{sec:cats}

\begin{definition}\label{Def:FILLcat}
A \emph{FILL-category} is a category equipped with
\begin{itemize}
\item a symmetric monoidal closed structure $(\otimes,I,\limp)$
\item a symmetric monoidal structure $(\parr,\bot)$
\item a natural family of \emph{weak distributivity} arrows $A\otimes(B\parr C)\to(A\otimes B)\parr C$.
\end{itemize}
A \emph{BiILL-category} is a FILL-category where the $\parr$ bifunctor has a
\emph{co-closure} $\excl$, so there is a natural isomorphism between arrows $A
\to B\parr C$ and $A\excl B\to C$.
\end{definition}

To interpret BiILL sequents in the category semantics, we use the following
translation from (antecedent/succeedent) structures to formulae:
\[
\begin{tabular}{|c|c|c|c|c|c|}
\hline & $A$ & $\Phi$ & $X,Y$ & $X>Y$ & $X<Y$ \\
\hline $\tau^a$ & $A$ & $I$ & $\tau^a(X)\otimes\tau^a(Y)$ & & $\tau^a(X)\excl\tau^s(Y)$ \\
\hline $\tau^s$ & $A$ & $\bot$ & $\tau^s(X)\parr\tau^s(Y)$ & $\tau^a(X)\limp\tau^s(Y)$ & \ \\ \hline
\end{tabular}
\]

\begin{definition}\label{Def:valid}
  A FILL- (resp. BiILL-) sequent $X\turn Y$ is \emph{satisfied} by a
  FILL- (resp.\ BiILL-) category if, given any valuation of its
  propositional variables as objects, there exists an arrow
  $I\to\tau^a(X)\limp\tau^s(Y)$.
  It is FILL- (resp. BiILL-) \emph{valid} if
  it is satisfied by all such categories. In fact, we only need to
  check the free categories under their generic valuations.
\end{definition}

%% For the Isabelle proofs we used the equivalent existence of
%% an arrow $\tau^a(X)\to\tau^s(Y)$.
%% \begin{definition}\label{def:tau}
%% We can translate sequents $X\turn Y$ into formulae as $\tau^a(X)\limp\tau^s(Y)$,
%% given the mutually inductively defined antecedent and succedent
%% $\tau$-\emph{translations}:
%% \[
%% \begin{tabular}{|c|c|c|c|c|c|}
%% \hline & $A$ & $\Phi$ & $X,Y$ & $X>Y$ & $X<Y$ \\
%% \hline $\tau^a$ & $A$ & $I$ & $\tau^a(X)\otimes\tau^a(Y)$ & & $\tau^a(X)\excl\tau^s(Y)$ \\
%% \hline $\tau^s$ & $A$ & $\bot$ & $\tau^s(X)\parr\tau^s(Y)$ & $\tau^a(X)\limp\tau^s(Y)$ & \ \\ \hline
%% \end{tabular}
%% \]
%% Hence $\Phi$ and comma are \emph{overloaded} to be translated into
%% different connectives depending on their position%
%% %, but the overloading is more subtle than in traditional Gentzen
%% %sequents. For example, the comma in the sequent $p < (q , p) \turn p$
%% %will become a $\mldn$ via the $\tau$-translation, even though visually
%% %it appears on the left hand side
%% . By uniformly replacing our
%% structural connective $<$ with $>$, we could have also 
%% overloaded $>$ to stand for $\limp$ and $\excl$,
%% which would have avoided the blank spaces in the above table, but we have
%% opted to use different connectives to help visually emphasise whether
%% a given structure lives in BiILL or its fragment FILL.
%% \end{definition}


\begin{definition}\label{def:free}
  The \emph{free} FILL- (resp. BiILL-) category has FILL- (resp.
  BiILL-) formulae as objects and the following arrows (quotiented by
  certain equations) where we are given objects $A, A',A'',B,C$ and
  arrows $f:A\to A',f':A'\to A'',g:B\to C$,
  $(\binop,K)\in\{(\otimes,I),(\parr,\bot)\}$, and where the
  co-closure arrows exist in the free BiILL-category only:
\begin{description}
\item[Category:] 
  $\xymatrix{A \ar[r]^{id} & A}
  \qquad
  \xymatrix{A \ar[r]^-{f'\circ f} & A''}$
\item[Symmetric Monoidal:]

  $\xymatrix{A\binop B \ar[r]^-{f\binop g} & A'\binop C}
   \qquad
  \xymatrix{(A\binop B)\binop C \ar@<0.5ex>[r]^{\alpha} & A\binop(B\binop C)
  \ar@<0.5ex>[l]^{\alpha^{-1}}}
  $   
%\item[\hphantom{Symmetric Monoidal:}]

  $
  \xymatrix{K\binop A \ar@<0.5ex>[r]^-{\lambda} & A
  \ar@<0.5ex>[l]^-{\lambda^{-1}}}
  \qquad
  \xymatrix{A\binop K \ar@<0.5ex>[r]^-{\rho} & A \ar@<0.5ex>[l]^-{\rho^{-1}}}
  \qquad
  \xymatrix{A\binop B \ar[r]^{\gamma} & B\binop A}
  $

\item[Closed:] 
  $$\xymatrix{A\limp B \ar[r]^-{A\limp g} & A\limp C}
   \quad
   \xymatrix{(A\limp B)\otimes A \ar[r]^-{\varepsilon} & B}
   \quad
  \xymatrix{A \ar[r]^-{\eta} & B\limp A\otimes B}$$

\item[Weak Distributivity:]
  $\xymatrix{A\otimes(A'\parr A'') \ar[r]^{\omega} & (A\otimes A')\parr A''}$
\item[Co-Closed:] 

  $$\xymatrix{A\excl B \ar[r]^-{f\excl B} & A'\excl B}
   \qquad
   \xymatrix{A\parr B\excl A \ar[r]^-{\varepsilon} & B}
   \qquad
   \xymatrix{A \ar[r]^-{\eta} & B\parr(A\excl B)}$$
\end{description}
We will suppress explicit reference to
the associativity and symmetry arrows.
\end{definition}

%\subsection{Formalisation of categorical semantics}

Definition~\ref{def:free} can also be written as a deducibility
relation between formulae where we use the ``turnstile'' to assert the
existence of an arrow, without specifying how it is constructed. For
example, the ``rules'' below capture the definition of
``closed'' above in which the finer details of the construction $A \limp g$ are
elided:
\[
\AxiomC{$B \vdash C$}
\UnaryInfC{$A \mlri B \vdash A \mlri C$}
\DisplayProof
\qquad
\AxiomC{}
\UnaryInfC{$(A \mlri B)\mlcn A \vdash B$}
\DisplayProof
\qquad
\AxiomC{}
\UnaryInfC{$ A \vdash B \mlri (A \mlcn B)$}
\DisplayProof
\]

We formalised this deducibility relation using the display calculus
turnstile which we had already defined in Isabelle,
but with only a formula (not a more complex structure) on each side.  
Then the identity arrow and composition of arrows become the usual display
calculus identity rule and cut rule. For example, the ``closure'' 
rules above are encoded as:
\begin{verbatim}
 lolli_monoR == (["B" |- "C"], "A" --o "B" |- "A" --o "C")
 lolliD == ([], ("A" --o "B") &&& "A" |- "B")
 lolliI == ([], "A" |- "B" --o ("A" &&& "B"))
\end{verbatim}
Our encoding is faithful because each arrow required by
Definition~\ref{def:free} is encoded as one such rule giving the rules
\texttt{biill\_cat\_rules} with subset \texttt{fill\_cat\_rules}.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
