\section{Display Calculi}\label{Sec:display}

%Hyland and de Paiva\marginpar{Raj still working this out. Please do
%  not delete.} define two objects $B$ and $C$ to be independent
%if the following property holds:
%if there is a map $A \mlcn B \to C \mldn D$ then there exists an $E$ such that 
%$A \to E \mldn C$
%and
%$E \mlcn B\to D$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Syntax}

\begin{definition}
BiILL-\emph{formulae} are defined using the grammar below
where $p$ is from some fixed set of propositional variables 
$$
  A ::= p \mid I \mid \bot \mid A\otimes A \mid A\parr A \mid A\limp A \mid A\excl A
$$
\emph{Antecedent} and \emph{succedent} BiILL-\emph{structures} (also
known as antecedent and succedent parts) are defined by
mutual induction, where $\Phi$ is a structural constant and
$A$ is a BiILL-formula:
$$
  X_a ::= A \mid \Phi \mid X_a,X_a \mid X_a<X_s
\qquad
\qquad
\qquad
  X_s ::= A \mid \Phi \mid X_s,X_s \mid X_a>X_s
$$
FILL-formulae are BiILL-formulae with no occurrence of the exclusion
connective $\excl$. FILL-structures are $\biill$-structures with
no occurrence of $<$, and containing only FILL-formulae.
%
We stipulate that $\otimes$ and $\parr$ bind tighter than $\limp$ and
$\excl$, that comma binds tighter than $>$ and $<$, and resolve
$A\limp B\limp C$ as $A\limp(B\limp C)$.
%
A BiILL- (resp. FILL-) \emph{sequent} is a pair comprising an antecedent and a
succedent BiILL- (resp. FILL-) structure, written $X_a\turn X_s$. 
\end{definition}

% \begin{definition}
% BiILL-\emph{formulae} are defined using the grammar below
% where $p$ is from some fixed set of propositional variables:
% $$
%   A ::= p \mid I \mid \bot \mid A\otimes A \mid A\parr A \mid A\limp A \mid A\excl A
% $$

% \emph{Antecedent} and \emph{succedent} BiILL-\emph{structures} are defined by
% mutual induction as follows, where $\Phi$ is a structural constant and
% $A$ is a BiILL-formula:
% $$
%   X_a ::= A \mid \Phi \mid X_a,X_a \mid X_a<X_s
% \qquad
%   X_s ::= A \mid \Phi \mid X_s,X_s \mid X_a>X_s
% $$
% FILL-formulae are BiILL-formulae with no occurrence of the exclusion
% connective $\excl$. FILL-structures are $\biill$-structures with
% no occurrence of $<$, and containing only FILL-formulae.

% We stipulate that $\otimes$ and $\parr$ bind tighter than $\limp$ and
% $\excl$, that comma binds tighter than $>$ and $<$, and resolve
% $A\limp B\limp C$ as $A\limp(B\limp C)$.

% A BiILL- (resp. FILL-) \emph{sequent} is a pair comprising an antecdent and a
% succedent BiILL- (resp. FILL-) structure, written $X_a\turn X_s$.
% \end{definition}

%\begin{definition}
%BiILL-\emph{formulae} and BiILL-\emph{structures} are defined using
%the following grammars, where $p$ is from some fixed set of
%propositional variables, and $\Phi$ is a structural constant:
%$$
%  A~~B ::= p \mid I \mid \bot \mid A\otimes B \mid A\parr B \mid A\limp B \mid A\excl B
%\qquad
%  X~~Y ::= A \mid \Phi \mid X,Y \mid X>Y \mid X<Y
%$$
%FILL-formulae are BiILL-formulae with no occurrence of the exclusion
%connective $\excl$. FILL-structures are $\biill$-structures with
%no occurrence of $<$, and containing only FILL-formulae.
%
%We stipulate that $\otimes$ and $\parr$ bind tighter than $\limp$ and
%$\excl$, that comma binds tighter than $>$ and $<$, and resolve
%$A\limp B\limp C$ as $A\limp(B\limp C)$.
%\end{definition}

%\begin{definition}
%We say that the structure $X$ \emph{is positive in} $X$. A proper
%substructure is positive (resp. \emph{negative}) in the structure
%\begin{itemize}
%\item $X,Y$ if it is positive (resp. negative) in $X$ or $Y$;
%\item $X>Y$ if it is negative (resp. positive) in $X$ or positive (resp.
%negative) in $Y$;
%\item $X<Y$ if it is positive (resp. negative) in $X$ or negative (resp.
%positive) in $Y$.
%\end{itemize}
%A BiILL- (resp. FILL-) \emph{context} is either a hole $[-]$ or a BiILL- (resp.
%FILL-) structure containing exactly one occurrence of $[-]$. We write $X[-]^i$
%for $i\in\{+,-\}$ to indicate whether the hole is positive or negative.
%A BiILL- (resp. FILL-) \emph{sequent} is a pair of BiILL- (resp.
%FILL-) structures written $X\turn Y$. A structure is an
%\emph{antecedent}
%(resp. \emph{succedent}) part of $X\turn Y$ if it is positive (resp. negative)
%in $X$ or negative (resp. positive) in $Y$. We require that no structure
%$X>Y$ may be an antecedent part, and no structure $X<Y$ may be a succedent part.
%We take the convention that all sequents seen in this paper are well-formed in
%this sense.
%\end{definition}

\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}

The display calculi for FILL and BiILL are given in Fig.~\ref{Fig:dc}.

\begin{figure}[t]
  \begin{tabular}[c]{l@{\extracolsep{3cm}}l}
\multicolumn{2}{l}{Cut and identity:}
  \\[0px]
  \qquad  \qquad
  \AxiomC{(id)\quad$p\turn p$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$A\turn Y$}
  \LeftLabel{(cut)\,}
  \BinaryInfC{$X\turn Y$}
  \DisplayProof
\\%[5px]
\multicolumn{2}{l}{Logical rules:}
\\[0px]
\qquad\qquad
  \AxiomC{$\Phi\turn X$}
  \LeftLabel{($I\turn$)\,}
  \UnaryInfC{$I\turn X$}
  \DisplayProof
  &
  \AxiomC{($\turn I$)\quad$\Phi\turn I$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{($\bot\turn$)\quad$\bot\turn\Phi$}
  \DisplayProof
  &
  \AxiomC{$X\turn\Phi$}
  \LeftLabel{($\turn\bot$)\,}
  \UnaryInfC{$X\turn\bot$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$A,B\turn X$}
  \LeftLabel{($\otimes\turn$)\,}
  \UnaryInfC{$A\otimes B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$Y\turn B$}
  \LeftLabel{($\turn\otimes$)\,}
  \BinaryInfC{$X,Y\turn A\otimes B$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$A\turn X$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\parr\turn$)\,}
  \BinaryInfC{$A\parr B\turn X,Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A,B$}
  \LeftLabel{($\turn\parr$)\,}
  \UnaryInfC{$X\turn A\parr B$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\limp\turn$)\,}
  \BinaryInfC{$A\limp B\turn X>Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn A>B$}
  \LeftLabel{($\turn\limp$)\,}
  \UnaryInfC{$X\turn A\limp B$}
  \DisplayProof
\\%[5px]
\multicolumn{2}{l}{Structural rules:}
\\[5px]
\multicolumn{2}{c}{
  \AxiomC{$X\turn Y>Z$}
  \doubleLine
  \LeftLabel{(rp)\,}
  \UnaryInfC{$X,Y\turn Z$}
  \DisplayProof
  \qquad
  \AxiomC{$X, Y \turn Z$}
  \doubleLine
  \LeftLabel{(rp)\,}
  \UnaryInfC{$Y\turn X>Z$}
  \DisplayProof
  \qquad
  \AxiomC{$X<Y\turn Z$}
  \doubleLine
  \LeftLabel{(drp)\,}
  \UnaryInfC{$X\turn Y,Z$}
  \DisplayProof
  \qquad
  \AxiomC{$X \turn Y,Z$}
  \doubleLine
  \LeftLabel{(drp)\,}
  \UnaryInfC{$X<Z\turn Y$}
  \DisplayProof
}
\\[10px]
  \qquad\qquad
  \AxiomC{$X,\Phi\turn Y$}
  \doubleLine
  \LeftLabel{($\Phi\turn$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof
  &
  \AxiomC{$X\turn \Phi,Y$}
  \doubleLine
  \LeftLabel{($\turn\Phi$)\,}
  \UnaryInfC{$X\turn Y$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$W,(X,Y)\turn Z$}
  \doubleLine
  \LeftLabel{(Ass $\turn$)\,}
  \UnaryInfC{$(W,X),Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\turn (X,Y),Z$}
  \doubleLine
  \LeftLabel{($\turn$ Ass)\,}
  \UnaryInfC{$W\turn X,(Y,Z)$}
  \DisplayProof
\\[10px]
  \qquad\qquad
  \AxiomC{$X,Y\turn Z$}
  \LeftLabel{(Com $\turn$)\,}
  \UnaryInfC{$Y,X\turn Z$}
  \DisplayProof
  &
  \AxiomC{$X\turn Y,Z$}
  \LeftLabel{($\turn$ Com)\,}
  \UnaryInfC{$X\turn Z,Y$}
  \DisplayProof
\\[10px]
% \multicolumn{2}{c}{
%   \AxiomC{$W\vdash (X> Y), Z$}
%     \LeftLabel{(Grnb)}
%   \UnaryInfC{$W\vdash X>(Y,Z)$}
% \DisplayProof
% }
  \qquad\qquad
  \AxiomC{$W,(X<Y)\turn Z$}
    \LeftLabel{(Grnb $\turn$)}
  \UnaryInfC{$(W,X)<Y\turn Z$}
  \DisplayProof
  &
  \AxiomC{$W\vdash (X> Y), Z$}
    \LeftLabel{($\turn$ Grnb)}
  \UnaryInfC{$W\vdash X>(Y,Z)$}
\DisplayProof
\\[5px]
\multicolumn{2}{l}{Further logical rules for $\biilldc$:}
\\[5px]
  \qquad\qquad
  \AxiomC{$A<B\turn X$}
    \LeftLabel{($\excl\turn$)\,}
  \UnaryInfC{$A\excl B\turn X$}
  \DisplayProof
  &
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\turn\excl$)\,}
  \BinaryInfC{$X<Y\turn A\excl B$}
  \DisplayProof
  \end{tabular}
\caption{$\filldc$ and $\biilldc$: display calculi for FILL and BiILL}
\label{Fig:dc}
\end{figure}

\begin{remark}
  For conciseness, we treat comma-separated structures as multisets
  and usually omit explicit use of (Ass $\turn$), ($\turn$ Ass), (Com
  $\turn$) and ($\turn$ Com). The \emph{residuated pair} and
  \emph{dual residuated pair} rules (rp) and (drp) are the
  \emph{display postulates} which give Thm.~\ref{thm:display} below.
  Our display postulates build in commutativity of comma, so 
  the two (Com) rules are derivable. If we wanted to drop
  commutativity~\cite{Cockett:Proof}, we would have to use the more
  general display postulates from~\cite{Gore:SLD}. Note that (drp) may
  create the structure $<$ which has no meaning in FILL, so we will
  return to this issue. For now, observe that proofs of even
  apparently trivial FILL-sequents such as $(p\parr q)\parr r\turn
  p,(q\parr r)$ require (drp) to `move $p$ out the way' so
  ($\turn\parr$) can be applied. Another (drp) then eliminates the $<$
  to restore $p$ to the right. The rule ($\turn$ Grnb) is the
  structural version of Grishin (b), the right hand formula of
  \eqref{eq:wdis}; the rule (Grnb $\turn$) is equivalent.
%
%The antecedent version
% $$
%   \AxiomC{$W,(X<Y)\turn Z$}
%   \UnaryInfC{$(W,X)<Y\turn Z$}
%   \DisplayProof
% $$
%is equivalent and therefore omitted.
%
Fig.~\ref{Fig:Bierman} gives a cut-free proof of the example from Bierman~\eqref{eq:Bierman}.
%, showing the essential use of (drp).
\end{remark}

\begin{figure}%[t]
\footnotesize{\begin{center}$
\AxiomC{$a\turn a$}
\AxiomC{$b\turn b$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$a\parr b\turn a,b$}
\AxiomC{$c\turn c$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(a\parr b)\parr c \turn a,b,c$} \LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c<a \turn b,c$} \LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(a\parr b)\parr c<a\turn b\parr c$}
\AxiomC{$d\turn d$}\LeftLabel{\scriptsize{($\limp\turn$)}}
\BinaryInfC{$b\parr c\limp d \turn ((a\parr b)\parr c<a)>d$}
\AxiomC{$e\turn e$}\LeftLabel{\scriptsize{($\parr\turn$)}}
\BinaryInfC{$(b\parr c\limp d)\parr e \turn (((a\parr b)\parr c<a)>d),e$}\LeftLabel{\scriptsize{($\turn$ Grnb)}}
\UnaryInfC{$(b\parr c\limp d)\parr e \turn ((a\parr b)\parr c<a)>d,e$}\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(b\parr c\limp d)\parr e,((a\parr b)\parr c<a)\turn d,e$}\LeftLabel{\scriptsize{($\turn\parr$)}}
\UnaryInfC{$(b\parr c\limp d)\parr e,((a\parr b)\parr c<a)\turn d\parr e$}\LeftLabel{\scriptsize{(rp)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn (b\parr c\limp d)\parr e>d\parr e$}\LeftLabel{\scriptsize{($\turn\limp$)}}
\UnaryInfC{$(a\parr b)\parr c<a \turn (b\parr c\limp d)\parr e\limp d\parr e$}\LeftLabel{\scriptsize{\textbf{(drp)}}}
\UnaryInfC{$(a\parr b)\parr c \turn a,(b\parr c\limp d)\parr e\limp d\parr e$}
\DisplayProof
%% \hspace{-2.6pt}
%% \AxiomC{$a\turn a$}
%% \AxiomC{$b\turn b$}
%% \BinaryInfC{$a\parr b\turn a,b$}
%% \AxiomC{$c\turn c$}
%% \BinaryInfC{$(a\parr b)\parr c \turn a,b,c$}
%% \UnaryInfC{$(a\parr b)\parr c \turn a,b,c$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,b\parr c$}
%% \AxiomC{$d\turn d$}
%% \BinaryInfC{$(a\parr b)\parr c\turn a,(b\parr c\limp d>d)$}
%% \AxiomC{$e\turn e$}
%% \BinaryInfC{$(a\parr b)\parr c\turn a,((b\parr c\limp d)\parr e>d,e)$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,((b\parr c\limp d)\parr e>d,e)$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,((b\parr c\limp d)\parr e>d,e)$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,((b\parr c\limp d)\parr e>d\parr e)$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,((b\parr c\limp d)\parr e>d\parr e)$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,(b\parr c\limp d)\parr e\limp d\parr e$}
%% \UnaryInfC{$(a\parr b)\parr c\turn a,(b\parr c\limp d)\parr e\limp d\parr e$}
%% \DisplayProof
$\end{center}}
%\caption{(i) Proof of the Bierman example; (ii) proof with
%$<$-deletion.}
\caption{The cut-free $\filldc$-derivation of the example from Bierman.}
%% ; (ii) the result
%%   of applying $<$-deletion to it.
\label{Fig:Bierman}
\end{figure}

\begin{theorem}[Display Property]\label{thm:display}
 For every structure $Z$ which is an antecedent (resp. succedent)
 part of the sequent $X \turn Y$, there is a sequent $Z \turn Y'$
 (resp. $X' \turn Z$) obtainable from $X \turn Y$ using only (rp) and
 (drp), thereby displaying the $Z$ as the whole of one side.
\end{theorem}
%\begin{proof}
%For every binary structural connective, there is a reversible
%rule that allows us to move its left or right argument to the other side
%of turnstile.
%\end{proof}

\begin{theorem}[Cut-Admissibility]\label{thm:cutad}
  From cut-free $\biilldc$-derivations of $X \turn A$ and 
  $A \turn Y$ there is an effective procedure to obtain
  a cut-free $\biilldc$-derivation of $X
  \turn Y$.
\end{theorem}

\begin{proof}
%  The rules of Fig.~\ref{Fig:dc} obey Belnap's conditions for
  $\biilldc$ obeys Belnap's conditions for
  cut-admissibility~\cite{Belnap82JPL}: see
  App.~\ref{app:display}.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Semantics}

\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$.

%These categorical notions can all be formulated as the requirement
%that a certain inductively defined set of arrows exists (satisfying certain
%equations). In particular, the \emph{free} FILL- (resp. BiILL-) category has as
%objects FILL- (resp. BiILL-) formulae, and as arrows only those required by the
%definition (quotiented by the required equations).
\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,B'$ and
  arrows $f:A\to A',f':A'\to A'',g:B\to B'$,
  $(\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 B'}
   \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 B'}
   \qquad
   \xymatrix{(A\limp B)\otimes A \ar[r]^-{\varepsilon} & B}
   \qquad
  \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}

\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)$.
%  (equivalently, an arrow $\tau^a(X)\to\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}

\begin{remark}
Those familiar with categorical logic will note that our use of category theory
here is rather shallow, looking only at whether hom-sets are populated,
and not at the rich structure of equivalences between proofs that
categorical logic supports. This is
an adequate basis for this work because the question of FILL-validity
alone has proved so vexed.
\end{remark}

\begin{theorem}\label{thm:dc=biill}
$\biilldc$ (Fig.~\ref{Fig:dc}) is \emph{sound} and \emph{cut-free complete} for
BiILL-validity.
\end{theorem}
\begin{proof}
$\biilldc$-proof rules and the arrows of the free BiILL-category are
interdefinable.
\end{proof}

\begin{corollary}\label{cor:filldc_complete}
The display calculus $\filldc$ is cut-free complete for FILL-validity.
\end{corollary}
\begin{proof}
Because BiILL-categories are FILL-categories, and $\biilldc$ proofs of
FILL-sequents are $\filldc$ proofs.
\end{proof}

We will return to the question of \emph{soundness} for $\filldc$ in
Sec.~\ref{sec:conserv}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: BiILL succedent drp rp Grnb multiset monoidal bifunctor hom Bierman Hyland de Paiva px Thm residuated Grishin eq wdis interdefinable


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

