\documentclass[12pt]{article}
\title{Documentation for {\tt llconnex.sty} \\ Version 0.99}
\author{J.M. Egger}
%\bibliographystyle{plain}

\usepackage{fullpage}
\usepackage{proof} 
\usepackage{llconnex} 

\let\fr\emph
\let\la\emph
\let\opt\texttt
\def\aka{\la{alias}} 
\def\eg{\la{e.g.}} 
\def\etc{\la{\&c}} 
\def\ie{\la{i.e.}} 
\def\llc{{\tt llconnex}} 

\def\scary#1{``#1''} 		
\def\Vec{\mathbf{Vec}_{fd}}
\def\mll{{\sc mll}}

\begin{document}

\maketitle
\tableofcontents

\section{Introduction}

The purpose of \llc\ is 
to define macros for the connectives of linear logic. 
The problem is that different authors use different symbols for 
these connectives, and that we wish to accommodate as many different 
tastes as possible.  

My solution to this problem is two-fold.
Firstly, to adopt the philosophy of Paul Taylor: %which is essentially 
that the source-code of the body of any \TeX\ document should reflect 
what the author {\em means}, rather than the notation which the author 
happens to be using. 
Secondly, to equip \llc\ with options 
which take over the job of translating concepts into symbols 
in accordance with the user's preferred convention.

Thus the correct usage of \llc\ is to include 
\begin{center}
\verb+\usepackage[+$opt_1,\ldots,opt_n$\verb+]{llconnex}+
\end{center}
in the preamble of one's document.
%The various options are discussed at length below.

At present, there exist three sets of options: 
one to control the denotations of conjunctions and disjunctions;
one to control the denotations of negations; and 
one to control the denotations of implications.
Future versions of \llc\ may incorporate yet more.

It is possible to use \llc\ without options---for example, 
the present document was prepared in this way---but this is only
recommended if, as in the present document, the user needs to refer to
symbols independently of the concepts they are intended to represent.

\subsection{System Requirements}

\llc\ makes frequent use of {\tt stmaryrd.sty} 
which appears to have become a standard tool.
It is freely available at \dots\

\section{Conjunctions and Disjunctions}

The macros assigned to each of the (binary) conjunctions and disjunctions
of linear logic are as follows: 
\begin{center}
\begin{tabular}{lll}
  multiplicative conjunction (\aka: tensor, \fr{tenseur}) 
    &$\mapsto$& \verb+\tens+ \\
  multiplicative disjunction (\aka: par) 
    &$\mapsto$& \verb+\parr+ \\
  additive conjunction (\aka: with, \fr{avec}) 
    &$\mapsto$& \verb+\with+, \verb+\avec+ \\
  additive disjunction (\aka: plus) 
    &$\mapsto$& \verb+\plus+ 
\end{tabular}
\end{center}
The default macros for the units corresponding to each binary are
\begin{center}
\begin{tabular}{ccccc}
   \verb+\uftens+ & (unit for \verb+\tens+) & 
 & \verb+\uptens+ & (unite pour \verb+\tens+) 
\\ \verb+\ufparr+ & (unit for \verb+\parr+) & 
 & \verb+\upparr+ & (unite pour \verb+\parr+) 
\\ \verb+\ufwith+ & (unit for \verb+\with+) & 
 & \verb+\upavec+ & (unite pour \verb+\avec+) 
\\ \verb+\ufplus+ & (unit for \verb+\plus+) & \qquad\qquad 
 & \verb+\upplus+ & (unite pour \verb+\plus+) 
\end{tabular}
\end{center}
[These can be abbreviated using option \opt{uns}---see below.]

%---but the meaning of these macros depends on which option has been
%selected.  

Thus the users of \llc\ are encouraged to type, for example,
\begin{center}
\verb+x \parr \uftens+ ( \dots\ or, \verb+x \parr \e+)
\end{center}
whenever they mean \scary{$x$ par (the unit for tensor)}---irregardless 
of which symbols they happen to be using to denote \scary{par} or
\scary{the unit for tensor}.    

\subsection{The orthodox option: \opt{jyg}}
Linear logic was, of course, invented by J.-Y.\ Girard \cite{Gir:ll}; 
his notation is as follows:
\[\begin{array}{ccccccc}
\verb+x \tens y+ &\mapsto& x \otimes y && \verb+\uftens+ &\mapsto& 1 \\
\verb+x \parr y+ &\mapsto& x \repma y  && \verb+\ufparr+ &\mapsto& \bot \\
\verb+x \with y+ &\mapsto& x \amper y  && \verb+\ufwith+ &\mapsto& \top \\ 
\verb+x \plus y+ &\mapsto& x \oplus y  &\qquad& \verb+\ufplus+ &\mapsto& 0 
  \end{array}\]

\subsection{A common heterodox option: \opt{cns}}

Many category theorists object to Girard's notation for a variety of
reasons.  
Commonly cited objections include that:
\begin{enumerate}
  \item the symbol $\repma$ is ugly and difficult to reproduce
    (both on the blackboard and in \TeX); and, 
  \item category theorists \scary{always} use $\times$ to denote product 
    (\ie, with), and $+$ for coproduct (\ie, plus). 
\end{enumerate}
[Both of these are easily refutable, but that is not the point.]

The notation used by M.\ Barr (who first defined the notion of {\em
$*$-autonomous category} \cite{BarChu}, which is often used to model \mll),
J.R.B.\ Cockett and R.A.G.\ Seely (who are jointly responsible for the
definition of {\em linear distributive} category \cite{CocSee:ldc}, 
which can be used to model \mll-without-negation) is as follows:  
\[\begin{array}{ccccccc}
\verb+x \tens y+ &\mapsto& x \otimes y && \verb+\uftens+ &\mapsto& \top \\
\verb+x \parr y+ &\mapsto& x \oplus y  && \verb+\ufparr+ &\mapsto& \bot \\
\verb+x \with y+ &\mapsto& x \times y  && \verb+\ufwith+ &\mapsto& 1 \\
\verb+x \plus y+ &\mapsto& x + y       &\qquad& \verb+\ufplus+ &\mapsto& 0 
  \end{array}\]

\subsection{A quantale theoretic option: \opt{cjm}} 

Prior to J.-Y. Girard's invention of linear logic,
C.J. Mulvey introduced quantale theory \cite{Mul:&}.  
Quantales only model a fragment of linear logic, 
but it is an interesting fragment---in particular, 
they capture Girard's {\em phase space semantics}, \cite{KRo:phases?}.

Thus it seems only fair for \llc\ to include a 
quantale-theoretic option: 
\[\begin{array}{ccccccc}
\verb+x \tens y+ &\mapsto& x \amper y && \verb+\uftens+ &\mapsto& e \\
\verb+x \parr y+ &\mapsto& x \repma y && \verb+\ufparr+ &\mapsto& d \\
\verb+x \with y+ &\mapsto& x \wedge y && \verb+\ufwith+ &\mapsto& 1 \\
\verb+x \plus y+ &\mapsto& x \vee y &\qquad& \verb+\ufplus+ &\mapsto& 0
  \end{array}\]
%{\bf Note-to-self: justify or change these symbols for units.}

% Note that quantale theorists disagree on how to denote units:
% here I have used the notation of the Czech school (Rosicky, Paseka, Kruml)
% for the nullaries---future versions of \llc\ may incorporate more
% quantale theoretic options, especially if outrage is expressed. 

\subsection{A very strange option indeed: \opt{jme}}

To make matters worse, I entered the scene.
I objected to all but the quantale-theoretic option as a result of the
following inferences: 
\[ \infer{\textrm{(The symbol $\otimes$ should only be used when 
          {\em tensor} and {\em par} coincide)}}{
   \infer{\textrm{(The original meaning of the symbol $\otimes$ is that 
          {\em tensor} and {\em par} coincide)}}{
   \textrm{(The symbol $\otimes$ originiated in linear algebra)} 
   & \textrm{(In $\Vec$, {\em tensor} and {\em par} coincide)}}} \] 
\[ \infer{\textrm{[The symbol $\oplus$ should only be used when 
          {\em with} and {\em plus} coincide]}}{
   \infer{\textrm{[The original meaning of the symbol $\oplus$ is that 
          {\em with} and {\em plus} coincide]}}{
   \textrm{[The symbol $\oplus$ originiated in linear algebra]} 
   & \textrm{[In $\Vec$, {\em with} and {\em plus} coincide]}}} \]

Eventually I hit upon the idea of breaking each of the symbols 
$\otimes$ and $\oplus$ into a conjunctive and a disjunctive part, 
and was thus led to the following system of notation:
\[\begin{array}{ccccccc}
\verb+x \tens y+ &\mapsto& x \ntimes y && \verb+\uftens+ &\mapsto& e \\
\verb+x \parr y+ &\mapsto& x \utimes y && \verb+\ufparr+ &\mapsto& d \\
\verb+x \with y+ &\mapsto& x \nplus y  && \verb+\ufwith+ &\mapsto& t \\
\verb+x \plus y+ &\mapsto& x \uplus y  &\qquad& \verb+\ufplus+ &\mapsto& o 
  \end{array}\]
[Unfortunately, it is more difficult to break apart the traditional symbols 
for the units of $\otimes$ and $\oplus$ ($k$ and 0) in a meaningful
way---my notation for units is justified as follows: 
$d$ stands for \scary{dualising} object;
$o$ stands for \scary{original} (=initial) object;
$t$ stands for \scary{terminal} object; and 
$e$ is simply a generic symbol for neutral elements.]

\subsection{Yet one more option: \opt{yom}}

By way of contrast, my only criticism of the quantale-theoretic notation is 
that the symbols $\wedge,\vee$ are too closely associated with posets to be
used for arbitrary categories. 
In particular, since categorical models of linear logic often happen to be
order-enriched, it seems sensible to reserve $\wedge,\vee$ to denote the
{meet} and {join} of parallel arrows, when they exist.  

Thus, while I consider \opt{cjm}\ fine for the syntax of linear logic, 
I briefly---\ie, prior to developing the notation of option
\opt{jme}---considered the following notation for the categorical semantics of 
linear logic:
\[\begin{array}{ccccccc}
\verb+x \tens y+ &\mapsto& x \amper y && \verb+\uftens+ &\mapsto& e \\
\verb+x \parr y+ &\mapsto& x \repma y && \verb+\ufparr+ &\mapsto& d \\
\verb+x \with y+ &\mapsto& x \sqcap y && \verb+\ufwith+ &\mapsto& t \\
\verb+x \plus y+ &\mapsto& x \sqcup y &\qquad& \verb+\ufplus+ &\mapsto& o 
  \end{array}\]
and therefore include it in \llc\ as an interesting relic.

\subsection{Abbreviated macros for units: \opt{uns}}

My preferred notation for nullaries suggests the following abbreviations:
\begin{eqnarray*}
  \verb+\uftens+ &\mapsfrom& \verb+\e+ \\
  \verb+\ufparr+ &\mapsfrom& \verb+\d+ \\
  \verb+\ufwith+ &\mapsfrom& \verb+\t+ \\
  \verb+\ufplus+ &\mapsfrom& \verb+\o+ 
\end{eqnarray*}
---these can be loaded by including option \opt{uns}\ in addition to one of
the options listed above.  

Note, however, that \verb+\d+, \verb+\o+ and \verb+\t+ already have
meanings in \TeX: by default,
\begin{center}
\begin{tabular}{ccc}
\verb+\d{a}+ & produces & \d{a} \\
\verb+\o+ & produces & \o \\
\verb+\t{a}{a}+ & produces & \t{a}{a}
\end{tabular}
\end{center}
---the option \opt{uns}\ simply overrides these.

A user who needs one of these symbols should either not use this option, 
or include something along the lines of 
\begin{center}
  \verb+\let\udot\d+ \qquad \verb+\let\nordico\o+
\end{center}
at a point prior to %loading \llc.
\verb+\usepackage[...,uns]{llconnex}+.

[Strangely, however, 
%\begin{quote} 
  \verb+\let\tieover\t+
%\end{quote}
does not seem to have the desired effect.]

%Note-to-self: these exist in text only, so it is 

\subsection{Indexed connectives}

It is rare that one needs to deal with infinitary conjunctions and
disjunctions in linear logic---although this can occur, 
for instance in quantale theory. 

Nevertheless, it seemed sensible to include \scary{large} versions of each
of the connectives described above, as these can also be used for finite
indices---\eg, $\bigrepma_{j=1}^n x_j$.  

The macros for these large connectives are \verb+\bigtens+,
\verb+\bigparr+, \verb+\bigwith+ and \verb+\bigplus+;  
in each case they produce a version of the ordinary binary symbol 
with appropriate spacing, except in option \opt{cns} where \verb+\bigwith+ 
compiles to $\prod$, and \verb+\bigplus+ compiles to $\sum$.    
% \[ \bigamper_{j=1}^n x_j \to  \]
% \[ \bigntimes_{j=1}^n x_j \to \bigotimes_{j=1}^n x_j 
%    \to \bigutimes_{j=1}^n x_j \]
% \[ \bignplus_{j=1}^n x_j \to \bigoplus_{j=1}^n x_j 
%     \to \biguplus_{j=1}^n x_j \]
% \[\prod_{j=1}^n x_j \to \sum_{j=1}^n x_j \]
% \[\bigsqcup_{j=1}^n x_j \to \bigsqcap_{j=1}^n x_j \]
% \[\bigvee_{j=1}^n x_j \to \bigwedge_{j=1}^n x_j \]

% \[\bigamper \to \bigrepma \]

\section{Negations and Implications}

In linear logic proper there exists only one notion of linear negation, 
but in non-commutative linear logic, there exist two.  
Wishing to be all things to all people, \llc\ accommodates the possibility
of two linear negations, and therefore also of two linear implications. 
\begin{center}
\begin{tabular}{cccc}
  linear negation (\aka: perp)  
    &$\mapsto$& \verb+\perp+ \\
  reverse linear negation 
    &$\mapsto$& \verb+\prep+ \\
  linear implication (\aka: lollipop) 
    &$\mapsto$& \verb+\loll+ \\
  reverse linear implication  
    &$\mapsto$& \verb+\llol+ 
\end{tabular}
\end{center}

By default, these compile as follows:
\begin{eqnarray*}
\verb+\perp{x}+ &\mapsto& \perp{x} \\
\verb+\prep{y}+ &\mapsto& \prep{y} \\
\verb+x \loll z+ &\mapsto& x \loll z \\
\verb+z \llol y+ &\mapsto& z \llol y 
\end{eqnarray*}
but options can be used to change these.

Note that \verb+\perp+ and \verb+\prep+ take an argument; 
either used alone will produce an error.
When referring to linear negation as a functor,  
it is advisable to pre-define a blank space 
(\eg, \verb+\def\blank{{(-)}}+),
so that one can simply write \verb+\perp\blank+. 

\subsection{Alternatives for negations}

Many category theorists, such as M.\ Barr and myself, 
prefer to denote linear negations with asterisks, 
as is standard in duality theory.
We therefore include an option \opt{ast}, 
which produces the following results:
%which are the standard symbol for duals in duality theory:
  \def\perpsymbol{\mathrel{^{\,\ast}}}
  \def\prepsymbol{\mathrel{^{\ast\,}}}
\begin{eqnarray*}
\verb+\perp{x}+ &\mapsto& \perp{x} \\
\verb+\prep{y}+ &\mapsto& \prep{y} \\
\end{eqnarray*}

Other category theorists, such as A.\ Joyal and R.\ Street,  
apparently object to having superscripts on the left. 
Option \opt{jns} produces their notation, which is as follows:
\begin{eqnarray*}
\verb+\perp{x}+ &\mapsto& x^\ast \\
\verb+\prep{y}+ &\mapsto& y^\vee \\
\end{eqnarray*}

Another convention for avoiding superscripts on the left, 
is provided by option \opt{mus}:
\begin{eqnarray*}
\verb+\perp{a}+ &\mapsto& a^\sharp \\
\verb+\prep{b}+ &\mapsto& b^\flat  \\
\end{eqnarray*}
---anyone who has played the piano will find this natural.

% \subsection{A change of heart? option \opt{cyc}} 

% This option redefines \verb+\perp+ to equal \verb+\prep+. 
%thus erasing the distinction between the two linear negations.

\subsection{Alternatives for implication}
The lollipop symbols for linear implication are nearly universal.
The only exceptions occur in quantale theory papers, 
where \scary{residuations} are commonly denoted with ordinary arrows.

Option \opt{arr} produces  
\begin{eqnarray*}
\verb+x \loll z+ &\mapsto& x \rightarrow z \\
\verb+z \llol y+ &\mapsto& z \leftarrow y \\
\end{eqnarray*}
and option \opt{Arr} produces
\begin{eqnarray*}
\verb+x \loll z+ &\mapsto& x \Rightarrow z \\
\verb+z \llol y+ &\mapsto& z \Leftarrow y \\
\end{eqnarray*}

\section{Exponentials}

Options for exponentials are redundant, 
as all authors seem to agree on how to denote them:
$\bang$ for the negative one (\aka: bang, of course, \fr{bien s\^ur}), and
$\whim$ for the positive one (\aka: whimper, why not, \fr{pourquoi pas}).

The macros for these symbols are 
\begin{center}
\begin{tabular}{ccc}
  bang, of course, \fr{bien s\^ur} %$\bang$ %neg.\ exponential 
    &$\mapsto$& \verb+\bang+, \verb+\duhh+, \verb+\bsur+ \\
  whimper, why not, \fr{pourquoi pas} %$\whim$ %pos.\ exponential 
    &$\mapsto$& \verb+\whim+, \verb+\ynot+, \verb+\ppas+ 
\end{tabular}
\end{center}

% \begin{eqnarray*}
% \verb+\bang[x]+, \verb+\bsur[x]+, \verb+\duhh[x]+ &\mapsto& \duhh[x] \\
% \verb+\whim[x]+, \verb+\ppas[x]+, \verb+\ynot[x]+ &\mapsto& \ynot[x] 
% \end{eqnarray*}
% Unlike negations, exponentials are equipped with an optional argument.
% This means it is possible to use \verb+\bang+ and \verb+\whim+ without
% obtaining an error message; they produce just $\bang$ and $\whim$. 

% This is useful when referring to $\bang$ as a functor; thus, for example, 
% \verb+\bang \rightarrow \bang\bang+, correctly produces $\bang \rightarrow
% \bang\bang$.  
% It is also useful to write simply \verb+\bang\bang[x]+ for $\bang\bang[x]$ 
% rather than \verb+\bang[{\bang[x]}]+.  
% [Note that \verb+\bang[\bang[x]]+ produces an error.]
% What about $\bang x,\bang{x}$.

% If you are going to use double exponentials on a regular basis, 
% you might want to define, say, \verb+\def\bbang{\bang\bang}+.

\section{Other connectives}

Future versions of \llc\ may incorporate macros for the linear
co-implications, and for connectives appearing in extensions of linear
logic, \eg\ the non-commutative \fr{seque} operations.

\section{Symbols new and old}

\subsection{Superimposed math symbols}
Only four symbols defined in \llc\ are entirely new: 
the binary \scary{partial tensor product} symbols, $\ntimes$ and $\utimes$
and their large versions, $\bigntimes$ and $\bigutimes$.  
These can, at any time, be produced using the macros 
\verb+\ntimes+, \verb+\utimes+, \verb+\bigntimes+ and \verb+\bigutimes+,
respectively. 
Understanding how these symbols are created will allow the user to create
many more similar symbols---$\mathsuperimpose\fixtimes\sqcap$,
$\mathsuperimpose\circ\fixcup$, \etc---should the need arise.  

Firstly, \llc\ defines a symbol \verb+\fixtimes+, 
which is simply a smaller version of $\times$ 
and a symbol \verb+\fixcup+ which is a slightly lower version of $\cup$.  
Next, \llc\ creates a means of superimposing two math symbols,
\verb+\mathsuperimpose+.
Finally, \llc\ defines \verb+\ntimes+ and \verb+\utimes+ by
\verb+\mathsuperimpose+-ing a \verb+\fixtimes+ on a \verb+\cap+ 
and a \verb+\fixcup+, respectively; \verb+\bigntimes+ and \verb+\bigutimes+
are defined by \verb+\mathsuperimpose+-ing an ordinary \verb+\times+ on a
\verb+\bigcap+ and a \verb+\bigcup+, respectively.

Thus $\mathsuperimpose\fixtimes\sqcap$ can be obtained by 
%\begin{center}
\verb+\mathsuperimpose\fixtimes\sqcap+ 
%\end{center}
and $\mathsuperimpose\circ\fixcup$ by 
\newline
%\begin{center}
\verb+\mathsuperimpose\circ\fixcup+.  
%\end{center}
Note that the wider of the two symbols (if they are not equal in width)
should be placed as the second argument of \verb+\mathsuperimpose+. 

%Feel free to use \verb+\mathsuperimpose+ for any other purpose you can
%think of.

\subsection{Ampersand and ampersor}
The symbols $\amper,\repma$ are part of the {\tt stmaryrd} package, 
which is required for \llc.  

There they go under the names \verb+\binampersand+ and \verb+\bindnasrepma+,
respectively, but \llc\ defines \verb+\amper+ and \verb+\repma+, to mean 
better-spaced versions of the same.
\begin{verbatim}
   \def\amper{\mathrel{\binampersand}}
   \def\repma{\mathrel{\bindnasrepma}}
\end{verbatim}
It also defines \verb+\bigamper+ and \verb+\bigrepma+ for indexed
conjunctions and disjunctions. 
\begin{verbatim}
   \def\bigamper{\mathop{\binampersand}\limits} 
   \def\bigrepma{\mathop{\bindnasrepma}\limits}
\end{verbatim}

\subsection{Others}
The symbol $\nplus$ also exists in {\tt stmaryrd.sty}, 
where it goes under the name \verb+\nplus+; 
and $\uplus$ is, of course, standard under the name \verb+\uplus+.

The definitions of \verb+\loll+ and \verb+\llol+ 
were stolen from R.A.G.\ Seely's list of macros, \verb+ragsmac.tex+;
\llc\ also defines a number of similar symbols:
\begin{center}
\begin{tabular}{ccccccc}
\verb+\sqloll+ &$\mapsto$& $\sqloll$ && 
\verb+\sqllol+ &$\mapsto$& $\sqllol$ \\
\verb+\varloll+ &$\mapsto$& $\varloll$ && 
\verb+\varllol+ &$\mapsto$& $\varllol$ \\
\verb+\doubloll+ &$\mapsto$& $\doubloll$ &\qquad& 
\verb+\doubllol+ &$\mapsto$& $\doubllol$. 
\end{tabular}
\end{center}

%They also inspired the definitions of \verb+\perp+ and \verb+\prep+.

% \subsubsection{Negations}

% All three notations for \verb+\perp+ and \verb+\prep+ are available, 
% at any time, under the following names:
% \begin{eqnarray*}
%   \verb+\orthperp{x}+ &\mapsto& \orthperp{x} \\
%   \verb+\orthprep{y}+ &\mapsto& \orthprep{y} \\
%   \verb+\opt{ast}perp{x}+ &\mapsto& \opt{ast}perp{x} \\
%   \verb+\opt{ast}prep{y}+ &\mapsto& \opt{ast}prep{y} \\
%   \verb+\opt{mus}eperp{x}+ &\mapsto& \opt{mus}eperp{x} \\
%   \verb+\opt{mus}eprep{y}+ &\mapsto& \opt{mus}eprep{y} 
% \end{eqnarray*}
% \begin{verbatim}
%    \def\orthperp#1{#1^{\bot}}
%    \def\orthprep#1{\!\!~^{\bot}\mkern-2mu{#1}} 
%    \def\opt{ast}perp#1{#1^*} 
%    \def\opt{ast}prep#1{\!\!~^*\mkern-2mu{#1}} 
%    \def\opt{mus}eperp#1{#1^\sharp}
%    \def\opt{mus}eprep#1{#1^\flat}
% \end{verbatim}

\section{Bugs, tips, \etc.}

The definition of \verb+\fixtimes+ uses hard measures which are 
optimised for 12pt fonts; these can, however, be redefined.
For example, if using 11pt font, I recommend \verb+\def\quasipt{0.75pt}+
and, if using 10pt font, \verb+\def\quasipt{0.67pt}+ to produce better
results for $\ntimes$ and $\utimes$.  
These commands should appear {immediately after}, not before, 
\verb+\usepackage[...]{llconnex}+. 

Moreover, the scriptscript-size version of \verb+\fixtimes+ is simply a
dot, which is less than ideal.
Thus, for example, \verb+{\scriptscriptstyle x \ntimes y}+ produces only 
$\scriptscriptstyle x \ntimes y$. 
Hopefully, this should not cause many problems.
A useful tip, when using Xy-pic, is to include the command 
\verb+\let\labelstyle\textstyle+ to increase the size of arrow names.  

If you appreciate \llc, then keep an eye out for {\tt mnats.sty} which  
will attempt to do for those natural transformations 
which commonly arise in monoidal category theory 
what \llc\ does for functors.   

\begin{thebibliography}{9}

\bibitem{BarChu}
Michael Barr.
\newblock {\em {$\ast$}-autonomous categories}, volume 752 of {\em Lecture
  Notes in Mathematics}.
\newblock Springer, Berlin, 1979.
\newblock With an appendix by Po Hsiang Chu.

\bibitem{CocSee:ldc}
J.~R.~B. Cockett and R.~A.~G. Seely.
\newblock Weakly distributive categories.
\newblock {\em J. Pure Appl. Algebra}, 114(2):133--173, 1997.

\bibitem{Gir:ll}
Jean-Yves Girard.
\newblock Linear logic.
\newblock {\em Theoret. Comput. Sci.}, 50(1):101, 1987.

\bibitem{Mul:&}
Christopher~J. Mulvey.
\newblock \&.
\newblock {\em Rend. Circ. Mat. Palermo (2) Suppl.}, (12):99--104, 1986.
\newblock Second topology conference (Taormina, 1984).

\bibitem{KRo:phases?}
Kimmo~I. Rosenthal.
\newblock {\em Quantales and their applications}, volume 234 of {\em Pitman
  Research Notes in Mathematics Series}.
\newblock Longman Scientific \& Technical, Harlow, 1990.

\end{thebibliography}


\end{document}
Using 

Thus \usepackage[opt]{llconnex} produces 
    the of Jean-Yves Girard if opt=jyg;
    the ``heterodox'' symbols of Cockett-'n'-Seely if opt=cns;
    my own newly-created and highly unusual symbols if opt=jme; 
    a set of symbols inspired by quantale theory if opt=cjm.

My personal version of llconnex.sty also defines macros for the
other connectives of (non-commutative) linear logic, such as 
but I have temporarily excised them from the public version.

KNOWN BUGS: I have not yet created scriptscriptsize versions of
\ntimes and \utimes.  If you are using Xy-pic and arrow-names which
have subscripts or superscripts containing connective symbols, you
may wish to consider inserting \let\labelstyle\displaystyle. 

\end{document}
