%
%
% JOURNAL = 
%
%
% A FAIRE = 
%
%
%
\documentclass[12pt]{article}
%\usepackage{latex8}
%\usepackage{newcent}
%\usepackage{palatcm}
%\usepackage{palatino}
%\usepackage[mathscr]{euscript}
\usepackage{bussproofs}
%\usepackage{mathabx}
\usepackage{lmodern}
\usepackage{cmll}
\usepackage{bbm}
\usepackage{newcent}
\usepackage{pxfonts}
%\usepackage{times}
\usepackage{graphicx}
\usepackage{mathrsfs}
\usepackage[all]{xy}
\usepackage{infer}

\usepackage[latin1]{inputenc}
\usepackage{stmaryrd}
%\usepackage{amssymb,wasysym,stmaryrd,marvosym}
\usepackage{latexsym}

\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}



%\newenvironment{proof}{{\vspace{1em}\noindent \textit{Proof.}\/}~}{$\Box$}
\newenvironment{proof}{{\vspace{1em}\noindent \textit{Proof.}\/}~}{}
\newtheorem{definition}{Definition}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}[proposition]{Corollary}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}


%\addtolength{\textheight}{1.4em}
\addtolength{\textwidth}{4em}
\addtolength{\hoffset}{-2em}
\addtolength{\textheight}{3.8em}
\addtolength{\voffset}{-1.9em}
%\setlength{\textwidth}{32em}
%\addtolength{\textwidth}{3em}

%\addtolength{\textheight}{5.5em}

%\addtolength{\parskip}{.6em}


\newcommand{\blackhole}[1]{}



%INTRODUCTION
\newcommand{\complementary}[1]{{\sim{#1}}}
\newcommand{\cartesianor}{\vee}
\newcommand{\cartesianand}{\wedge}
\newcommand{\cartesiantrue}{\mathbf{true}}
\newcommand{\cartesianfalse}{\mathbf{false}}

%SECTION 2
\newcommand{\functor}[1]{#1_{\bullet}}
\newcommand{\functorco}[1]{#1_{\circ}}
\newcommand{\functorcell}[1]{{\widetilde{#1}}}
%\newcommand{\functorcellbracket}[1]{{\dot{#1}}}
\newcommand{\functorcellbracket}[1]{{\overline{#1}}}
\newcommand{\functorcellbracketspecial}[1]{{\overline{#1}}}
\newcommand{\naturaltransformation}[1]{#1_{\bullet}}
\newcommand{\naturaltransformationco}[1]{#1_{\circ}}
%\newcommand{\naturaltransformation}[1]{{#1}_{\bullet}}
%\newcommand{\naturaltransformationco}[1]{{#1}_{\circ}}

\newcommand{\ReftoCat}{\mathcal{F}}
\newcommand{\CattoRef}{\mathcal{G}}
\newcommand{\Ftwofunctor}{\mathcal{F}}
\newcommand{\Gtwofunctor}{\mathcal{G}}

%SECTION 3
\newcommand{\dialoguefunctorcell}[1]{{\bot_{#1}}}

\newcommand{\bigquestion}[1]{\texttt{[#1]}}
\newcommand{\rightcomplementary}[1]{{#1^{\ast}}}
\newcommand{\leftcomplementary}[1]{{^{\ast}#1}}
\newcommand{\companionrightcomplementary}[1]{{#1^{\circledast}}}
\newcommand{\companionleftcomplementary}[1]{{^{\circledast}#1}}
\newcommand{\companioncurrify}[3]{\overline{\chi}_{#1,#2,#3}}
\newcommand{\companioncurrifyone}[1]{\overline{\chi}_{#1}}
%\newcommand{\unittensor}{I}
%\newcommand{\unittimes}{1}
\newcommand{\tensor}{\otimes}
%\newcommand{\tensorb}{\otimes}
\newcommand{\alphau}{\alpha}
\newcommand{\alphab}{\alpha}
\newcommand{\lambdau}{\lambda}
\newcommand{\lambdab}{\lambda}
\newcommand{\rhou}{\rho}
\newcommand{\rhob}{\rho}

\newcommand{\unit}{I}
\newcommand{\unitb}{I}
\newcommand{\ID}[1]{\mathrm{id}_{#1}}
\newcommand{\morph}[1]{\stackrel{#1}{\longrightarrow}}

\newcommand{\largebicategoricalop}{\mbox{\emph{\textbf{op}}}}
\newcommand{\bicategoricalop}{\ \!\!\mbox{\footnotesize{\emph{\textbf{op}}}}}
\newcommand{\monoidalco}{\ \!\!\mbox{\scriptsize{$\bullet$}}}
%\newcommand{\monoidalco}{\ \!\!\mbox{\scriptsize{$0$-op}}}

\newcommand{\category}{\mathscr{C}}
\newcommand{\Acategory}{\mathscr{A}}
\newcommand{\Bcategory}{\mathscr{B}}
\newcommand{\Ccategory}{\mathscr{C}}
\newcommand{\Dcategory}{\mathscr{D}}
\newcommand{\Jcategory}{\mathscr{J}}
\newcommand{\Mcategory}{\mathscr{M}}
\newcommand{\Ncategory}{\mathscr{N}}
\newcommand{\Wcategory}{\mathscr{W}}
\newcommand{\Xcategory}{\mathscr{X}}
\newcommand{\bicategory}{\mathbb{B}}
\newcommand{\distributor}[2]{\langle \, #1 \, | \, #2 \, \rangle}
\newcommand{\dialoguedistributor}[2]{\Acategory(\, #1 \, , \, R(#2) \, )}
\newcommand{\companiondistributor}[2]{\langle\!\langle \, #1 \, | \, #2 \, \rangle\!\rangle}
\newcommand{\objects}{\mathscr{O}}
\newcommand{\Vcategory}{\mathscr{V}}
\newcommand{\Wbicategory}{\mathscr{W}}
\newcommand{\Bbicategory}{\mathscr{B}}
\newcommand{\dague}[1]{{#1}^{\dagger}}
\newcommand{\Set}{\mbox{\emph{\textbf{Set}}}}
\newcommand{\Cat}{\mbox{\textit{\textbf{Cat}}}}
\newcommand{\Kat}{\mbox{\textit{\textbf{Kat}}}}
\newcommand{\MonCat}{\mbox{\textit{\textbf{MonCat}}}}

\newcommand{\Cata}{A}
\newcommand{\Catb}{B}
\newcommand{\MonCata}{M}
\newcommand{\Unit}{\eta}
%\newcommand{\Unit}{\eta}
\newcommand{\Counit}{\varepsilon}
\newcommand{\Unitprime}{[\eta]}
\newcommand{\Counitprime}{[\epsilon]}

\newcommand{\Ffunctor}[1]{\mathcal{F}\, #1}
\newcommand{\Ffunctorandseul}{\mathcal{F}_{\tensorialand}}
\newcommand{\Ffunctororseul}{\mathcal{F}_{\tensorialor}}
\newcommand{\Ffunctorand}[1]{\mathcal{F}_{\tensorialand}\, #1}
\newcommand{\Ffunctoror}[1]{\mathcal{F}_{\tensorialor}\, #1}
\newcommand{\Gfunctor}[1]{\mathcal{G}\, #1}
\newcommand{\Gfunctorandseul}{\mathcal{G}_{\tensorialand}}
\newcommand{\Gfunctororseul}{\mathcal{G}_{\tensorialor}}
\newcommand{\Gfunctorand}[1]{\mathcal{G}_{\tensorialand}\, #1}
\newcommand{\Gfunctoror}[1]{\mathcal{G}_{\tensorialor}\, #1}


\newcommand{\pole}[1]{\mathsf{pole}(#1)}
\newcommand{\parametricduality}[1]{\mathsf{duality}(#1)}

%\newcommand{\LogiRefl}{\mbox{\textit{\textbf{LogRef}}}}
%\newcommand{\DialoguePairs}{\mathbf{SpRefl}}
\newcommand{\DialoguePairs}{\mbox{\textit{\textbf{DiaMir}}}}
%\newcommand{\LogiRefl}{\mathbf{MR}}
\newcommand{\Dial}{\mbox{\textit{\textbf{DiaCat}}}}
%\newcommand{\Dial}{\mathbf{DIAL}}
%\newcommand{\DialoguePairs}{\mathbf{SpMR}}
\newcommand{\BCP}{\mathbf{BrMR}}
\newcommand{\BDC}{\mathbf{BrDIAL}}
\newcommand{\BSD}{\mathbf{BrSpMR}}
%\newcommand{\Cat}{\mbox{\textit{\textbf{Cat}}}}
\newcommand{\Reflector}{\mbox{\textit{\textbf{Ref}}}}
\newcommand{\MirrorPairs}{\mbox{\textit{\textbf{Mir}}}}
\newcommand{\RefCat}{\mbox{\textit{\textbf{Ref\,Cat}}}}
\newcommand{\MonMirrorPairs}{\mbox{\textit{\textbf{MonMir}}}}

\newcommand{\Companion}[1]{\mathcal{H}(#1)}
\newcommand{\CompanionAlone}{\mathcal{H}}

%\newcommand{\Bot}{\bot\,\bot}
\newcommand{\ReflectionPresheaf}[2]{\Bot_{#1}(#2)}
\newcommand{\ReflectionPresheafAlone}{\Bot}
\newcommand{\ReflectionPresheafOne}[1]{\Bot_{#1}}
\newcommand{\ReflectionPresheafSimple}[1]{\Bot({#1})}
\newcommand{\ReflectionPresheafFunctor}[1]{\Bot_{#1}}
\newcommand{\CAT}{\mathbb{C}}
\newcommand{\DAT}{\mathbb{D}}
\newcommand{\leftpop}{\multimap\!}
\newcommand{\rightpop}{\!\multimapinv}

\newcommand{\pivotalnegation}[1]{\lnot\, #1}
\newcommand{\pivot}[1]{\mathbf{\mathbf{pivot}}_{\, #1}}

\newcommand{\lefteval}[1]{\mathbf{\mathit{lev}}_{\, #1}}
\newcommand{\righteval}[1]{{\mathit{\mathit{rev}}}_{\, #1}}
\newcommand{\leftcoeval}[1]{{\mathit{colev}}_{\, #1}}
\newcommand{\rightcoeval}[1]{{\mathit{corev}}_{\, #1}}
\newcommand{\leftname}[1]{\ulcorner #1 \urcorner}

\newcommand{\rightstrength}{\mathit{strength}}

\newcommand{\tensorialand}{\varowedge}
\newcommand{\tensorialor}{\varovee}
\newcommand{\tensora}{\tensorialand}
\newcommand{\tensorb}{\tensorialor}
\newcommand{\tensorialtrue}{\mathbf{\mathit{true}}}
\newcommand{\tensorialfalse}{\mathbf{\mathit{false}}}
\newcommand{\tensorialunit}{e}
%\newcommand{\distau}{\kappa^{-}}
%\newcommand{\contau}{\kappa^{+}}
\newcommand{\distau}{\kappa^{\tensorb}}
\newcommand{\contau}{\kappa^{\tensora}}
\newcommand{\leftdistau}{\mathbf{left.}\kappa^{\tensorb}}
\newcommand{\leftcontau}{\mathbf{left.}\kappa^{\tensora}}
\newcommand{\rightdistau}{\mathbf{right.}\kappa^{\tensorb}}
\newcommand{\rightcontau}{\mathbf{right.}\kappa^{\tensora}}
%\newcommand{\leftadjoint}{\downarrow}
%\newcommand{\rightadjoint}{\uparrow}
\newcommand{\leftadjoint}{L}
\newcommand{\rightadjoint}{R}

\newcommand{\llpar}{\parr}

\newcommand{\ReflectionCycle}[2]{\mathit{wheel}_{\, #1,#2}}
\newcommand{\ReflectionCycleAlone}{\mathit{wheel}}
\newcommand{\ReflectionPairCycle}[2]{\mathit{wheel}_{\, #1,#2}}
\newcommand{\ReflectionPairCycleAlone}{\mathit{wheel}}

\newcommand{\DialogueCycle}[1]{\mathit{turn}_{\, #1}}
\newcommand{\DialogueCycleAlone}{\mathit{turn}}
\newcommand{\DialogueTwist}{\mathit{twist}}

\newcommand{\cycle}[2]{\mathbf{cycle}_{#1,#2}}
\newcommand{\cyclealone}{\mathbf{cycle}}
\newcommand{\turn}[2]{\sigma_{#1,#2}}
\newcommand{\turnalone}{\sigma}
%\newcommand{\cyclic}[2]{\mathbf{cycle}_{#1,#2}}
\newcommand{\cyclic}[2]{\mathbf{wheel}_{\, #1,#2}}

\newcommand{\leftcurrify}[3]{\chi^{L}_{#1,#2,#3}}
\newcommand{\leftcurrifyone}[1]{\chi^{L}_{#1}}
\newcommand{\leftcurrifyalone}{\chi^{L}}
\newcommand{\rightcurrify}[3]{\chi^{R}_{#1,#2,#3}}
\newcommand{\rightcurrifyone}[1]{\chi^{R}_{#1}}
\newcommand{\rightcurrifyalone}{\chi^{R}}
\newcommand{\currify}[3]{\chi_{#1,#2,#3}}
\newcommand{\currifyone}[1]{\chi_{#1}}
\newcommand{\currifyalone}{\chi}
\newcommand{\AX}[1]{\mathbf{AX}{[{#1}]}}
\newcommand{\CUT}[1]{\mathbf{CUT}{[#1]}}
\newcommand{\LEFTAX}[1]{\mathbf{left.AX}{[{#1}]}}
\newcommand{\LEFTCUT}[1]{\mathbf{left.CUT}{[{#1}]}}
\newcommand{\RIGHTAX}[1]{\mathbf{right.AX}{[{#1}]}}
\newcommand{\RIGHTCUT}[1]{\mathbf{right.CUT}[{#1}]}
\newcommand{\leftaxiom}[1]{\mathbf{left.axiom}[{#1}]}
\newcommand{\leftcut}[1]{\mathbf{left.cut}[{#1}]}
\newcommand{\rightaxiom}[1]{\mathbf{right.axiom}[{#1}]}
\newcommand{\rightcut}[1]{\mathbf{right.cut}[{#1}]}

\newcommand{\braidgroup}[1]{\mathbf{B}_{#1}}
%\newcommand{\adjunction}[6]{{#1},{#2}:{#3}\dashv{#4}:{#5}\rightarrow {#6}}
\newcommand{\shortadjunction}[4]{{#1}\dashv{#2}:{#3}\rightarrow {#4}}
\newcommand{\veryshortadjunction}[6]{{#3}\dashv{#4}}
\newcommand{\adjunction}[4]{{#3}:\vcenter{\xymatrix @-.1pc {{#1}\ar@/^.7pc/[rr]\ar@{}[rr]|-{\bot}&&{#2}\ar@/^.7pc/[ll]}}:{#4}}
\newcommand{\braiding}[2]{\gamma_{#1,#2}}

\newcommand{\parametricunit}[1]{\eta{[#1]}}
\newcommand{\parametriccounit}[1]{\varepsilon{[#1]}}
\newcommand{\axiom}[1]{\mathbf{axiom}{[#1]}}
\newcommand{\cut}[1]{\mathbf{cut}{[#1]}}

\newcommand{\RefutationCycle}[2]{\mathit{wheel}_{\, #1,#2}}
\newcommand{\RefutationCycleAlone}{\mathit{wheel}}

\newcommand{\Endofunctors}[1]{\mathrm{End}(#1)}
%\newcommand{\Unit}{\eta}
\newcommand{\IDCAT}[1]{1_{#1}}
\newcommand{\IDCATa}{1_A}
\newcommand{\IDCATb}{1_B}
\newcommand{\leftadjointprime}{[L,R]}
\newcommand{\rightadjointprime}{[R,L]}
\newcommand{\id}[1]{\mathrm{id}_{#1}}
\newcommand{\ONECAT}{\mathbbm{1}}
\newcommand{\INDEX}{J}
\newcommand{\oneINDEX}{e}

\newcommand{\verticalproof}[1]{\begin{array}{c}#1\vspace{-.5em}\\ \vdots\end{array}}
\newcommand{\HelCat}{\mbox{\textit{\textbf{HelCat}}}}
\newcommand{\HelChir}{\mbox{\textit{\textbf{HelChir}}}}

\newcommand{\helix}{\sigma}

\newcommand{\freeribbon}[1]{\mathbf{free\mbox{-}ribbon}(#1)}
\newcommand{\freedialogue}[1]{\mathbf{free\mbox{-}dialogue}(#1)}

%MISE EN PAGE
\hyphenation{co-monoidal co-monoid co-monoids mo-noidal La-marche Lorent-zen Har-mer Klee-ne catego-rical cate-gorical}


%pole axis calotte rivet enjeu mise (stake) tropisme racine (root) attache cheville
%pin ancre (anchor) horizon articulation lentille (lense) modulation accent
%fanal climax tonality une marque (mark) caprice chimere monomania totem
%
%paire mimetique, paire mirroir, reflecteur, mimoid, catadioptrie, fantasmagory
%
%
%
%articulation totem tonality
%
%une farce taquin foyer (pole)
%
%the axis of negation


%transjunctions


\begin{document}

\title{
A micrological study of negation
%Linearly distributive chiralities
%A combinatorial presentation\\
%\hspace{.8em}
%of dialogue categories\\
%$[$ Part I $]$
%\vspace{.5em}
%------ part one ------
%------ act i ------
%\vspace{.5em}
%--- I ---
%Tensorial logic 1\\
%An algebraic presentation\\
%of dialogue categories\\
%\vspace{.3em}
%--------- Act I ---------}
%\\
%formulated as chiral pairs}
% and dialogue games}
}
\author{Paul-Andr\'e Melli\`es\thanks{
CNRS, Laboratoire PPS, UMR 7126,
Universit\'e Paris Diderot, Sorbonne Paris Cit\'e,
F-75205 Paris, France.
This work has been partly supported by the ANR Project RECRE.}}

\date{}

\maketitle

%
%\begin{flushright}
%\begin{tabular}{r}
%<< Et si j'affirme, j'interroge encore >>
%\\
%Jacques Rigaut
%\end{tabular}
%\end{flushright}


\begin{abstract}
%
The purpose of this paper is to develop a combinatorial presentation of tensorial negation in dialogue categories.
%
The formulation is based on the disclosure of a fundamental symmetry of tensorial logic
between proofs and anti-proofs.
%
The micrological analysis reveals that tensorial negation
may be either seen as primitive, or decomposed into a series
of more elementary components.
% in the spirit of proof-theory.
%, including a pair of distributivity laws in chirality.
%
%
%The purpose of this paper is to illustrate with an example
%the recent emergence in logic of a fundamental symmetry
%between proofs and anti-proofs.
%
%Starting from this new picture of logic,
%we develop a purely combinatorial and symmetric
%presentation of dialogue categories.
%
%The micrological analysis also reveals that tensorial negation is not atomic,
%is a molecule of operations,
%rather than a primary element,
%of more elementary operations,
%and may be thus decomposed into a series of more primitive elements.
%The technical purpose of this paper is to develop
%based on a properly symmetric understanding of logic.
% emergence of a new picture of logic,
%on a fundamental symmetry between Prover and Refutator.
%
%The resulting micrological analysis may be understood
%as performing a chemical decomposition of the molecule
%of negation into its primary elements.
\end{abstract}


\section{Introduction}
%
One primary purpose of our work in tensorial logic is to transfer 
the ideas and constructions of linear logic
% and his school
to this more primitive logic of tensor
and negation, where negation~$A\mapsto \lnot \, A$ is not required to be involutive anymore.
%anymore.
%
An amusing but also disturbing
%An amusing but also disturbing
%quite extraordinary 
%amusing but at the same time disturbing 
aspect of this research program
is that it looks perfectly meaningless on the surface, at least
when one considers it with the prevailing spectacles of linear logic.
%
%Seen from this well-established but secretly distorted angle, 
Seen from this too familiar angle, the project immediately bumps
against the objection that tensorial logic is an ``intuitionistic'' system,
and thus lacks the ``classical'' symmetries of linear logic
exhibited by Jean-Yves Girard~\cite{girard:ll,girard:synsem}.
%in the second part of the 1980s.
%
%As a matter of fact, 
The misunderstanding is so deeply rooted in the traditions
and habits of the field that it cannot be overtaken
% ideological
%This compels us to start the whole project
% \emph{before anything else}
%{on the first hand} 
without recasting the foundations of linear logic 
in a radically different way.
% in order to be understood.
%

\medbreak 

%
The task is accomplished here by transporting the ``classical'' symmetries
of linear logic to an ``intuitionistic'' system like tensorial logic.
%
%The discovery of these ``intuitionistic'' symmetries
This act of relocation is 
%is also an act of subversion,
%is also an act of rebellion,
designed to annihilate the customary view
that these ``classical'' symmetries of linear logic
should originate from its ``classical'' negation.
%and of its negation.
%--- since these symmetries appear \emph{in exactly the same way} in tensorial logic.
%
%This is not the case, and 
The destruction of this ancient and well-established dogma
% of linear logic
leads to a more harmonious picture of logic.
%
In particular, the symmetries of classical logic appear to originate 
from a more fundamental \emph{invariance property} of logic
% of logic %of various logical systems of interest 
with respect to an \emph{internal symmetry} of a very primitive nature
---
since its primary effect is to interchange the two sides \emph{Prover} 
and \emph{Denier} of the logical dispute.
%
This invariance property with respect to the symmetry Prover\,/\,Denier
is precisely what underlies the \emph{chirality principle} between proofs
and anti-proofs noticed for tensorial logic in~\cite{mellies:tensorial-logic-1}.
%
%The internal symmetry is reflected algebraically by the operation of transforming
%a category~$\Ccategory$ into its oppositive category~$\Ccategory^{\, op}$.
%
An important methodological point is that the chirality principle
is not limited to tensorial logic, and that it regulates in exactly
the same way ``classical'' and ``intuitionistic'' systems.
%
%The internal symmetry of logic is of a more primitive nature, whose effect is to interchange
%the two sides \emph{Prover} and \emph{Denier} of the logical dispute.
%
%Besides the obvious influence of game semantics, 

%%%%
%The discovery of this internal symmetry of logic $\Ccategory\mapsto\Ccategory^{\, op}$
%owes a lot to the notion of \emph{polarities} introduced by Girard in his beautiful work
%on classical logic~\cite{girard:lc}.
%
%It elucidates their algebraic nature and consecrates them as a universal principle of logic.
%%%%

%
%We believe that it consecrates the notion of polarity as a universal principle of logic.
%
%We will see that this idea of internal symmetry clarifies the algebraic nature of these polarities
%and in doing so, consecrates them as a universal principle of logic.

\medbreak

Once the new picture of logic has been spelled out,
the rigid separation between classical logic and intuitionistic logic
%inherited from the past
appears suddenly obsolete -- and our research program
becomes meaningful again...
%
%More specifically, seen from this revised perspective,
%In particular, tensorial logic benefits of the symmetries of classical logic,
%just like any other reasonable logical system.
% like intuitionistic logic.
% or linear logic.
%tensorial logic appears just as symmetric
%as linear logic.
%
%
%As a matter of fact, our careful and somewhat obsessive analysis of tensorial logic
%will reveal that these ``classical'' symmetries are a basic and foundational principle
%of logic as a whole, which applies in essentially the same way to all logical systems,
%either classical or intuitionistic.
%
%Another quite different picture will emerge.
%
%This will be quite the contrary in fact: our work is driven by the discovery that these symmetries
%are universal principles of logic, which 
%

\medbreak

%An important methodological point is that t
%From a purely methodological point of view,
%it is worth mentioning that this revised picture of logic emerged
%gradually and naturally 
%One methodological point deserves to be mentioned here.
%
%As we will see, t
%As we already mentioned, 
%From a purely historical point of view, 
This alternative understanding of logic 
%In order to understand this symmetric account of logic as a whole,
%An important methodological point is that this revised picture of logic
emerged from our desire to transfer the ``classical'' symmetries
of linear logic to an ``intuitionistic'' system like tensorial logic.
%--- and not the other way round.
%
%It became at some point the appropriate mental landscape
%in order to articulate the symmetries of game semantics.
%
%In order to understand how, 
Our starting point
%in this investigation 
was provided by the notion of $\ast$-autonomous category
--- the categorical counterpart of linear logic ---
%An appropriate starting point for this investigation of symmetries in logic is provided by 
%ypical illustration of ``classical'' symmetry in linear logic is provided by 
traditionally defined as a monoidal biclosed category~$\Ccategory$
equipped with a dualizing object~$\bot$, see~\cite{barr:non-symmetric-star-autonomous}
for details.
%
Recall that an object~$\bot$ of a biclosed monoidal category~$\Ccategory$
is called \emph{dualizing} when the two canonical morphisms
$$
x \hspace{.2em} \morph{} \hspace{.4em} (\bot\rightpop x)\leftpop\bot
\quad\quad\quad\quad\quad
x \hspace{.2em} \morph{} \hspace{.4em} \bot\rightpop (x\leftpop\bot)
$$
transporting~$x$ into its double negation are isomorphisms,
for every object~$x$ of the dialogue category.
%
The terminology of ``dualizing object'' comes from the fact that the two negation functors
$$
\begin{array}{ccccccc}
{^{\bot}(-)}
& \quad : \quad & x & \quad \mapsto \quad & \bot\rightpop x & \quad : \quad & \Ccategory \quad \morph{} \quad \Ccategory^{\, op}
\\
{(-)^{\bot}} & \quad : \quad & x & \quad \mapsto \quad & x\leftpop\bot & \quad : \quad & \Ccategory^{\, op} \quad \morph{} \quad \Ccategory
\end{array}
$$
%associated to such a dualizing object~$\bot$ 
define in that case an equivalence
\begin{equation}\label{equation/star-autonomous-categories-equivalence}
\xymatrix @-1.8pc {
\Ccategory
&\ar@/^1.2pc/[rrrrrrrr]^-{^{\bot}(-)}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{(-)^{\bot}}
&
\Ccategory^{\, op}}
\end{equation}
between the category~$\Ccategory$ and its opposite category~$\Ccategory^{\, op}$.
%
This establishes that every $\ast$-autonomous category~$\Ccategory$ is self-dual,
in the technical sense that it is equivalent to its opposite category.
%

\medbreak

%
Although this definition of $\ast$-autonomous category is prevailing,
% one should probably complain about the fact that 
it is not sufficiently ``symmetric'' in the sense that it starts from
the conjunction \hspace{.1em}$\tensor$\hspace{.1em} and from the implications 
\hspace{.1em}${\leftpop}$\hspace{.3em} and \hspace{.3em}${\rightpop}$\hspace{.1em}
provided by the biclosed monoidal category, rather than from the conjunction
\hspace{.1em}$\tensor$\hspace{.1em}
and from the disjunction \hspace{.1em}$\llpar$\hspace{.1em} provided by linear logic.
%
From a purely esthaetic point of view, this non-symmetric presentation
of a perfectly self-dual logic like linear logic looks awkward, and
one thus wonders whether the formulation may be replaced by a more symmetric one.
%
A preliminary difficulty is that there are two different canonical ways to define the disjunction
in a biclosed monoidal category:
$$
\begin{array}{ccccc}
x\llpar_{1} y & \quad := \quad & ((\bot\rightpop y)\tensor(\bot\rightpop x))\leftpop\bot 
& \quad := \quad & ({^{\bot}{y}}\tensor{^{\bot}{x}})^{\bot}
\\
x\llpar_{2} y 
& \quad := \quad & 
\bot\rightpop((y\leftpop\bot)\tensor(x\leftpop\bot)) 
& \quad := \quad & 
{^{\bot}({y^{\bot}}\tensor{x^{\bot}})}
\end{array}
$$
However, the series of monoidal equivalences 
$$
\xymatrix @-1.8pc {
(\Ccategory,\llpar_1,\bot)
&\ar@/^1.2pc/[rrrrrrrr]^{^{\bot}(-)}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{(-)^{\bot}}
&
(\Ccategory,\tensor,\mathbf{1})^{\,op(0,1)}
&\ar@/^1.2pc/[rrrrrrrr]^-{^{\bot}(-)}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{(-)^{\bot}}
&
(\Ccategory,\llpar_2,\bot)}
$$
establishes that the two monoidal structures~$\llpar_1$ and~$\llpar_2$
on the category~$\Ccategory$ are related by the monoidal equivalence~$x\mapsto x^{\bot\bot}$
in the sense that there exists two families of isomorphisms
$$
(x\llpar_2 y)^{\bot\bot} \cong x^{\bot\bot} \llpar_1 y^{\bot\bot}
\quad\quad\quad
\bot^{\bot\bot} \cong \bot
$$
natural in~$x$ and~$y$ and compatible 
in the expected sense
with the two disjunctions~$\llpar_1$
and~$\llpar_2$ and with their common unit~$\bot$.
%
For that reason, it often makes sense to restrict oneself to the case of a pivotal
or of a symmetric $\ast$-autonomous category, where the monoidal 
equivalence~$x\mapsto x^{\bot\bot}$ is isomorphic to the identity.
%
In that case, the left and the right implication functors necessarily coincide modulo isomorphism,
and the disjunction~$\llpar$ may be thus defined in a non equivocal way as
$$
x\llpar y \quad := \quad ((y\leftpop\bot)\tensor(x\leftpop\bot))\leftpop\bot.
$$
This leads to the question of presenting such a $\ast$-autonomous category
starting from the symmetric pair of connectives~$\tensor$ and~$\llpar$ instead
of the asymmetric pair~$\tensor$ and~$\leftpop$\hspace{.2em}.
%
The matter was resolved in a clean and elegant way
by Cockett and Seely with their notion of \emph{linearly distributive category}.
%
Recall from~\cite{cockett-seely:weakly-distributive-categories,blute-cockett-seely-trimble}
that a linearly distributive category is defined as a category~$\Ccategory$
equipped with two monoidal structures $(\Ccategory,\tensor, 1)$
and $(\Ccategory,\llpar, \bot)$ together with a pair of distributivity laws
\begin{equation}\label{equation/distributivity-law-linear-distributive-categories}
\begin{array}{ccccc}
\kappa^{\,R}_{\, x,y,z} &
\quad : \quad &
(\, x \llpar y \,) \,  \tensor \, z &
\quad \morph{} \quad &
x \llpar \, (\, y \, \tensor \, z \,)
\\
\kappa^{\,L}_{\, x,y,z} &
\quad : \quad &
x \, \tensor \, (\, y \llpar z \,) &
\quad \morph{} \quad  &
(\, x \, \tensor \, y \, ) \, \llpar \, z
\end{array}
\end{equation}
between the two tensor products,
%%which relates the two tensor products, and 
which satisfy a series of coherence diagrams recalled in the paper.
%
%exhibited in~\cite{blute-cockett-seely-trimble}.
%
The two authors establish in~\cite{cockett-seely:weakly-distributive-categories}
a fundamental theorem which states (in particular) that a symmetric $\ast$-autonomous category
is the same thing as a symmetric linearly distributive category where every object~$m$ 
comes equipped with a dual object~$\rightcomplementary{m}$ together with two maps
\begin{equation}\label{equation/distributivity-axiom-cut}
\begin{array}{ccccc}
\AX{m} & \quad : \quad & \mathbf{1} & \quad \morph{} \quad & \rightcomplementary{m}\llpar m\\
\CUT{m} & \quad : \quad & m\tensor \rightcomplementary{m} & \quad \morph{} \quad & \bot
\end{array}
\end{equation}
satisfying a series of well-chosen coherence diagrams.
%
This alternative presentation of $\ast$-autonomous categories 
% is purely combinatorial
provides the expected symmetric formulation directly
based on the conjunction~$\tensor$ and on the disjunction~$\llpar$ of linear logic.
 %
A fascinating aspect of the approach is that the notion of linearly distributive category
does not require the category~$\Ccategory$ to be self-dual.
%
One should stress that in this particular presentation of $\ast$-autonomous categories,
self-duality is decoupled from~$\tensor$ and~$\llpar$ and comes only
at the very last stage, when one equips every object~$x$
of the linearly distributive category~$\Ccategory$ with a dual object~$\rightcomplementary{x}$.
%
As already explained, this very last step forces the category~$\Ccategory$
to be $\ast$-autonomous, and thus self-dual.
%

\medbreak

%
%At this point, it is important to remember that 
%
%We have already seen that 
The notion of \emph{dialogue category} provides
a categorical counterpart to tensorial logic in the same way as
the notion of $\ast$-autonomous category does for linear logic.
%
So, if one really believes in this 
%apparently 
extravagant idea that tensorial logic is a refinement of linear logic
--- rather than simply an ``intuitionistic'' fragment of it --- 
there should be a way to present dialogue categories  in a similarly symmetric fashion.
%
As we have already pointed out earlier, the problem is that this idea
does not make much sense when one looks at it with the traditional
spectacles of linear logic.
%
Recall that a dialogue category is a monoidal category
equipped with an object~$\bot$ and two natural isomorphisms
$$
\begin{array}{ccccc}
\varphi_{x,y} &  :   & \Ccategory(x\otimes y, \bot) &  \cong  & \Ccategory(y,x\leftpop\bot)
\\
\psi_{x,y} &  :  & \Ccategory(x\otimes y, \bot) & \cong  & \Ccategory(x,\bot\rightpop y)
\end{array}
$$
%each of them providing in turn a representation of the functor
%$$y\mapsto \Ccategory(x\otimes y, \bot) \quad : \quad \Ccategory^{op} \longrightarrow Set$$
%for each object~$x$, and of the functor
%$$x\mapsto \Ccategory(x\otimes y, \bot) \quad : \quad \Ccategory^{op} \longrightarrow Set$$ 
%for each object~$y$.
%
%The dialogue category is called symmetric when the underlying
%monoidal category is symmetric.
%
So, if one wants to adapt the notion of linearly distributive category
to dialogue categories, one needs
\begin{itemize}
\item[a.] to understand how and where the conjunction $\tensor$ and the disjunction $\llpar$
should be interpreted in a dialogue category,
\item[b.] to decorrelate very carefully the self-duality (for what this means) 
%between two objects~$x$ and~$\rightcomplementary{x}$ 
from the conjunction $\tensor$ and the disjunction $\llpar$ of the dialogue category,
in the same way as the self-duality is decoupled from $\ast$-autonomous categories
in order to get linearly distributive categories.
\end{itemize}
%
Again, all this does not make much sense, at least in the way it is currently formulated.
%
In particular, one does not see how to interpret the disjunction~$\llpar$ in a dialogue category,
and even worse possibly, where its self-duality lies.
%
So, one needs to change spectacles at this point, and to analyze the problem
in a different way, nurtured by 2-dimensional algebra.
%
The first thing to observe is that every dialogue category comes with an adjunction
%
\begin{equation}\label{equation/dialogue-categories-adjunction}
\xymatrix @-1.8pc {
\Ccategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\bot
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Ccategory^{\, op}}
\end{equation}
between the two negation functors
$$
L\hspace{.5em} : \hspace{.5em}
x \hspace{.5em} \mapsto \hspace{.5em} \bot\rightpop x
\quad\quad\quad\quad\quad
R\hspace{.5em} : \hspace{.5em} x \hspace{.5em} \mapsto \hspace{.5em} x\leftpop \bot
$$
This adjunction induces a monad in~$\Ccategory$
$$
T \quad : \quad x \quad \mapsto \quad (\bot\rightpop x)\leftpop\bot
\quad : \quad \Ccategory \quad \morph{} \quad \Ccategory
$$
and a comonad in~$\Ccategory^{\,op}$ 
$$
T' \quad : \quad x \quad \mapsto \quad \bot\rightpop (x\leftpop\bot)
\quad : \quad \Ccategory^{\,op} \quad \morph{} \quad \Ccategory^{\,op}
$$
which may be alternatively seen as a monad in~$\Ccategory$.
%
At this point, it is worth mentioning that a $\ast$-autonomous category
%in the traditional sense 
may be alternatively defined as a dialogue category
where the units~$\eta$ and~$\eta'$ 
of the two double negation monads~$T$ and~$T'$
$$
\eta_x \hspace{.2em} : \hspace{.2em} x \hspace{.2em} \morph{} \hspace{.4em} (\bot\rightpop x)\leftpop\bot
\quad\quad\quad\quad\quad
\eta'_x \hspace{.2em} : \hspace{.2em} x \hspace{.2em} \morph{} \hspace{.4em} \bot\rightpop (x\leftpop\bot)
$$
are invertible for every object~$x$ of the category.
%
Equivalently, a $\ast$-autonomous category is a dialogue category
where the adjunction~(\ref{equation/dialogue-categories-adjunction}) is an equivalence.
%
This establishes that one does not need to start from the notion of biclosed monoidal category
in order to define the notion of $\ast$-autonomous category: the more primitive notion
of dialogue category is sufficient for that task.
%

\medbreak 

%
At this point, a tentative solution for problem a. emerges
from the contemplation of the adjunction~(\ref{equation/dialogue-categories-adjunction})
between the category~$\Ccategory$ and its opposite category~$\Ccategory^{\, op}$.
%
The idea is to interpret the conjunction $\tensor$ as the tensor product
taken in the dialogue category~$\Ccategory$ and the disjunction $\llpar$
as the tensor product taken in the opposite dialogue category~$\Ccategory^{\, op(0,1)}$.
%
%the disjunction $(\llpar)$ as the tensor product taken in its opposite category~
%
Here, we write~$\Ccategory^{\, op(0,1)}$ for the monoidal category~$\Ccategory$
where the orientation of tensors (dimension $0$) and of morphisms (dimension $1$)
have been reversed.
%
After this appealing but also very speculative resolution of problem a. we are facing 
two additional and quite serious difficulties:
\begin{itemize}
\item[c.] on the one hand, the conjunction~$\tensor$ and the disjunction~$\llpar$
do not live in the same category, since the conjunction~$\tensor$ lives
in the category~$\Ccategory$ and the disjunction~$\llpar$ lives in its opposite category,
\item[d.] on the other hand, it is difficult to understand in what sense
the conjunction~$\tensor$ is really different from the disjunction~$\llpar$
since they are both defined as the tensor product of the category~$\Ccategory$
and of the category~$\Ccategory^{\, op}$, and consequently,
they only differ modulo the apparentlyconventional difference
between the category~$\Ccategory$ and its opposite category~$\Ccategory^{\, op}$.
\end{itemize}
%
We will see how to resolve the three difficulties b. c. and d. in three steps.
%
The first step is fundamental, although it appears at first sight as purely notational.
%
It consists in writing
$$\Acategory \quad = \quad (\Acategory,\tensorialand,\tensorialtrue)$$
for the monoidal category~$\Ccategory$ and
$$\Bcategory \quad = \quad (\Bcategory,\tensorialor,\tensorialfalse)$$
for its opposite category~$\Ccategory^{\, op(0,1)}$.
%
This resolves problem d. or at least overcomes it,
since the two categories~$\Acategory$ and~$\Bcategory$
are considered from now on as intrinsically different,
although they are ``secretly'' related by the identity
\begin{equation}\label{equation/negation-as-identity}
\Bcategory^{\, op(0,1)}  \quad = \quad \Acategory.
\end{equation}
%
Accordingly, and for clarity's sake, we choose to write conjunction as $\tensorialand$
in the category~$\Acategory$  and disjunction as~$\tensorialor$ in the category~$\Bcategory$.
%

\medbreak 

%
A good intuition to keep in mind is that~$\Acategory$ denotes 
a category of proofs implemented by one side of the logical dispute
(typically called Prover) whereas~$\Bcategory$ denotes a category
of anti-proofs implemented by the other side (typically called Denier).
%
%\medbreak 
%
We find convenient to call ``polarization'' this decoupling of the original dialogue category~$\Ccategory$
and of its opposite category~$\Ccategory^{\,op(0,1)}$ in two independent components~$\Acategory$ and~$\Bcategory$.
%
The terminology pays tribute to the notion of \emph{polarity}
introduced by Jean-Yves Girard in his seminal work on classical logic.
%
The key insight of this work was to polarize the formulas of classical logic
in order to interpret every positive formula as a commutative $\tensor$-comonoid 
and every negative formula as a commutative $\llpar$-monoid
in the category of coherence spaces, see~\cite{girard:lc} for details.
%
%who very early introduced a distinction between positive and negative formula
%in order to interpret classical logic in correlation spaces~\cite{girard:lc}.
%
%The idea of decoupling emerged from the categorical study of this construction.
Our own decision of decoupling the category~$\Ccategory$ from
its opposite category~$\Ccategory^{\,op(0,1)}$ is directly inspired
by this construction.
%
The idea of decoupling reveals the intrinsically 2-dimensional nature
of the construction and generalizes it at the same time to a large variety
of proof systems besides classical logic.
%
%In our case, the positive formulas would be interpreted in the category~$\Acategory$
%and the negative formulas in the category~$\Bcategory$.
% work on classical logic.
%originally emerged in our work on game semantics,
% the comparison
%of the category~$\Acategory$ of Opponent-starting games and 
%of the category~$\Bcategory$ of Proponent-starting games in Conway games, 
%is directly inspired by this work.
%
%Decoupling captures the cardinal idea of Girard's construction in~\cite{girard:lc}
%and generalizes it to a large variety of proof systems besides classical logic.
%
%This leads to various systems of polarities 
%--- going far beyond the notion of polarity originally imagined by Girard.
%
Typically, when applied to a purely ``intuitionistic'' situation like cartesian closed categories,
decoupling induces the same ``classical'' decomposition of implication as in linear logic,
with a notion of polarity intrinsically different from Girard's original notion of polarity,
% for classical logic,
see~\cite{mellies:tensorial-logic-2} for details.
%
%In our polarized formulation of dialogue categories, positive formulas would be
%interpreted in~$\Acategory$ whereas negative formulas would be interpreted in~$\Bcategory$.

%Correlation spaces define a cartesian dialogue category~$\Ccategory$
%where positive formulas are interpreted in~$\Acategory$
%and negative formulas are interpreted in~$\Bcategory$.
%In a similarly polarized account of tensorial logic, the positive formulas
%are interpreted in~$\Acategory$ whereas the negative formulas
%are interpreted in~$\Bcategory$.
%One main contribution of our algebraic approach is to establish
%that there exist several notions of polarities.

\medbreak

The problem c. is resolved at this point by recasting
the original adjunction~(\ref{equation/dialogue-categories-adjunction})
as the adjunction
\begin{equation}\label{equation/dialogue-chiralities-adjunction}
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\bot
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory}
\end{equation}
between the categories~$\Acategory$ and~$\Bcategory$.
%
In that way, the conjunction~$\tensorialand$ and the disjunction~$\tensorialor$ 
live in \emph{different} categories~$\Acategory$ and~$\Bcategory$ related by the functors~$L$
and~$R$ of the adjunction~(\ref{equation/dialogue-chiralities-adjunction}).
%
\medbreak 

%
The ongoing analysis is sufficiently advanced to provide the ground 
for a polarized notion of ``linearly distributive category'' adapted 
to tensorial logic.
%
The key idea is that the linearly distributive category~$\Ccategory$
together with its two tensor products~$\tensor$ and $\llpar$
should be replaced 
%in the case of tensorial logic 
by \emph{a pair} of monoidal categories
\begin{equation}\label{equation/pair-of-monoidal-categories}
(\Acategory,\tensorialand,\tensorialtrue)
\quad\quad\quad\quad\quad
(\Bcategory,\tensorialor,\tensorialfalse)
\end{equation}
equipped with an adjunction~(\ref{equation/dialogue-chiralities-adjunction})
relating them.
%
In addition, the original pair of distributivity laws~(\ref{equation/distributivity-law-linear-distributive-categories})
should be replaced by the following pair of distributivity laws
%
\begin{equation}
\label{equation/distributivity-laws-conversing-pair}
\begin{array}{ccccc}
\contau
& \quad : \quad &
R(b\tensorialor L(a)) \tensorialand m
& \quad \morph{} \quad &
R(b\tensorialor L(a\tensorialand m))
\\
\distau & \quad : \quad &
L(a\tensorialand R(b\tensorialor n))
& \quad \morph{} \quad &
L(a\tensorialand R(b))\tensorialor n
\end{array}
\end{equation}
%
Although these distributivity laws may appear intimidating at first sight,
we will see that each of them conveys an absolutely fundamental principle of logic.
%
In particular, they hold in \emph{every} dialogue category and 
thus secretly regulate essentially every existing logical system.
%

\medbreak


Putting~(\ref{equation/dialogue-chiralities-adjunction}-\ref{equation/pair-of-monoidal-categories}-\ref{equation/distributivity-laws-conversing-pair})
together leads to the notion of \emph{linearly distributive chirality}
introduced in the technical core of the paper, see~\S\ref{section/linearly-distributive-chirality}
for details.
%
This two-sided notion of chirality refines the one-sided notion of linearly distributive category
in just the same way as the notion of dialogue category refines the notion of $\ast$-autonomous category.
%
It is worth mentioning that the notion of chirality we have in mind here
is \emph{mixed} rather than \emph{pure} in the sense of~\cite{mellies:tensorial-logic-2}.
%
A mixed chirality is a pair of categories in which the side~$\Bcategory$ 
is not required to be equivalent to the opposite of the side~$\Acategory$ 
in contrast to the case of a pure chirality.
%
The resulting notion of linearly distributive chirality satisfies two cardinal properties:
\begin{itemize}
\item every dialogue category~$\Ccategory$ defines a linearly distributive
chirality whose sides~$\Acategory$ and~$\Bcategory$ are
defined as $\Acategory=\Ccategory$ and $\Bcategory=\Ccategory^{\, op(0,1)}$
and whose functors $L$ and $R$ are defined as negation functors,
%as indicated above,
\item a linearly distributive category~$\Ccategory$ is the same thing 
as a linearly distributive chirality where the two sides $\Acategory$ and $\Bcategory$
are defined as the category~$\Ccategory$ and where the two functors~$L$ and~$R$
are defined as the identity functor between the category~$\Ccategory$ and itself.
\end{itemize}
%
In the same way as we call ``polarization'' the process
of decoupling~$\Ccategory$ and its opposite category~$\Ccategory^{\,op(0,1)}$,
%into a pair of independent components~$\Acategory$ and~$\Bcategory$, 
we find convenient to call ``depolarization'' the operation of restricting
the definition of a linearly distributive chirality to the specific case
when the two sides~$\Acategory$ and~$\Bcategory$ coincide
and when the two functors~$L$ and~$R$
are defined as identity functors.
%of a linearly distributive category~$\Ccategory$.
%
%The terminology is justified by the fact that the two sides $\Acategory$ and $\Bcategory$ are equal
%in that case to the same category~$\Ccategory$, and the functors~$L$ and~$R$ are identity functors
%between~$\Ccategory$ and itself.
%
The philosophy of tensorial logic is that all the concepts and constructions
of linear logic should have a counterpart in tensorial logic,
from which they may be then recovered by depolarization.
%
The notion of linearly distributive category offers a typical illustration of this principle,
since we will see that it may be recovered by depolarization from the notion of linearly distributive chirality.
%as we have just claimed.
%in tensorial logic, and may be then recovered by depolarization, as we have just seen.
%
%Another example is provided by the notion of multiplicative proof-net in linear logic
%which upgrades to the notion of tensorial proof-net in tensorial logic, reintegrating
%the execution time in the logic, with deep connections to game semantics, see~\S\ref{section/proof-nets} for a discussion.
%

\medbreak

%
Once again, it is worth stressing the nice symmetry between the two distributivity laws~$\contau$ and~$\distau$.
%
This symmetry is an instance of the \emph{chirality principle} between proofs
and anti-proofs observed in~\cite{mellies:tensorial-logic-1}.
%
This symmetry is witnessed in this case by the fact that each of the two laws may be obtained
from the other one by applying the involution 
$$
R \hspace{.5em} \leftrightarrow \hspace{.5em} L
\quad\quad\quad
x \, \tensorialand \, y \hspace{.5em} \leftrightarrow \hspace{.5em} x \, \tensorialor \, y
\quad\quad\quad
a \hspace{.5em} \leftrightarrow \hspace{.5em} b
\quad\quad\quad
m \hspace{.5em} \leftrightarrow \hspace{.5em} n
$$
and by reversing the orientation of the map.
%
After ``depolarization'' to the specific case of a linearly distributive chirality~$(\Ccategory,\Ccategory)$
with~$L=R=id_{\Ccategory}$ coming from a linearly distributive category~$\Ccategory$,
this mirror symmetry between~$\contau$ and~$\distau$ boils down\footnote{The discovery of this unexpected
degeneracy of linear logic was the starting point of tensorial logic in May 2006.}
to the ``self-symmetry'' of the two components~$\kappa^{\, R}$ and~$\kappa^{\, L}$
of the original distributivity law~(\ref{equation/distributivity-law-linear-distributive-categories}).
%or more precisely to the symmetry between the left and right variants
%


\medbreak 

%
Now that we have designed a tensorial counterpart to the notion of linearly distributive category,
we are very close to the resolution of problem b.
and to understanding how the self-duality of $\ast$-autonomous categories
may be adapted to dialogue categories.
%
The key idea is to take the identity~(\ref{equation/negation-as-identity})
very seriously, and to relax it
% (and upgrade it at the same time)
to a monoidal equivalence
\begin{equation}\label{equation/negation-as-equivalence}
%\begin{equation}\label{equation/dialogue-categories-monoidal-equivalence}
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{\rightcomplementary{(-)}}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{\leftcomplementary{(-)}}
&
\Bcategory^{\, op(0,1)}}
\end{equation}
between the monoidal categories~$\Acategory$ and~$\Bcategory^{\, op(0,1)}$
respectively equipped with conjunction~$\tensorialand$
and the disjunction~$\tensorialor^{\, op}$ oriented right-to-left.
%
The decision of relaxing the identity~(\ref{equation/negation-as-identity})
into a monoidal equivalence~(\ref{equation/negation-as-equivalence})
is motivated by the desire to encapsulate the original notion of \emph{duality} introduced
by Cockett and Seely~\cite{cockett-seely:weakly-distributive-categories,blute-cockett-seely-trimble}
for linearly distributive categories, see \S\ref{section/monoidal/dualities} for details.
%
The important point to remember here is that the negation functor of a $\ast$-autonomous category
is not required to be strictly involutive --- but only involutive up to equivalence.
%
By shifting from an equality to an equivalence~(\ref{equation/negation-as-equivalence})
the notion of duality on a linearly distributive chirality~$(\Acategory,\Bcategory)$
thus includes the two cases we have in mind:
\begin{itemize}
\item in the case of a dialogue category~$\Ccategory$,
the equivalence~(\ref{equation/negation-as-equivalence})
is defined by taking the identity functors between~$\Ccategory$ and itself,
\item in the case of a $\ast$-autonomous category~$\Ccategory$,
the equivalence~(\ref{equation/negation-as-equivalence})
is defined by taking the two negation functors
between the category~$\Ccategory$ and its opposite
category~$\Ccategory^{\, op(0,1)}$.
%described as a linearly distributive category~$\Ccategory$
%equipped with a notion of duality.
\end{itemize}
%
At this stage, we have resolved the four obstructions a. b. c. and d. 
%to the very idea of presenting the notion of dialogue category in a nice and symmetric fashion.
%
In order to complete our program, there simply remains to formulate a variant of duality
refining~(\ref{equation/distributivity-axiom-cut})
between an object~$m$ in the category~$\Acategory$ and an object~$\rightcomplementary{m}$
in the category~$\Bcategory$.
%
We will see that this polarized notion of duality requires the existence of the two combinators
%
$$
\begin{array}{ccc}
\AX{m} & \quad : \quad & \tensorialtrue \quad \morph{} \quad \rightadjoint \, ( \,  \rightcomplementary{m} \, \tensorialor \, \leftadjoint \, ( \, m \, ) \, )
\\
\CUT{m} & \quad : \quad & \leftadjoint \, ( \,  m \, \tensorialand \,  \rightadjoint \, ( \, \rightcomplementary{m} \, ) \, ) 
\quad \morph{} \quad \tensorialfalse.
\end{array}
$$
As expected, one recovers the two combinators~(\ref{equation/distributivity-axiom-cut}) 
after depolarization to a situation where the two sides of the linearly distributive chirality coincide,
%coincide with a linearly distributive category~$\Ccategory$, 
with $L$ and $R$ equal to the identity functor.
%
We will also see that the existence of such a duality for every object~$m$ of the category~$\Acategory$
implies that~$\Acategory$ defines a dialogue category ---
at least when~$\Acategory$ and~$\Bcategory$ are \emph{symmetric} monoidal categories,
see \S\ref{section/conclusion} for details.
%, but also symmetric monoidal.

%\medbreak

%
%So, let us summarize at this point.
%It is probably time to summarize at this stage.
%
\paragraph{A brief summary.}
What have we learned from this short journey in the universe of logical symmetries?
%
We would say, three things essentially:
\begin{itemize}
\item that every category~$\Acategory=\Ccategory$ of proofs
comes with an opposite category~$\Bcategory=\Ccategory^{\, op(0,1)}$
of anti-proofs (or refutations) which may be decoupled from~$\Ccategory$,
% and considered as a proper category of anti-proofs (or refutations)
\item that every formula~$x$ of the logic may be either seen from the point of view of
the Prover or from the point of view of the Denier,
% according to a \emph{change of frame}
%$x\mapsto\rightcomplementary{x}$ between~$\Acategory$ and~$\Bcategory$,
%is precisely what the ``classical'' involutive negation of linear logic $x\mapsto\rightcomplementary{x}$ reflects
\item that the change of frame $x\mapsto\rightcomplementary{x}$ between Prover in~$\Acategory$ 
and Denier in~$\Bcategory$ is \emph{involutive} even in the case of
an ``intuitionistic'' system like tensorial logic.
%\item that this symmetry between~$\Acategory$ and~$\Bcategory$ 
%has nothing to do with the fact that linear logic is ``classical'' since
%it also holds in an ``intuitionistic'' system like tensorial logic.
\end{itemize}
%
%An important contribution of the present line of work
%is possibly the discovery that this symmetry between~$\Acategory$ and~$\Bcategory$ 
%has nothing to do with the fact that linear logic is ``classical'' since
%it also holds in an intuitionistic system like tensorial logic.
%
We have all reasons to believe that this new scenography of logic
is more harmonious and satisfactory than the old-fashioned picture
with its rigid separation between classical and intuitionistic logic.
%
%
Behind the idea of change of frame lies a ``relativity'' principle
which tells that every logical dispute in tensorial logic
is invariant under the internal symmetry Prover\,/\,Denier.
%involves a Player (or Prover)
%and an Opponent (or Refutator) and that each of them
%looks at the formula from his (or her) own point of view.
%
The superficial belief that tensorial logic should lack the nice symmetries
of linear logic is an illusion coming from the fact that the category~$\Acategory$
of proofs happens to coincide in linear logic
% (up to equivalence) 
with the category~$\Bcategory$ of anti-proofs.
%

\medbreak




%

\medbreak


%
%Besides our debt to the notion of polarity introduced by Jean-Yves Girard,
We would like to stress here how much this alternative picture of logic
owes to the technical shift from 1-dimensional to 2-dimensional categories.
%
%Nothing would have been possible without it.
%
This shift is indeed necessary in order to realize that
%In particular, the shift to 2-categories enables to articulate the fact that
%As a matter of fact, this 2-dimensional understanding of logic is prerequisite
%in order to articulate the fact that
the primitive symmetry between Prover and Denier
lives at a 2-dimensional level, rather than at the 1-dimensional 
(that is, categorical) level --- as one generally believed.
%
There lies an important microcosm principle in logic formulated
for the first time in~\cite{mellies:tensorial-logic-2}
and directly inspired by a similar phenomenon in higher dimensional algebra
pointed out by Baez and Dolan~\cite{baez-dolan:hda3}.
%
The microcosm principle tells that any contravariant operation 
--- like negation or implication --- relies in the end on 
the internal symmetry $\Ccategory\mapsto\Ccategory^{\, op(0,1)}$
of the 2-category~$Cat$ of categories.
%
In other words, the primary duality of logic is provided by the 2-dimensional
operation of ``reversing''  a category~$\Ccategory$ of proofs
into its opposite category~$\Ccategory^{\, op(0,1)}$ of anti-proofs.
%
We like to think that this purely formal and algebraic observation
reflects
%in a striking way 
the phylogenetic principle that
%(possibly ethological) 
%\begin{center}
\emph{symmetry comes before logic\,}\footnote{An intellectual challenge
for logicians today is to develop a sufficiently fine-grained understanding
(or anatomy) of formal logic in order to articulate it
with the investigations on the evolutionary mechanisms 
which lead to the emergence of logical or prelogical reasoning
in the human societies.}.
% in our human species.}
%, as part of the current investigation of social behaviours in the animal reign.}
%\end{center}
%
%Every logical system appears in this way as a specific linguistic regime
%designed to accomodate this primitive symmetry between Player
%and Opponent, and to make the two sides of the dispute interact.
%%
%

\medbreak 

%
%
An illuminating spiritual exercise at this stage
is to look at linear logic in retrospect
with this new picture in mind.
%~$\Ccategory\mapsto\Ccategory^{\,op(0,1)}$
%
Linear logic appears then as the historical
and somewhat miraculous encounter (second part of the 1980s)
%the somewhat miraculous encounter in the second part of the 1980s
%(and at the same time confusion)
between this internal symmetry~$\Ccategory\mapsto\Ccategory^{\, op(0,1)}$
of a 2-dimensional nature
% between~$\Ccategory$ and~$\Ccategory^{\, op(0,1)}$
and the 1-dimensional notion of $\ast$-autonomous category.
%
%From this magnificent quiproquo 
From this singular quiproquo followed the long-standing belief 
that the ``classical'' symmetries of linear logic have to do with the fact
that every $\ast$-autonomous category~$\Ccategory$ is itself self-dual ---
in the technical sense that~$\Ccategory$ is equivalent to its opposite category~$\Ccategory^{\, op(0,1)}$.
%
Our main purpose in the present paper is to clarify this extraordinary misunderstanding,
%and to dissect the ``classical'' symmetries of linear logic in order to upgrade them to tensorial logic.
%and to dissect the micro-structure of negation in order
and to dissect the micro-structure of tensorial negation in such a way
as to make the flow of time explicit in the logic --- see \S\ref{section/proof-nets} for a discussion.
%upgrade linear logic to tensorial logic by integrating
%the flow of time in the logic --- see \S\ref{section/proof-nets} 
%for a graphical comparison.
%discussion.

% linear logic in order to upgrade its combinatorics to tensorial logic.
%reintegrate time in the logic, see \S\ref{section/proof-nets} for details.
% its combinatorial structure to tensorial logic.
%
%This leads to a clear polarization of the logic between the category~$\Acategory$ of proofs and
%the category~$\Bcategory$ of anti-proofs (or refutations)
%and a careful reintegration of time in the logic (see \S\ref{section/proof-nets} for details).

%and to bring to light the primary structure of 
%tensorial logic based on the 2-dimensional duality $\Ccategory\mapsto \Ccategory^{\, op(0,1)}$
%and its refraction in the 1-dimensional notion of dialogue category.
% logical system.
%connecting the 1-dimensional to a 2-dimensional structures.
%On the other hand, the general belief that the ``classical'' symmetries of linear logic
%have to do with the fact that negation is involutive
%is driven by an old misconception about the nature of symmetries in logic.



\paragraph{Plan of the paper.}
We start by recalling in~\S\ref{section/linearly-distributive-categories}
the notion of linearly distributive category introduced by Cockett and Seely
in~\cite{cockett-seely:weakly-distributive-categories} together
with the notion of right duality we will be specifically interested in.
%
We recall in \S\ref{section/dialogue-chiralities} the notion of dialogue chirality
introduced by the author in~\cite{mellies:tensorial-logic-2} as a symmetric
and deformed notion of dialogue category.
%
Follows in \S\ref{section/proof-nets} a discussion on the reintegration
of time in the traditional proof-net syntax of linear logic.
%
The notion of bimodulation between modulations (also called lax actions
or parametric monads) is then recalled in~\S\ref{section/bimodulations}.
%
We reach in \S\ref{section/linearly-distributive-chirality} the technical core
of the paper, where we introduce the notion of linearly distributive chirality,
and formulate the corresponding notion of right duality.
%
We establish at the end of the section that the notion of dialogue chirality
coincides with the notion of linearly distributive chirality with a right duality
when the underlying monoidal categories are symmetric.
%
We conclude in \S\ref{section/conclusion} by observing that a mismatch
remains between the two notions of dialogue chirality and linearly distributive chirality
in the case of non-symmetric monoidal categories.
%
We leave the task of resolving this matter to the companion paper~\cite{mellies:tensorial-logic-5}.

\section{Linearly distributive categories}\label{section/linearly-distributive-categories}
\newcommand{\cotensor}{\llpar}
%\newcommand{\cotensor}{\small{\bigcirc}}
\newcommand{\unitt}{\mathbf{1}}
\newcommand{\unitcot}{\bot}
\newcommand{\alphat}{\alpha^{\tensor}}
\newcommand{\lambdat}{\lambda^{\tensor}}
\newcommand{\rhot}{\rho^{\tensor}}
\newcommand{\alphacot}{\alpha^{\cotensor}}
\newcommand{\lambdacot}{\lambda^{\cotensor}}
\newcommand{\rhocot}{\rho^{\cotensor}}
\newcommand{\distL}{\kappa^L}
\newcommand{\distR}{\kappa^R}
\newcommand{\leftdual}[1]{{}^{\ast}{#1}}
\newcommand{\leftdualbis}[1]{{}^{\circ}\!{#1}}
\newcommand{\rightdual}[1]{{#1}^{\ast}}
\newcommand{\distributiveleftaxiom}[1]{\mathbf{\overline{AX}}{[{#1}]}}
\newcommand{\distributiveleftcut}[1]{\mathbf{\overline{CUT}}{[{#1}]}}
\newcommand{\distributiverightaxiom}[1]{\mathbf{AX}{[{#1}]}}
\newcommand{\distributiverightcut}[1]{\mathbf{CUT}{[{#1}]}}
%\newcommand{\distributiveleftaxiom}[1]{\mathit{ax}^{L}_{#1}}
%\newcommand{\distributiveleftcut}[1]{\mathit{cut}^{L}_{#1}}
%\newcommand{\distributiverightaxiom}[1]{\mathit{ax}^{R}_{#1}}
%\newcommand{\distributiverightcut}[1]{\mathit{cut}^{R}_{#1}}
\newcommand{\gammat}{\gamma^{\tensor}}
\newcommand{\gammacot}{\gamma^{\cotensor}}
%
We start by recalling the notion of linearly distributive category
in~\S\ref{section/linearly-distributive-category/definition}
and introduce the notion of right duality in~\S\ref{section/monoidal/dualities}.
%
We establish in~\S\ref{section/linearly-distributive-category/main-statement}
that every linearly distributive category with a right duality is monoidal closed
on the left.
%
We introduce the symmetric notion of left duality in~\S\ref{section/left-dualities}
and show that every linearly distributive category equipped with a left
\emph{and} a right duality defines a $\ast$-autonomous category.
%
Finally, we establish in~\S\ref{section/monoidality-of-right-duality}
that every right duality defines a monoidal functor between
the underlying linearly distributive category~$\Ccategory$
equipped with~$\tensor$ and its opposite category equipped with~$\cotensor$.

\subsection{Definition}\label{section/linearly-distributive-category/definition}
Recall from~\cite{cockett-seely:weakly-distributive-categories,blute-cockett-seely-trimble} 
that a (planar) linearly distributive category $\Ccategory$ is defined as a category equipped
with two monoidal structures, the first one called ``tensor product''
given by the bifunctor $\tensor:\Ccategory\times\Ccategory\morph{}\Ccategory$
with unit $\unitt$ and natural isomorphisms
$$\alphat_{x,y,z}:(x\tensor y)\tensor z \morph{} x\tensor (y\tensor z)$$
$$\lambdat_{x}:\unitt\tensor x\morph{} x
\hspace{3em}
\rhot_{x}:x\morph{}x\tensor\unitt$$
and the second one called ``cotensor product'' given by the bifunctor 
$\cotensor:\Ccategory\times\Ccategory\morph{}\Ccategory$
with unit $\unitcot$ and natural isomorphisms
$$\alphacot_{x,y,z}:x\cotensor (y\cotensor z) \morph{} (x\cotensor y)\cotensor z$$
$$\lambdacot_{x}:x\morph{}\unitcot\cotensor x
\hspace{3em}
\rhocot_{x}:x\cotensor\unitcot\morph{} x.$$
%
%The operations $\tensor$ and $\cotensor$ are called ``tensor product'' and ``cotensor product'' respectively.
%
Linearly distributive categories are moreover equipped with two natural morphisms
%The tensor product is required to distribute over the cotensor product
%by natural morphisms
$$
\distL_{x,y,z}: x\tensor (y\cotensor z) \morph{} (x\tensor y)\cotensor z
$$
$$
\distR_{x,y,z}: (x\cotensor y)\tensor z \morph{} x\cotensor (y\tensor z)
$$
required to satisfy a series of commutativity axioms,
consisting of six pentagons and four triangles.
%
The six pentagons may be separated into three series of two pentagons,
where the first series describes how the distributive law~$\distR$ interacts
with the associativity laws:
%
% pentagone A1
%
$$\vcenter{
\xymatrix @-1pc {
((w\cotensor x)\tensor y)\tensor z
\ar[rr]^-{\distR}
\ar[dd]_-{\alphat}
&&
(w\cotensor (x\tensor y))\tensor z
\ar[rr]^{\distR}
&&
w\cotensor ((x\tensor y)\tensor z)
\ar[dd]^-{\alphat}
\\
\\
(w\cotensor x)\tensor (y\tensor z)
\ar[rrrr]^-{\distR}
&&&&
w\cotensor (x\tensor (y\tensor z))
}}$$
%
% pentagone B2
%
$$\vcenter{
\xymatrix @-1pc {
(w\cotensor (x\cotensor y))\tensor z
\ar[rr]^-{\distR} 
\ar[dd]_-{\alphacot}
&&
w\cotensor ((x\cotensor y)\tensor z)
\ar[rr]^-{\distR}
&&
w\cotensor (x\cotensor (y\tensor z))
\ar[dd]^-{\alphacot}
\\
\\
((w\cotensor x)\cotensor y)\tensor z
\ar[rrrr]^-{\distR}
&&&&
(w\cotensor x)\cotensor (y\tensor z)
}}$$
the second series describes how the distributive law~$\distL$ interacts with
the associativity laws:
%
% pentagone C4
%
$$\vcenter{
\xymatrix @-1pc {
(w\tensor x)\tensor (y\cotensor z)
\ar[rrrr]^-{\distL}
\ar[dd]_-{\alphat}
&&&&
((w\tensor x)\tensor y)\cotensor z
\ar[dd]^-{\alphat}
\\
\\
w\tensor (x\tensor (y\cotensor z))
\ar[rr]^-{\distL}
&&
w\tensor ((x\tensor y)\cotensor z)
\ar[rr]^-{\distL}
&&
(w\tensor (x\tensor y))\cotensor z
}}$$
%
% pentagone D3
%
$$\vcenter{
\xymatrix @-1pc {
w\tensor (x\cotensor (y\cotensor z))
\ar[rrrr]^-{\distL}
\ar[dd]_-{\alphacot}
&&&&
(w\tensor x)\cotensor (y\cotensor z)
\ar[dd]^-{\alphacot}
\\
\\
w\tensor ((x\cotensor y)\cotensor z)
\ar[rr]^-{\distL}
&&
(w\tensor (x\cotensor y))\cotensor z
\ar[rr]^-{\distL}
&&
((w\tensor x)\cotensor y)\cotensor z
}}$$
and the last series describes how~$\distL$ and $\distR$ interact 
together with the associativity laws:
% pentagone E6 (mysterious)
%
%\begin{equation}\label{equation/pentagon-5}
$$\vcenter{
\xymatrix @-1pc {
(w\tensor (x\cotensor y))\tensor z
\ar[dd]_-{\distL}
\ar[rr]^{\alphat}
&&
w\tensor ((x\cotensor y)\tensor z)
\ar[rr]^{\distR}
&&
w\tensor(x\cotensor (y\tensor z))
\ar[dd]^-{\distL}
\\
\\
((w\tensor x)\cotensor y)\tensor z
\ar[rrrr]^{\distR}
&&&&
(w\tensor x)\cotensor (y\tensor z)
}}$$
%\end{equation}
%
%
%A sixth pentagon is required to commute in the original definition
%of a linearly distributive category formulated in~\cite{blute-cockett-seely-trimble}.
%
%However, although it looks like the fifth pentagon~(\ref{equation/pentagon-5}),
%we will see in the course of the paper that this last pentagon
%is of a different nature of the previous five diagrams, and that
%it may be considered as problematic in some specific situations.
%
% pentagone 5
%
$$\vcenter{
\xymatrix @-1pc {
(w\cotensor x)\tensor (y\cotensor z)
\ar[rrrr]^-{\distL}
\ar[dd]_-{\distR}
&&&&
((w\cotensor x)\tensor y)\cotensor z
\ar[dd]^-{\distR}
\\
\\
w\cotensor (x\tensor (y\cotensor z))
\ar[rr]^-{\distL}
&&
w\cotensor ((x\tensor y)\cotensor z)
\ar[rr]^-{\alphacot}
&&
(w\cotensor (x\tensor y))\cotensor z
}}$$
%
%
Similarly, the four coherence triangles may be separated in two series
of two triangles, where the first series describes how
the distributive law~$\distR$ interacts with the units:
%
$$\begin{array}{cc}
\xymatrix  @-1.9pc {
&&
x\tensor y
\ar[rrddd]^-{\lambdacot}
\ar[llddd]_-{\lambdacot}
\\
\\
\\
(\unitcot \cotensor x)\tensor y
\ar[rrrr]^{\distR}
&&&&
\unitcot \cotensor (x\tensor y)
}
&
\xymatrix  @-1.9pc {
&&
x\cotensor y
\ar[llddd]_-{\rhot}
\ar[rrddd]^-{\rhot}
\\
\\
\\
(x\cotensor y)\tensor \unitt
\ar[rrrr]^{\distR}
&&&&
x\cotensor (y\tensor \unitt)
}
\end{array}$$
and the second series describes how the distributive law~$\distL$
interacts with the units:
$$\begin{array}{cc}
\xymatrix  @-1.9pc {
\unitt\tensor (x\cotensor y)
\ar[rrrr]^{\distL}
\ar[rrddd]_-{\lambdat}
&&&&
(\unitt\tensor x)\cotensor y
\ar[llddd]^-{\lambdat}
\\
\\
\\
&&
x\cotensor y
}
&
\xymatrix  @-1.9pc {
x\tensor (y\cotensor \unitcot)
\ar[rrrr]^{\distL}
\ar[rrddd]_-{\rhocot}
&&&&
(x\tensor y)\cotensor \unitcot
\ar[llddd]^-{\rhocot}
\\
\\
\\
&&
x\tensor y
}
\end{array}$$
One requires that these diagrams commute 
for all objects~$w,x,y,z$ of the linearly distributive category~$\Ccategory$.


%
\subsection{Right dualities in linearly distributive categories}
\label{section/monoidal/dualities}
%
\index{Linearly distributive categories!Duality}
%
A general notion of negation in a linearly distributive category~$\Ccategory$
is introduced by Cockett and Seely in~\cite{cockett-seely:weakly-distributive-categories}.
%
Here, we find convenient to keep only half of it.
%
This leads us to the notion of \emph{right duality} in a linearly distributive category~$\Ccategory$, defined below.
%
The complementary notion of \emph{left duality} is discussed at the end of the section.
%paper (see~\S\ref{section/conclusion}).
%
 \begin{definition}
A right duality in a linearly distributive category~$\Ccategory$
consists of the following data:
\begin{itemize}
\item an object $\rightdual{x}$,
\item two morphisms
$\distributiverightaxiom{x}:\unitt\morph{}\rightdual{x}\cotensor x$
and
$\distributiverightcut{x}:x\tensor\rightdual{x}\morph{}\unitcot$
\end{itemize}
for every object $x$ of the category~$\Ccategory$.
%
The morphisms are moreover required to make the diagrams
\begin{equation}\label{equation/right-axiom-coherence-for-linearly-distributive-categories}
\begin{tabular}{ccc}
$
\vcenter{\xymatrix @-.1pc {
x\tensor \unitt
\ar[rr]^-{x\,\tensor\,\distributiverightaxiom{x}}
&&
x\tensor(\rightdual{x}\cotensor x)
\ar[d]^-{\distL}
\\
&&
(x\tensor\rightdual{x})\cotensor x
\ar[d]^-{\distributiverightcut{x}\cotensor x}
\\
x
\ar[uu]^-{\rhot}
\ar[rr]^-{\lambdacot}
&&
\unitcot\cotensor x
}}$
& \hspace{1em} &
$\vcenter{\xymatrix @-.1pc {
\unitt\tensor\rightdual{x}
\ar[dd]_-{\lambdat}
\ar[rr]^-{\distributiverightaxiom{x}\,\tensor\,\rightdual{x}}
&&
(\rightdual{x}\cotensor x)\tensor\rightdual{x}
\ar[d]^-{\distR}
\\
&&
\rightdual{x}\cotensor (x\tensor\rightdual{x})
\ar[d]^-{\rightdual{x}\cotensor\distributiverightcut{x}}
\\
\rightdual{x}
&&
\rightdual{x}\cotensor\unitcot
\ar[ll]_-{\rhocot}
}}$
\end{tabular}
\end{equation}
commute.
%
\end{definition}
%
%
Every such right duality defines a contravariant functor
$$x\mapsto \rightdual{x} \quad : \quad \Ccategory\morph{}\Ccategory^{\, op}$$
which transports every morphism $f:x\morph{}y$ of the linearly distributive
category~$\Ccategory$ to the morphism
$\rightdual{f}:\rightdual{y}\morph{}\rightdual{x}$
defined in the following way:
$$\xymatrix @-.2pc {
\rightdual{y}\ar[d]_-{(\lambdat)^{-1}}
&&
\rightdual{x}\cotensor (x\tensor\rightdual{y})
\ar[rr]^-{\rightdual{x}\cotensor (f\tensor\rightdual{y})}
&&
\rightdual{x}\cotensor (y\tensor\rightdual{y})
\ar[rr]^-{\rightdual{x}\cotensor\distributiverightcut{y}}
&&
\rightdual{x}\cotensor \unitcot
\ar[d]^-{\rhocot}
\\
\unitt\tensor\rightdual{y}
\ar[rr]^-{\distributiverightaxiom{x}\tensor\rightdual{y}}
&&
(\rightdual{x}\cotensor x)\tensor\rightdual{y}
\ar[u]^-{\distR}
\ar[rr]^-{(\rightdual{x}\cotensor f)\tensor\rightdual{y}}
&&
(\rightdual{x}\cotensor y)\tensor\rightdual{y}
\ar[u]_-{\distR}
&&
\rightdual{x}
}$$
The functoriality of $x\mapsto \rightdual{x}$ follows easily from the coherence diagrams.
%
The construction of $\rightdual{f}$ also ensures that the two families
$\distributiverightaxiom{-}$ and $\distributiverightcut{-}$ are dinatural
in the sense that the two diagrams
$$
\vcenter{\xymatrix @-1.2pc {
&& 
\rightdual{x}\cotensor x
\ar[rdd]^-{x\cotensor f}
\\
\\
\unitt
\ar[rruu]^-{\distributiverightaxiom{x}}
\ar[rrdd]_-{\distributiverightaxiom{y}}
&&&
\rightdual{x}\cotensor y
\\
\\
&&
\rightdual{y} \cotensor y
\ar[ruu]_-{\rightdual{f}\cotensor y}
}}
\quad\quad\quad\quad
\vcenter{\xymatrix @-1.2pc {
& 
y\tensor \rightdual{y}
\ar[rrdd]^-{\distributiverightcut{y}}
\\
\\
x\tensor \rightdual{y}
\ar[ruu]^-{f\tensor\rightdual{y}}
\ar[rdd]_-{x\tensor\rightdual{f}}
&&&
\unitcot
\\
\\
&
x\tensor \rightdual{x}
\ar[rruu]_-{\distributiverightcut{x}}
}}
$$
commute for every morphism~$f:x\to y$.

%\subsection{Alternative formulation of $\ast$-autonomous categories}
\subsection{Main statement}\label{section/linearly-distributive-category/main-statement}
%
As explained in the introduction, one main purpose of the notion of linearly distributive category
is to isolate the properties of $\tensor$ and $\cotensor$
from the properties of the duality in a $\ast$-autonomous category.
%
In particular, the notion of right duality is motivated by the following property,
which states that every linearly distributive category~$\Ccategory$ equipped
with a right duality is monoidal closed on the left.
%
\begin{proposition}
\label{proposition/main-result-linearly-distributive-categories}
In any linearly distributive category~$\Ccategory$ with a right duality,
\begin{itemize}
\item the functor $(x\tensor -)$ is left adjoint to the functor $(\rightdual{x}\cotensor -)$
\item the functor $(-\cotensor y)$ is right adjoint to the functor $(-\tensor \rightdual{y})$
\end{itemize}
for all objects $x,y$ of the category.
%
In particular, every such category~$\Ccategory$ is monoidal closed on the left,
with implication defined as
$$
x \, \leftpop \, y \quad = \quad \rightdual{x} \, \cotensor \, y.
$$
\end{proposition}
The proof is essentially immediate.
%
One associates to every morphism
$$
f \quad : \quad x\tensor y \quad \morph{} \quad z
$$
the morphism~$\varphi_{x,y,z}(f)$ defined as the composite
$$
\xymatrix @-1pc {
y\ar[rr]^-{(\lambdat)^{-1}}
&&
\unitt\tensor y\ar[rrr]^-{\distributiverightaxiom{x}}
&&&
(\rightdual{x}\cotensor x) \tensor y
\ar[rr]^-{\distR}
&&
\rightdual{x}\cotensor (x \tensor y)
\ar[rr]^-{f}
&&
\rightdual{x}\cotensor z
}
$$
Conversely, one associates to every morphism
$$
g \quad : \quad y \quad \morph{} \quad \rightdual{x}\cotensor z
$$
the morphism~$\psi_{x,y,z}(g)$ defined as the composite
$$
\xymatrix @-1pc {
x\tensor y\ar[rr]^-{g}
&&
x\tensor (\rightdual{x}\cotensor z)
\ar[rr]^-{\distL}
&&
(x\tensor \rightdual{x})\cotensor z
\ar[rrr]^-{\distributiverightcut{x}}
&&&
\unitcot\cotensor z
\ar[rr]^-{\rhocot}
&&
z
}
$$
%\section{Preliminaries}\label{section/parametric-monad}
%
The coherence properties of the linearly distributive category~$\Ccategory$
and of the right duality $x\mapsto\rightdual{x}$ imply together
that the correspondence is one-to-one and natural in~$y$ and~$z$.
%
This establishes the property.
%
Note that the unit~$\eta_x$ and counit~$\varepsilon_x$
of the adjunction are equal to the composite morphisms:
$$
\begin{array}{c}
\xymatrix @-1pc {
\eta_x & : & 
y\ar[rr]^-{(\lambdat)^{-1}}
&&
\unitt\tensor y\ar[rrr]^-{\distributiverightaxiom{x}}
&&&
(\rightdual{x}\cotensor x) \tensor y
\ar[rr]^-{\distR}
&&
\rightdual{x}\cotensor (x \tensor y)
}
\\
\xymatrix @-1pc {
\varepsilon_x
&:&
x\tensor (\rightdual{x}\cotensor y)
\ar[rr]^-{\distL}
&&
(x\tensor \rightdual{x})\cotensor y
\ar[rrr]^-{\distributiverightcut{x}}
&&&
\unitcot\cotensor y
\ar[rr]^-{\rhocot}
&&
y
}
\end{array}
$$
%aaaaa
%\medbreak
%
%\noindent
%A linearly distributive category~$\Ccategory$ is called symmetric
%when its monoidal structure $(\Ccategory,\tensor,1)$ is equipped
%with a symmetry.
%%
%An immediate but important corollary of Proposition~\ref{proposition/main-result-linearly-distributive-categories}
%is that
%%
%\begin{corollary}
%The notion of $\ast$-autonomous category coincides with the notion
%of symmetric linearly distributive category~$\Ccategory$ with a right duality.
%\end{corollary}


\subsection{Left dualities in linearly distributive categories}\label{section/left-dualities}
%
A remarkable feature of the notion of linearly distributive category 
is  that it is invariant under symmetry in the following sense:
given a linearly distributive category~$\Ccategory$, 
the category~$\Ccategory^{\, op(0)}$ obtained by reversing the orientation
of the tensor~$\tensor$ and cotensor~$\cotensor$ products 
is also linearly distributive.
%
This enables to define a left duality~$x\mapsto\leftdual{x}$ in a linearly distributive category~$\Ccategory$
as a right duality in the linearly distributive category~$\Ccategory^{\, op(0)}$.
%
The definition may be expanded in the following way.
%
A left duality consists of a family of morphisms
$$
\distributiveleftaxiom{x}:\unitt\morph{}x\cotensor\leftdual{x}
\quad\quad\quad
\distributiveleftcut{x}:\leftdual{x}\tensor x\morph{}\unitcot
$$
parametrized by the objects~$x$ of the category~$\Ccategory$,
and making the two diagrams below commute:
\begin{equation}\label{equation/left-axiom-coherence-for-linearly-distributive-categories}
\begin{tabular}{ccc}
$\vcenter{\xymatrix @-.1pc {
\unitt\tensor x
\ar[dd]_-{\lambdat}
\ar[rr]^-{\distributiveleftaxiom{x}\,\tensor \, x}
&&
(x\cotensor \leftdual{x})\tensor x
\ar[d]^-{\distR}
\\
&&
x\cotensor (\leftdual{x}\tensor x)
\ar[d]^-{x\cotensor\distributiveleftcut{x}}
\\
x
&&
x\cotensor\unitcot
\ar[ll]_-{\rhocot}
}}$
& \hspace{1em} &
$
\vcenter{\xymatrix @-.1pc {
\leftdual{x}\tensor \unitt
\ar[rr]^-{\leftdual{x}\,\tensor\,\distributiveleftaxiom{x}}
&&
\leftdual{x}\tensor(x\cotensor\leftdual{x})
\ar[d]^-{\distL}
\\
&&
(\leftdual{x}\tensor x)\cotensor\leftdual{x}
\ar[d]^-{\distributiveleftcut{x}\cotensor \leftdual{x}}
\\
\leftdual{x}
\ar[uu]^-{\rhot}
\ar[rr]^-{\lambdacot}
&&
\unitcot\cotensor\leftdual{x}
}}$
\end{tabular}
\end{equation}
%
The following statement is a direct consequence of Proposition~\ref{proposition/main-result-linearly-distributive-categories}
%and~\ref{proposition/main-result-linearly-distributive-categories-on-the-right}
when applied to the corresponding right duality in~$\Ccategory^{\, op(0)}$.
%
\begin{proposition}\label{proposition/main-result-linearly-distributive-categories-on-the-left}
In any linearly distributive category~$\Ccategory$ with a left duality,
\begin{itemize}
\item the functor $(-\tensor x)$ is left adjoint to the functor $(-\cotensor\leftdual{x})$
\item the functor $(y\cotensor -)$ is right adjoint to the functor $(\leftdual{y}\tensor -)$
\end{itemize}
for all objects $x,y$ of the category.
%
In particular, every such category~$\Ccategory$ is monoidal closed on the right,
with implication $y \, \rightpop  x$ defined as $y \, \cotensor \, \leftdual{x}$.
%
%Moreover, the left duality defines a monoidal functor
%$$
%\leftdual{(-)} \quad : \quad
%(\Ccategory,\cotensor,\unitcot)^{\,op(0,1)} \quad \morph{} \quad (\Ccategory,\tensor,\unitt)
%$$
%with coercion isomorphisms $\leftdual{(x\cotensor y)} \cong \leftdual{y}\tensor \leftdual{x}$
%and $\leftdual{\unitcot} \cong \unitt$.
%$$
%$$
%\leftdual{(x\cotensor y)} \cong \leftdual{y}\tensor \leftdual{x} 
%\quad\quad\quad\quad
%\leftdual{\unitcot} \cong \unitt.
%$$
\end{proposition}
%
This leads to the following key property which justifies the very definition
of linearly distributive category:
\begin{proposition}[Cockett-Seely]
\label{proposition/main-result-linearly-distributive-categories-on-both-sides}
Every linearly distributive category~$\Ccategory$ equipped with a right duality
and a left duality is $\ast$-autonomous with negation functors defined as 
$$
x\leftpop\bot = \rightdual{x}\cotensor\unitcot
\quad\quad\quad\quad
\bot\rightpop x = \unitcot\cotensor\leftdual{x}
$$
%In particular, any such linearly distributive category~$\Ccategory$
%inducing a monoidal equivalence
%with a left duality~$x\mapsto\leftdual{x}$
%and a right duality~$x\mapsto\rightdual{x}$
%defines a monoidal equivalence
%$$
%\xymatrix @-1.8pc {
%(\Ccategory,\tensor,\unitt)
%&\ar@/^1.2pc/[rrrrrrrr]^{\rightcomplementary{(-)}}
%\ar@{}[rrrrrrrr]|-{\begin{tiny}
%\begin{array}{c}
%monoidal
%\\
%equivalence
%\end{array}
%\end{tiny}}
%&&&&
%&&&&
%\ar@/^1.2pc/[llllllll]^{\leftcomplementary{(-)}}
%&
%(\Ccategory,\cotensor,\unitcot)^{\,op(0,1)}}
%$$
%which equips the category~$\Ccategory$ with the structure of a $\ast$-autonomous category.
\end{proposition}
%
In fact, it may be established that a symmetric $\ast$-autonomous category
is essentially the same thing as a symmetric linearly distributive category
equipped with a right duality, see \S\ref{section/conclusion} for a discussion.

\subsection{Monoidality of right duality}\label{section/monoidality-of-right-duality}
%
This section is mainly technical.
%
We establish that every right duality defines a monoidal functor
(and not just a functor) from the underlying linearly distributive category~$\Ccategory$
equipped with~$\tensor$ to its opposite category equipped with~$\cotensor$.
%
This property will play an important role in our later comparison
(in \S\ref{section/linearly-distributive-chiralities-comparison})
with the notion of right duality in a linearly distributive chirality.
%
Suppose given such a right duality in a linearly distributive category~$\Ccategory$.
%
We know by Proposition~\ref{proposition/main-result-linearly-distributive-categories}
that the right duality associates to every pair of objects~$x$ and~$y$
a pair of adjunctions
$$
\xymatrix @-1.8pc {
\Ccategory
&\ar@/^1.2pc/[rrrrrrrr]^{y\tensor -}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{\rightdual{y}\cotensor-}
&
\Ccategory
&\ar@/^1.2pc/[rrrrrrrr]^{x\tensor -}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{\rightdual{x}\cotensor-}
&
\Ccategory
}
$$
which may be then composed into an adjunction
$$
x\tensor (y\tensor -) \quad \dashv \quad \rightcomplementary{y}\cotensor(\rightcomplementary{x}\cotensor-)
$$
%
Composing with associativity on both sides induces the adjunction
$$
(x\tensor y)\tensor - \quad \dashv \quad (\rightcomplementary{y}\cotensor\rightcomplementary{x})\cotensor-
$$
which may be then compared with the adjunction associated
by the right duality to the object~$x\tensor y$:
$$
(x\tensor y)\tensor - \quad \dashv \quad \rightcomplementary{(x\tensor y)}\cotensor -
$$
%
by Proposition~\ref{proposition/main-result-linearly-distributive-categories} again.
%
The uniqueness of a right adjoint modulo isomorphism implies 
the existence of a family of isomorphisms
$$
\theta_{x,y,z} \quad : \quad (\rightdual{y}\cotensor\rightdual{x})\cotensor z
\hspace{.2em} \morph{} \hspace{.2em}
\rightdual{(x\tensor y)}\cotensor z
$$
natural in~$z$, defined as the composite morphism
$$
\xymatrix @-.6pc {
\rightdual{(x\tensor y)}\cotensor ((x\tensor y)\tensor
((\rightdual{y}\cotensor\rightdual{x})\cotensor z))
\ar[rr]^-{\alphat,\,\alphacot}
&&
\rightdual{(x\tensor y)}\cotensor (x\tensor (y\tensor
(\rightdual{y}\cotensor(\rightdual{x}\cotensor z))))
\ar[d]^-{\varepsilon_{y}}
\\
&&
\rightdual{(x\tensor y)}\cotensor (x\tensor (\rightdual{x}\cotensor z))
\ar[d]^-{\varepsilon_{x}}
\\
(\rightdual{y}\cotensor\rightdual{x})\cotensor z
\ar[uu]^-{\eta_{x\tensor y}}
\ar[rr]^-{\theta_{x,y,z}}
&&
\rightdual{(x\tensor y)}\cotensor z
}
$$
In the same way, one deduces from the adjunction
$(\, \unitt\tensor - \dashv \rightdual{\unitt}\cotensor -\,)$
the existence of a natural isomorphism
$$
\theta_{z}  \quad : \quad z
\hspace{.2em} \morph{} \hspace{.2em}
\rightdual{\unitt}\cotensor z
$$
defined as the composite
$$
\xymatrix{
z\ar[r]^-{\eta_{\unitt}}
&
\rightdual{\unitt}\cotensor(\unitt\tensor z)
\ar[r]^-{\lambdat}
&
\rightdual{\unitt}\cotensor z.
}
$$
From this follows the existence of two families of isomorphisms
\begin{equation}\label{equation/monoidal-coercions}
\tilde{\theta}_{x,y}:
\rightdual{y}\cotensor\rightdual{x}\morph{} \rightdual{(x\tensor y)}
\quad\quad\quad\quad
\tilde{\theta}_{\unitt}:\unitcot\morph{}\rightdual{\unitt} 
\end{equation}
defined by instantiating $z$ as $\bot$ in both cases.
%from~$\theta_{x,y,\unitcot}$ and from $\theta_{\unitcot}$
%in the expected way.
%
It is not difficult to check that
\begin{proposition}\label{proposition/right-duality-is-monoidal}
In a linearly distributive category~$\Ccategory$, the right duality functor
equipped with the coercion maps~(\ref{equation/monoidal-coercions})
defines a monoidal functor
$$
\rightdual{(-)} \quad : \quad
(\Ccategory,\tensor,\unitt) \quad \morph{} \quad (\Ccategory,\cotensor,\unitcot)^{\,op(0,1)}.
$$
\end{proposition}
One checks moreover that the two coercion maps~$\tilde{\theta}$ 
make the four diagrams below
$$
\xymatrix @-1.7pc {
\rightdual{y}\cotensor(\unitt\tensor y)
\ar[rrrrr]^-{\distributiverightaxiom{x}}
&&&&&
\rightdual{y}\cotensor((\rightdual{x}\cotensor x) \tensor y)
\ar[rrrr]^-{\distR}
&&&&
\rightdual{y}\cotensor (\rightdual{x}\cotensor (x \tensor y))
\ar[dd]^-{\alphacot}
\\
\\
\rightdual{y}\cotensor y
\ar[uu]^-{(\lambdat)^{-1}}
&&&&&
&&&&
(\rightdual{y}\cotensor\rightdual{x})\cotensor (x \tensor y)
\ar[dd]^{\tilde{\theta}_{x,y}}
\\
\\
\unitt
\ar[uu]^-{\distributiverightaxiom{y}}
\ar[rrrrrrrrr]^-{\distributiverightaxiom{x\tensor y}}
&&&&&&&&&
\rightdual{(x\tensor y)}\cotensor (x\tensor y)
}
$$
$$
\xymatrix @-1.7pc {
x\tensor (y\tensor(\rightdual{y}\cotensor\rightdual{x}))
\ar[rrrr]^-{\distL}
&&&&
x\tensor ((y\tensor\rightdual{y})\cotensor\rightdual{x})
\ar[rrrrr]^-{\distributiverightcut{y}}
&&&&&
x\tensor (\unitcot\cotensor\rightdual{x})
\ar[dd]^-{(\lambdacot)^{-1}}
\\
\\
(x\tensor y)\tensor(\rightdual{y}\cotensor\rightdual{x})
\ar[uu]^-{\alphat}
&&&&
&&&&&
x\tensor \rightdual{x}
\ar[dd]^-{\distributiverightcut{x}}
\\
\\
(x\tensor y)\tensor\rightdual{(x\tensor y)}
\ar[uu]^-{\tilde{\theta}^{-1}_{x,y}}
\ar[rrrrrrrrr]^-{\distributiverightcut{x\tensor y}}
&&&&&&&&&
\unitcot
}
$$
%as well as the diagrams
$$
\vcenter{\xymatrix @-.1pc {
\rightdual{\unitt}\cotensor\unitt
\ar[rrr]^-{\tilde{\theta}_{\unitt}} 
&&&
\unitcot\cotensor\unitt
\ar[d]^-{(\lambdacot)^{-1}}
\\
\unitt
\ar[u]^-{\distributiverightaxiom{\unitt}}
\ar[rrr]^-{id}
&&&
\unitt
}}
\quad\quad\quad\quad
\vcenter{\xymatrix @-.1pc {
\unitt\tensor\unitcot
\ar[rrr]^-{\tilde{\theta}_{\unitt}} 
&&&
\unitt\tensor\rightdual{\unitt}
\ar[d]^-{\distributiverightcut{\unitt}}
\\
\unitcot
\ar[u]^-{(\lambdat)^{-1}}
\ar[rrr]^-{id}
&&&
\unitcot
}}
$$
commute for all objects~$x,y$ of the linearly distributive category~$\Ccategory$.
%
These four diagrams will also be used in our later comparison with
the notion of right duality in linearly distributive chiralities.
%
%\subsection{Left dualities}
%A left duality is defined as 
%
%\begin{definition}[left dualities]
%A left duality in a linearly distributive category~$\Ccategory$ consists of the following data:
%\begin{itemize}
%\item an object $\leftdual{x}$,
%\item two morphisms
%$\distributiverightaxiom{x}:\unitt\morph{}x\cotensor\leftdual{x}$
%and
%$\distributiverightcut{x}:\leftdual{x}\tensor x\morph{}\unitcot$
%\end{itemize}
%for every object $x$ of the category~$\Ccategory$.
%%
%The morphisms are moreover required to make the diagrams
%\begin{equation}\label{equation/left-axiom-coherence-for-linearly-distributive-categories}
%\begin{tabular}{ccc}
%$
%\vcenter{\xymatrix @-.1pc {
%x\tensor \unitt
%\ar[dd]_-{\rhot}
%\ar[rr]^-{x\,\tensor\,\distributiverightaxiom{}}
%&&
%x\tensor(\rightdual{x}\cotensor x)
%\ar[d]^-{\distL}
%\\
%&&
%(x\tensor\rightdual{x})\cotensor x
%\ar[d]^-{\distributiverightcut{}\cotensor x}
%\\
%x
%&&
%\unitcot\cotensor x
%\ar[ll]_-{\lambdacot}
%}}$
%& \hspace{1em} &
%$\vcenter{\xymatrix @-.1pc {
%\unitt\tensor\rightdual{x}
%\ar[dd]_-{\lambdat}
%\ar[rr]^-{\distributiverightaxiom{}\,\tensor\,\rightdual{x}}
%&&
%(\rightdual{x}\cotensor x)\tensor\rightdual{x}
%\ar[d]^-{\distR}
%\\
%&&
%\rightdual{x}\cotensor (x\tensor\rightdual{x})
%\ar[d]^-{\rightdual{x}\cotensor\distributiverightcut{}}
%\\
%\rightdual{x}
%&&
%\rightdual{x}\cotensor\unitcot
%\ar[ll]_-{\rhocot}
%}}$
%\end{tabular}
%\end{equation}
%commute.
%%
%\end{definition}


\section{Dialogue chiralities}\label{section/dialogue-chiralities}
%
We start the section by recalling in \S\ref{section/dialogue-chiralities-original-definition}
the two-sided formulation as so-called \emph{dialogue chiralities}
of the elementary notion of dialogue category.
%
We then investigate a series of equivalent formulations of dialogue chiralities,
either based on a family of adjunctions in \S\ref{section/dialogue-chirality-by-adjunctions}
or on a family of transjunctions in \S\ref{section/dialogue-chirality-by-transjunctions}.
%
Meanwhile, we recall in \S\ref{section/transjunctions} the notion of transjunction
introduced by the author in~\cite{mellies:tensorial-logic-3} 
together with their pictorial representation in string diagrams.
%
%

\subsection{Dialogue chiralities on the left}\label{section/dialogue-chiralities-original-definition}
We start from the original definition of dialogue chiralities given in~\cite{mellies:tensorial-logic-2}
which we slightly alter by replacing the monoidal equivalence~(\ref{equation/negation-as-equivalence})
by the appropriate monoidal functor~(\ref{proposition/main-proposition}).
%
This innocuous change in the original definition is mainly justified by
the slick formulation of our main result (Proposition~\ref{proposition/main-proposition}) established 
in~\S\ref{section/linearly-distributive-chirality/main-theorem}.
%\begin{equation}\label{equation/dialogue-categories-monoidal-equivalence}
%\xymatrix @-1.8pc {
%\Acategory
%&\ar@/^1.2pc/[rrrrrrrr]^{\rightcomplementary{(-)}}
%\ar@{}[rrrrrrrr]|-{\begin{tiny}
%\begin{array}{c}
%monoidal
%\\
%equivalence
%\end{array}
%\end{tiny}}
%&&&&
%&&&&
%\ar@/^1.2pc/[llllllll]^{\leftcomplementary{(-)}}
%&
%\Bcategory^{\, op(0,1)}}
%\end{equation}
%by a monoidal functor.
%
\begin{definition}[dialogue chiralities]
A dialogue chirality on the left is defined as a pair of monoidal categories
$$
(\Acategory,\tensorialand,\tensorialtrue)
\quad \quad\quad \quad
(\Bcategory,\tensorialor,\tensorialfalse)
$$
equipped with an adjunction
\begin{equation}\label{equation/dialogue-categories-adjunction-main}
\xymatrix @-1.9pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory
}
\end{equation}
whose unit and counit are denoted as
$$\eta\hspace{.5em} :\hspace{.5em} Id \hspace{.5em} \morph{} \hspace{.5em} R\circ L
\quad\quad\quad\quad
\varepsilon \hspace{.5em} : \hspace{.5em} L\circ R \hspace{.5em} \morph{}  \hspace{.5em}Id$$
together with a monoidal functor
\begin{equation}\label{equation/dialogue-categories-monoidal-functor}
\rightcomplementary{(-)}
\quad : \quad
\Acategory
\quad \morph{} \quad 
\Bcategory^{\, op(0,1)}
\end{equation}
and a family of bijections
$$
\currify{m}{a}{b} \quad : \quad \distributor{m\tensorialand a}{b}
\quad \morph{} \quad \distributor{a}{\rightcomplementary{m}\tensorialor b}
$$
natural in $m$, $a$, $b$, which we call \emph{currification} in honor of the logician Haskell Curry.
%
Here, the bracket~$\distributor{a}{b}$ denotes the set of morphisms from~$a$ to $R(b)$ in the category~$\Acategory$:
$$
\distributor{a}{b} \quad = \quad \dialoguedistributor{a}{b}.
$$
%
The family~$\currifyalone$ is moreover required to make the diagram
\begin{equation}\label{equation/coherence/currify-one}
\vcenter{\xymatrix @-1pc {
\distributor{(m\tensorialand n)\tensorialand a}{b}
\ar[rrrr]^-{\currifyone{m\tensorialand n}} \ar[ddd]|-{associativity}
&&&& 
\distributor{a}{\rightcomplementary{(m\tensorialand n)}\tensorialor b}
\\
\\
\\
\distributor{m\tensorialand (n\tensorialand a)}{b}
\ar[rr]^-{\currifyone{m}}
&&
\distributor{n\tensorialand a}{\rightcomplementary{m}\tensorialor b}
\ar[rr]^-{\currifyone{n}}
&&
\distributor{a}{{\rightcomplementary{n}}\tensorialor({\rightcomplementary{m}}\tensorialor b)}
\ar[uuu]|-{\begin{tiny}\begin{array}{c}associativity\\ monoidality\ of\ negation\end{array}\end{tiny}}
}}
\end{equation}
commute for all objects~$a,m,n$ of the category~$\Acategory$,
and all objects~$b$ of the category~$\Bcategory$.
\end{definition}

\subsection{A formulation based on adjunctions}\label{section/dialogue-chirality-by-adjunctions}
%
A preliminary step towards the algebraic presentation of dialogue chiralities
performed in \S\ref{section/linearly-distributive-chirality} is to replace
the currification isomorphism~$\currifyalone$ by a family of adjunctions,
in the following way.
%
\begin{proposition}\label{proposition/dialogue-chirality-by-adjunctions}
A dialogue chirality on the left is the same thing as a pair of monoidal categories~$(\Acategory,\tensorialand,\tensorialtrue)$
and~$(\Bcategory,\tensorialor,\tensorialfalse)$
equipped with an adjunction~(\ref{equation/dialogue-categories-adjunction-main})
and a monoidal functor~(\ref{equation/dialogue-categories-monoidal-functor})
together with an adjunction
%
\begin{equation}\label{equation/family-of-adjunctions}
\leftadjoint{(m\tensorialand -)}\quad\dashv\quad\rightadjoint{(\rightcomplementary{m}\tensorialor -)}
\end{equation}
%
for every object~$m$ of the category~$\Acategory$, whose unit and counit are denoted
$$
\parametricunit{m} \, : \, a \, \morph{} \, \rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand a))
\quad\quad\quad
\parametriccounit{m} \, : \, \leftadjoint(m\tensorialand\rightadjoint(\rightcomplementary{m}\tensorialor b)) \, \morph{} \,  b
$$
The family~$\parametricunit{-}$ is moreover required to be natural and monoidal,
this meaning that the diagrams below
\begin{equation}\label{equation/family-of-adjunctions-naturality}
\vcenter{\xymatrix @-1.5pc {
&&&
\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand a))
\ar@/^1.4pc/[rdd]^-{f}
\\
\\
a
\ar@/^1.4pc/[rrruu]^-{\parametricunit{m}}
\ar@/_1.4pc/[rrrdd]_-{\parametricunit{n}}
&&&&
\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint(n\tensorialand a))
\\
\\
&&&
\rightadjoint(\rightcomplementary{n}\tensorialor\leftadjoint(n\tensorialand a))
\ar@/_1.4pc/[ruu]_-{\rightcomplementary{f}}
}}
\end{equation}
\begin{equation}\label{equation/family-of-adjunctions-monoidality}
\vcenter{\xymatrix @-1.6pc {
a 
\ar[rr]^-{\parametricunit{m\tensorialand n}} 
\ar[dd]_-{\parametricunit{n}}
&& 
\rightadjoint(\rightcomplementary{(m\tensorialand n)}\tensorialor\leftadjoint((m\tensorialand n)\tensorialand a))
\ar[dddd]|-{\begin{tiny}\begin{array}{c}associativity\,\& \\ monoidality\ of\ negation\end{array}\end{tiny}}
\\
\\
\rightadjoint(\rightcomplementary{n}\tensorialor\leftadjoint(n\tensorialand a))
\ar[dd]_-{\parametricunit{m}}
\\
\\
\rightadjoint(\rightcomplementary{n}\tensorialor\leftadjoint\rightadjoint
(\rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand (n\tensorialand a))))
\ar[rr]^-{\varepsilon}
&&
\rightadjoint(\rightcomplementary{n}\tensorialor ( \rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand (n\tensorialand a))))
}}
\end{equation}
should commute for all objects~$a,m,n$ and all morphisms~$f:m\to n$ of the category~$\Acategory$.
\end{proposition}

\paragraph{Remark.}
%
The family of adjunctions~(\ref{equation/family-of-adjunctions}) instantiated
at the unit~$\tensorialtrue$ induces an adjunction~$L\dashv R$
between the functors~$L$ and~$R$, whose unit and counit are defined as
the expected families of morphisms
$$
\begin{array}{c}
\xymatrix @-1.6pc {
\eta'_a & : & a & \ar[rrrr]^-{\parametricunit{\tensorialtrue}} &&&& 
&\rightadjoint(\rightcomplementary{\tensorialtrue}\tensorialor\leftadjoint{(\tensorialtrue\tensorialand a)})&
\ar[rrrrrr]^-{\begin{tiny}\begin{array}{c}associativity\\ \&\,monoidality\end{array}\end{tiny}} &&&&&& 
&\rightadjoint\leftadjoint{(a)}}
\\
\xymatrix @-1.6pc {
\varepsilon'_b & : 
&\leftadjoint\rightadjoint{(b)}&
\ar[rrrrrr]^-{\begin{tiny}\begin{array}{c}associativity\\ \&\,monoidality\end{array}\end{tiny}} &&&&&& 
&\leftadjoint(\tensorialtrue\tensorialand\rightadjoint{(\rightcomplementary{\tensorialtrue}\tensorialor b)}) &
\ar[rrrr]^-{\parametriccounit{\tensorialtrue}} &&&& 
& b
}
\end{array}$$
%
An important question is to understand whether this adjunction necessarily coincides
with the original adjunction~(\ref{equation/dialogue-categories-adjunction})
between~$L$ and~$R$.
%
The answer is positive.
%
Indeed, it is not difficult to see that the coherence diagram~(\ref{equation/family-of-adjunctions-monoidality})
implies that the two adjunctions coincide in the sense that $\eta=\eta'$ and $\varepsilon=\varepsilon'$.
%
The main idea is to instantiate the coherence diagram~(\ref{equation/family-of-adjunctions-monoidality})
with $m=n=\tensorialunit$, and to apply the coherence laws of the monoidal categories~$\Acategory$
and~$\Bcategory$ in order to show that the diagram
$$
\xymatrix @-.8pc {
a\ar[rrrr]^-{\eta'} \ar[d]_-{\eta'}
&&&& 
\rightadjoint\leftadjoint a
\ar@{=}[dd]
\\
\rightadjoint\leftadjoint a
\ar[d]_-{\eta'}
\\
\rightadjoint\leftadjoint \rightadjoint\leftadjoint  a
\ar[rrrr]^-{\varepsilon}
&&&&
\rightadjoint\leftadjoint a
}
$$
commutes.
%
It easily follows from this and from the properties of adjunctions
that $\eta=\eta'$ and $\varepsilon'=\varepsilon$.
%
This means in particular that the coherence diagram
\begin{equation}\label{equation/coherence-diagram-for-units-not-necessary}
\vcenter{\xymatrix @-.9pc{
\rightadjoint(\rightcomplementary{\tensorialtrue}\tensorialor\leftadjoint{(\tensorialtrue\tensorialand a)})
\ar[rrrr]^-{monoidality}
&&&&
\rightadjoint(\tensorialfalse\tensorialor\leftadjoint{(\tensorialtrue\tensorialand a)})
\ar[dd]^-{associativity}
\\
\\
a
\ar[rrrr]^{\eta}
\ar[uu]^{\parametricunit{\tensorialtrue}}
&&&&
\rightadjoint\leftadjoint(a)
}}
\end{equation}
is a consequence of the two coherence diagrams~(\ref{equation/family-of-adjunctions-naturality})
and~(\ref{equation/family-of-adjunctions-monoidality}) formulated 
in the statement of Proposition~\ref{proposition/dialogue-chirality-by-adjunctions}.

\paragraph{Remark.}
Once established that the adjunction~$(L,R,\eta',\varepsilon')$ coincides with
the adjunction~$(L,R,\eta,\varepsilon)$, it is not difficult to deduce from
their companion diagrams~(\ref{equation/family-of-adjunctions-naturality}) 
and~(\ref{equation/family-of-adjunctions-monoidality}) that the two coherence diagrams
$$
\xymatrix @-1.2pc {
&
\leftadjoint(n\tensorialand\rightadjoint(\rightcomplementary{n}\tensorialor b)) 
\ar@/^1.3pc/[rrrdd]^-{\parametriccounit{n}}
\\
\\
\leftadjoint(m\tensorialand\rightadjoint(\rightcomplementary{n}\tensorialor b)) 
\ar@/^1.3pc/[ruu]^-{f}
\ar@/_1.3pc/[rdd]_-{\rightcomplementary{f}}
&&&&
b
\\
\\
&
\leftadjoint(m\tensorialand\rightadjoint(\rightcomplementary{m}\tensorialor b))
\ar@/_1.3pc/[rrruu]_-{\parametriccounit{m}}
}
$$
$$\vcenter{\xymatrix @-1.4pc {
\leftadjoint(m\tensorialand (n\tensorialand\rightadjoint(\rightcomplementary{n}\tensorialor(\rightcomplementary{m}\tensorialor b))))
\ar[rr]^-{\eta}
\ar[dddd]|-{\begin{tiny}\begin{array}{c}associativity\,\& \\ monoidality\ of\ negation\end{array}\end{tiny}}
&&
\leftadjoint(m\tensorialand RL(n\tensorialand\rightadjoint(\rightcomplementary{n}\tensorialor(\rightcomplementary{m}\tensorialor b))))
\ar[dd]^-{\parametriccounit{n}}
\\
\\
&&
\leftadjoint(m\tensorialand\rightadjoint(\rightcomplementary{m}\tensorialor b)) 
\ar[dd]^-{\parametriccounit{m}}
\\
\\
\leftadjoint((m\tensorialand n)\tensorialand\rightadjoint(\rightcomplementary{(m\tensorialand n)}\tensorialor b)) 
\ar[rr]^-{\parametriccounit{m\tensorialand n}}
&&
b
}}
$$
commute for all object~$b$ of the category~$\Bcategory$
and all objects~$m,n$ and all morphisms $f:m\to n$ of the category~$\Acategory$.
%
At this point, it is worth mentioning that there is an element of choice
in the definition of dialogue chiralities formulated in Proposition~\ref{proposition/dialogue-chirality-by-adjunctions}
since the two coherence diagrams for~$\parametriccounit{-}$ may very well
replace the two corresponding diagrams~(\ref{equation/family-of-adjunctions-naturality}) 
and~(\ref{equation/family-of-adjunctions-monoidality}) for $\parametricunit{-}$.

\subsection{A formulation based on transjunctions}\label{section/dialogue-chirality-by-transjunctions}
The formulation of dialogue chiralities described in~\S\ref{section/dialogue-chirality-by-adjunctions}
is fine, but may be marginally improved.
%
The idea is to replace the original combinators~$\parametricunit{-}$ and~$\parametriccounit{-}$
presenting the adjunctions by somewhat simpler combinators inspired by proof-theory:
$$
\begin{array}{c}
\xymatrix @-1.6pc {
\axiom{m} & : & \leftadjoint(a) & \ar[rrrr] &&&&
& \rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand a)}
\\
\xymatrix @-1.6pc {
\cut{m} & : 
&
m\tensorialand \rightadjoint (\rightcomplementary{m}\tensorialor b)
&
\ar[rrrr] &&&&
& \rightadjoint (b)
}
\end{array}$$
This pair of combinators is defined from~$\parametricunit{-}$ and~$\parametriccounit{-}$
in the following way:
$$
\begin{array}{c}
\xymatrix @-1.6pc {
\axiom{m} & : & 
\leftadjoint(a)
& 
\ar[rrrr]^-{\parametricunit{m}} 
&&&&&
\leftadjoint\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand a)})
&
\ar[rrr]^-{\varepsilon}
&&&&
\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand a)}}
\\
\xymatrix @-1.6pc {
\cut{m} & : 
&
m\tensorialand \rightadjoint (\rightcomplementary{m}\tensorialor b)
&
\ar[rrr]^-{\eta} &&&
& 
\rightadjoint\leftadjoint (m\tensorialand\rightadjoint (\rightcomplementary{m}\tensorialor b)) &
\ar[rrrr]^-{\parametriccounit{m}} &&&& 
& \rightadjoint (b)
}
\end{array}$$
%
Conversely, the combinators~$\parametricunit{-}$ and $\parametriccounit{-}$
may be recovered from the original combinators~$\axiom{-}$ and $\cut{-}$ in the following way:
$$
\begin{array}{c}
\xymatrix @-1.55pc {
\parametricunit{m} & : & a & \ar[rrr]^-{\eta} &&& 
&\rightadjoint\leftadjoint(a) &
\ar[rrrrr]^-{\axiom{m}} &&&&&
&\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand a)})}
\\
\xymatrix @-1.55pc {
\parametriccounit{m} & : 
&
\leftadjoint(m\tensorialand \rightadjoint (\rightcomplementary{m}\tensorialor b))
&
\ar[rrrrr]^-{\cut{m}} &&&&&
&\leftadjoint\rightadjoint(b) &
\ar[rrr]^-{\varepsilon} &&&
& b
}
\end{array}$$
%
It is immediate that this back-and-forth translation between
the pair $\parametricunit{-}$, $\parametriccounit{-}$ and
the pair $\axiom{-}$, $\cut{-}$ defines a one-to-one relationship
between the two pairs of combinators.
%
%
This idea leads to an alternative formulation of dialogue chiralities,
based this time on the transjunction between the two functors
$$
m \,\tensorialand\, - \hspace{.5em} : \hspace{.5em}
\Acategory \hspace{.5em}  \morph{} \hspace{.5em}  \Acategory
\quad\quad\quad\quad
\rightcomplementary{m}  \,\tensorialor\, - \hspace{.5em} : \hspace{.5em}
\Bcategory\hspace{.5em}  \morph{} \hspace{.5em} \Bcategory$$
along the adjunction~$L\dashv R$ between~$\Acategory$ and~$\Bcategory$.
%
The reader unaware of the notion of transjunction will find the notion
recalled in~\S\ref{section/transjunctions}.
%The notion of transjunction was introduced by the author in~\cite{mellies:tensorial-logic-3}.
%
One main reason for introducing this notion is that it
enables to replace the original combinators $\parametricunit{-}$
and $\parametriccounit{-}$ by the logically flavoured combinators~$\axiom{-}$ and $\cut{-}$.
%
\begin{proposition}\label{proposition/dialogue-chirality-by-transjunctions}
A dialogue chirality on the left may be alternatively defined as
a pair of categories~$(\Acategory,\tensorialand,\tensorialtrue)$
and~$(\Bcategory,\tensorialor,\tensorialfalse)$
equipped with an adjunction~(\ref{equation/dialogue-categories-adjunction-main})
and a monoidal functor~(\ref{equation/dialogue-categories-monoidal-functor})
together with a family of transjunctions
$$
\axiom{m} \, : \, \leftadjoint(a) \, \morph{} \, \rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand a)
\quad\quad\quad
\cut{m} \, : \, m\tensorialand \rightadjoint(\rightcomplementary{m}\tensorialor b) \, \morph{} \,  \rightadjoint(b)
$$
natural in~$b$ and~$m$.
%
The family~$\cut{-}$ is moreover required to be natural and monoidal,
in the sense that the two diagrams
\begin{equation}\label{equation/family-of-transjunctions-naturality}
\vcenter{\xymatrix @-1.4pc {
&&
m\tensorialand \rightadjoint(\rightcomplementary{m}\tensorialor b)
\ar@/^1.3pc/[rrrdd]^-{\cut{m}}
\\
\\
m\tensorialand \rightadjoint(\rightcomplementary{n}\tensorialor b)
\ar@/^1.3pc/[rruu]^-{\rightcomplementary{f}}
\ar@/_1.3pc/[rrdd]_-{f}
&&&&&
\rightadjoint{(b)}
\\
\\
&&
n\tensorialand \rightadjoint(\rightcomplementary{n}\tensorialor b)
\ar@/_1.3pc/[rrruu]_-{\cut{n}}
}}
\end{equation}
\begin{equation}\label{equation/family-of-transjunctions-monoidality}
\vcenter{\xymatrix @-1pc {
m\tensorialand (n \tensorialand \rightadjoint(\rightcomplementary{n}\tensorialor (\rightcomplementary{m}\tensorialor b)))
\ar[rrrrrr]^-{\cut{n}}
&&&&&&
m\tensorialand \rightadjoint(\rightcomplementary{m}\tensorialor b)
\ar[dddd]^-{\cut{m}}
\\
\\
(m\tensorialand n) \tensorialand \rightadjoint((\rightcomplementary{n}\tensorialor \rightcomplementary{m})\tensorialor b)
\ar[uu]^-{associativity}
&&&&&&
\\
\\
(m\tensorialand n) \tensorialand \rightadjoint(\rightcomplementary{(m\tensorialand n)}\tensorialor b)
\ar[uu]^-{monoidality}
\ar[rrrrrr]^-{\cut{m\tensorialand n}}
&&&&&&
\rightadjoint{(b)}
}}
\end{equation}
commute for all objects~$a,m,n$ and morphisms $f:m\to n$ of the category~$\Acategory$.
\end{proposition}

\paragraph{Remark.}
In the same way as in the definition of dialogue chiralities based
on adjunctions in \S\ref{section/dialogue-chirality-by-adjunctions},
the coherence diagram
\begin{equation}\label{equation/family-of-transjunctions-unit}
\vcenter{\xymatrix @-.5pc{
\rightadjoint{(b)}
\ar[rrrr]^-{id}
&&&&
\rightadjoint{(b)}
\\
\\
\tensorialtrue\tensorialand\rightadjoint{(\rightcomplementary{\tensorialtrue}\tensorialor b)}
\ar[rrrr]^-{monoidality}
\ar[uu]^-{\cut{\tensorialtrue}}
&&&&
\tensorialtrue\tensorialand\rightadjoint{(\tensorialfalse\tensorialor b)}
\ar[uu]_-{associativity}
}}
\end{equation}
%
follows from the coherence diagrams~(\ref{equation/family-of-transjunctions-naturality})
and~(\ref{equation/family-of-transjunctions-monoidality}).
%
Moreover, one can easily check that in the same way as in \S\ref{section/dialogue-chirality-by-adjunctions},
the two coherence diagrams for the combinator~$\cut{-}$  are equivalent
to the corresponding coherence diagrams for~$\axiom{-}$ below:
$$
\xymatrix @-1.4pc {
&&&
\rightcomplementary{m}
\tensorialor
\leftadjoint{(m\tensorialand a)}
\ar@/^1.3pc/[rrdd]^-{f}
\\
\\
\leftadjoint{(a)}
\ar@/^1.3pc/[rrruu]^-{\axiom{m}\,\,}
\ar@/_1.3pc/[rrrdd]_-{\axiom{n}\,\,}
&&&&&
\rightcomplementary{m}
\tensorialor
\leftadjoint{(n\tensorialand a)}
\\
\\
&&&
\rightcomplementary{n}\tensorialor
\leftadjoint{(n\tensorialand a)}
\ar@/_1.3pc/[rruu]_-{\rightcomplementary{f}}
}
$$
\begin{equation}\label{equation/tensorial-eta-expansion-diagram}
\vcenter{\xymatrix @-1.2pc {
\rightcomplementary{n}\tensorialor
\leftadjoint{(n\tensorialand a)}
\ar[rrrrrr]^-{\axiom{m}}
&&&&&&
\rightcomplementary{n}\tensorialor(\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand (n\tensorialand a))})
\ar[dd]^-{associativity}
\\
\\
&&&&&&
(\rightcomplementary{n}\tensorialor\rightcomplementary{m})\tensorialor\leftadjoint{((m\tensorialand n)\tensorialand a)}
\ar[dd]^-{monoidality}
\\
\\
\leftadjoint{a}
\ar[uuuu]^-{\axiom{n}}
\ar[rrrrrr]^-{\axiom{m\tensorialand n}}
&&&&&&
\rightcomplementary{(m\tensorialand n)}\tensorialor\leftadjoint{((m\tensorialand n)\tensorialand a)}
}}
\end{equation}
%
Note that the coherence diagram
\begin{equation}\label{equation/tensorial-eta-expansion-diagram-unit}
\vcenter{\xymatrix @-.8pc{
\rightcomplementary{\tensorialtrue}\tensorialor\leftadjoint{(\tensorialtrue\tensorialand a)}
\ar[rrrr]^-{monoidality}
&&&&
\tensorialfalse\tensorialor\leftadjoint{(\tensorialtrue\tensorialand a)}
\ar[dd]^-{associativity}
\\
\\
\leftadjoint{(a)}
\ar[rrrr]^{id}
\ar[uu]^{\axiom{\tensorialtrue}}
&&&&
\leftadjoint{(a)}
}}
\end{equation}
also follows from the coherence diagrams~(\ref{equation/family-of-transjunctions-naturality})
and~(\ref{equation/family-of-transjunctions-monoidality}).
%commute for all objects~$a,m,n$ and all morphisms~$f:m\to n$ of the category~$\Acategory$
%and all objects~$b$ of the category~$\Bcategory$.




\subsection{Transjunctions}\label{section/transjunctions}
%
The notion of transjunction was introduced in~\cite{mellies:tensorial-logic-3}
in order to reflect the structure of negation in dialogue categories.
%
%Applying the translation to the triangular equations of adjunctions
%leads to the notion of transjunction.
\begin{definition}[transjunction]\label{definition/transjunction}
Suppose given a pair of adjunctions
$$
\begin{array}{ccc}
\vcenter{\xymatrix @-1.9pc {
\Acategory_1
&\ar@/^1.2pc/[rrrrrrrr]^{L_1}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R_1}
&
\Bcategory_1}}
& \quad\quad\quad &
\vcenter{\xymatrix @-1.9pc {
\Acategory_2
&\ar@/^1.2pc/[rrrrrrrr]^{L_2}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R_2}
&
\Bcategory_2}}
\end{array}
$$
whose units and counits are denoted~$\eta_1,\eta_2$ and $\varepsilon_1,\varepsilon_2$
respectively.
%
A transjunction~$F\dashv G$ between a pair of functors
$$
F : \Acategory_1 \to \Acategory_2
\quad\quad\quad
G : \Bcategory_2 \to \Bcategory_1
$$
accross the adjunctions~$L_1\dashv R_1$ and $L_2\dashv R_2$
is defined as a pair of natural transformations
$$
\mathbf{axiom} :  L_1 \Rightarrow G\circ L_2\circ F
\quad\quad\quad\quad
\mathbf{cut} : F\circ R_1\circ G \Rightarrow R_2
$$
making the two diagrams
\begin{equation}\label{equation/coherence-diagrams-for-transjunctions}
\vcenter{\xymatrix @-1.4pc {
F\circ R_1\circ L_1
\ar@{=>}[rrr]^-{\mathbf{axiom}}
\ar@{}[rrrdd]|-{(a)}
&&&
F\circ R_1\circ G \circ L_2 \circ F
\ar@{=>}[dd]^-{\mathbf{cut}}
\\
\\
F
\ar@{=>}[uu]^-{\eta_1}
\ar@{=>}[rrr]^-{\eta_2}
&&&
R_2\circ L_2\circ F
}}
\hspace{.6em}
\vcenter{\xymatrix @-1.4pc {
G\circ L_2 \circ F \circ R_1 \circ G
\ar@{=>}[rrr]^-{\mathbf{cut}}
\ar@{}[rrrdd]|-{(b)}
&&&
G\circ L_2\circ R_2
\ar@{=>}[dd]^-{\varepsilon_2}
\\
\\
L_1\circ R_1 \circ G
\ar@{=>}[uu]^-{\mathbf{axiom}}
\ar@{=>}[rrr]^-{\varepsilon_1}
&&&
G
}}
\end{equation}
commute.
\end{definition}
%
This notion of transjunction is ultimately justified by the following statement.
%
\begin{proposition}\label{equation/transjunction-as-adjunction}
A transjunction $F\dashv G$ accross the adjunctions~$L_1\dashv R_1$ and $L_2\dashv R_2$
is the same thing as an adjunction $F\circ L_1\dashv R_2\circ G$.
\end{proposition}
%
The two equations $(a)$ and $(b)$ may be alternatively depicted as string diagrams living 
in the 2-category~$\Cat$ of categories, functors and natural transformations.
%
First of all, the generators~$\mathbf{axiom}$ and~$\mathbf{cut}$
of a transjunction $F\dashv G$ accross the adjunctions~$L_1\dashv R_1$
and~$L_2\dashv R_2$ mentioned in Definition~\ref{definition/transjunction}
are depicted as follows:
\begin{center}
\begin{tabular}{ccccc}
\raisebox{22mm}{$\mathbf{axiom}=$}
&
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-link.pdf}
&
\quad\quad\quad
&
\raisebox{22mm}{$\mathbf{cut}=$}
&
\includegraphics[height=50mm]{dessins/axiom-cut/cut-link.pdf}
\end{tabular}
\end{center}
The two commutative diagrams~$(a)$ and $(b)$
are then depicted as follows:
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=55mm]{dessins/axiom-cut/axiom-cut-1-a.pdf}
&
\hspace{2em} \raisebox{25mm}{\Large{$\stackrel{(a)}{=}$}} \hspace{2em}
&
\includegraphics[height=55mm]{dessins/axiom-cut/axiom-cut-1-b.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=55mm]{dessins/axiom-cut/axiom-cut-2-a.pdf}
&
\hspace{2em} \raisebox{25mm}{\Large{$\stackrel{(b)}{=}$}} \hspace{2em}
&
\includegraphics[height=55mm]{dessins/axiom-cut/axiom-cut-2-b.pdf}
\end{tabular}
\end{center}
%%\subsection{Transjunction homomorphism}
A notion of homorphism between transjunctions may be then introduced,
this giving rise to a category of transjunctions.
%
\begin{definition}[homomorphism]
A homomorphism between two transjunctions $F\dashv G$ and $F'\dashv G'$
accross the same pair of adjunctions~$L_1\dashv R_1$ and~$L_2\dashv R_2$ 
is defined as a pair of natural transformations
$$
f\quad : \quad F\quad \Rightarrow \quad F'
\quad\quad\quad\quad
g\quad : \quad G'\quad \Rightarrow \quad G
$$
making the two diagrams
$$
\begin{array}{ccc}
\xymatrix @-1pc {
G\circ L_2\circ F
\ar@{=>}[rrr]^-{f} 
\ar@{}[rrrdd]|-{(a)}
&&& G\circ L_2\circ F'
\\
\\
L_1\ar@{=>}[uu]^-{\mathbf{axiom}} 
\ar@{=>}[rrr]^-{\mathbf{axiom'}} 
&&& G'\circ L_2\circ F'\ar@{=>}[uu]_-{g}
}
&
\quad
&
\xymatrix @-1pc {
F'\circ R_1\circ G'
\ar@{=>}[rrr]^-{\mathbf{cut'}}
\ar@{}[rrrdd]|-{(b)}
&&& 
R_2
\\
\\
F\circ R_1\circ G'
\ar@{=>}[uu]^-{f}
\ar@{=>}[rrr]^-{g}
&&& 
F\circ R_1\circ G
\ar@{=>}[uu]_-{\mathbf{cut}}
}
\end{array}
$$
commute.
\end{definition}
%
Pictorially, such a homomorphism~$(f,g)$ is defined as a pair
of natural transformations~$f:F\Rightarrow F'$ and
$g:G'\Rightarrow G$ satisfying the diagrammatic equalities below:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=45mm]{dessins/axiom-cut/two-cell-1-a.pdf}
&
\hspace{2em} \raisebox{20mm}{\Large{$\stackrel{}{=}$}} \hspace{2em}
&
\includegraphics[height=45mm]{dessins/axiom-cut/two-cell-1-b.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=45mm]{dessins/axiom-cut/two-cell-2-a.pdf}
&
\hspace{2em} \raisebox{20mm}{\Large{$\stackrel{}{=}$}} \hspace{2em}
&
\includegraphics[height=45mm]{dessins/axiom-cut/two-cell-2-b.pdf}
\end{tabular}
\end{center}


%We conclude the section in \S\ref{section/eta-equalities} by pointing out
%how the formulation of dialogue chiralities based on transjunctions
%recovers and refines the familiar axiom-cut and $\tensor$-$\llpar$ cut-elimination
%rules of multiplicative proof-nets in linear logic, as well as their $\eta$-expansion rules
%for axiom links.

\section{Tensorial proof-nets vs. multiplicative proof-nets}\label{section/proof-nets}
%Tensorial conjunction vs. disjunction}\label{section/eta-equalities}
%
The guiding philosophy of our work in tensorial logic is to transfer
the traditional constructions of linear logic to this more primitive situation,
where negation is not required to be involutive anymore.
%
Although it may not be entirely obvious to the reader at this stage,
the solution for the axiom-cut equation of linear logic appears
(although somewhat secretly!) 
in the two previous sections~\S\ref{section/dialogue-chirality-by-transjunctions}
and~\S\ref{section/transjunctions}.
%
Indeed, putting Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}
together with Definition~\ref{definition/transjunction},
it appears that the two coherence diagrams~(\ref{equation/coherence-diagrams-for-transjunctions})
required of a transjunction should be instantiated as follows in the definition of a dialogue chirality:
$$
\vcenter{\xymatrix @-.4pc {
m\tensorialand RL \, a
\ar[rr]^-{\axiom{m}}
\ar@{}[rrdd]|-{(a)}
&&
m\tensorialand R(\rightcomplementary{m}\tensorialor L(m\tensorialand a))
\ar[dd]^-{\cut{m}}
\\
\\
m\tensorialand a
\ar[uu]^-{\eta}
\ar[rr]_-{\eta}
&&
RL(m\tensorialand a)
}}
$$
$$
\vcenter{\xymatrix @-.4pc {
\rightcomplementary{m}\tensorialor L( m \tensorialand R (\rightcomplementary{m}\tensorialor b))
\ar[rr]^-{\cut{m}}
\ar@{}[rrdd]|-{(b)}
&&
\rightcomplementary{m}\tensorialor LRb
\ar[dd]^-{\varepsilon}
\\
\\
L R (\rightcomplementary{m}\tensorialor b)
\ar[uu]^-{\axiom{m}}
\ar[rr]_-{\varepsilon}
&&
\rightcomplementary{m}\tensorialor b
}}
$$
%
These diagrams are required to commute for all objects~$m,a$
of the category~$\Acategory$ and all objects~$b$ of the category~$\Bcategory$.
%
The coherence diagram~$(a)$ is depicted in the following way in string diagrams:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=55mm]{dessins/axiom-cut/tensorial-axiom-cut-1-a.pdf}
&
\hspace{1em} \raisebox{25mm}{\Large{$\stackrel{(a)}{=}$}} \hspace{1em}
&
\includegraphics[height=55mm]{dessins/axiom-cut/tensorial-axiom-cut-1-b.pdf}
\end{tabular}
\end{center}
%
while its companion diagram~$(b)$ is depicted as its mirror image:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=55mm]{dessins/axiom-cut/tensorial-axiom-cut-2-a.pdf}
&
\hspace{1em} \raisebox{25mm}{\Large{$\stackrel{(b)}{=}$}} \hspace{1em}
&
\includegraphics[height=55mm]{dessins/axiom-cut/tensorial-axiom-cut-2-b.pdf}
\end{tabular}
\end{center}
%
Here, an important methodological point is that the two equations~$(a)$ and~$(b)$
refine the traditional axiom-cut annihilation equation of linear logic,
and integrate in it the non involutive pair of negation functors~$L$ and~$R$.
%
Indeed, in the particular case of a $\ast$-autonomous category~$\Ccategory$,
where the two sides~$\Acategory$ and~$\Bcategory$ of the dialogue chirality
coincide with~$\Ccategory$, and the two functors~$R$ and~$L$ are defined
as the identity functor, the family of transjunctions defining the 
$\ast$-autonomous category in Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}
boils down to a family of adjunctions 
\begin{equation}\label{equation/linear-logic/family-of-adjunction}
m\tensor -  \quad \dashv \quad \rightcomplementary{m}\llpar -
\quad \quad : \quad \quad \Ccategory \quad \morph{} \quad \Ccategory
\end{equation}
in the usual sense, with unit and counit defined as
$$
\axiom{m} \, : \, a \, \morph{} \, \rightcomplementary{m}\llpar (m\tensor a)
\quad\quad\quad\quad
\cut{m} \, : \, m\tensor (\rightcomplementary{m}\llpar b) \, \morph{} \,  b.
$$
Note that the equations~$(a)$ and~$(b)$ are replaced in that case
by the familiar triangular laws of the adjunction:
$$
\vcenter{\xymatrix @-1pc {
&
m\tensor (\rightcomplementary{m}\llpar (m\tensor a))
\ar[rdd]^-{\cut{m}}
\ar@{}[dd]|-{(a)}
&
\\
\\
m\tensor a
\ar[ruu]^-{\axiom{m}\,\,\, }
\ar[rr]_-{id}
&&
m\tensor a
}}
\hspace{1em}
\vcenter{\xymatrix @-1pc {
& \rightcomplementary{m}\llpar ( m \tensor (\rightcomplementary{m}\llpar b))
\ar[rdd]^-{\cut{m}}
\ar@{}[dd]|-{(b)}
\\
\\
\rightcomplementary{m}\llpar b
\ar[ruu]^-{\axiom{m}\,\,\, }
\ar[rr]_-{id}
&&
\rightcomplementary{m}\llpar b
}}
$$
which are required to commute for all objects~$m,a$ of the category~$\Acategory$
and all objects~$b$ of the category~$\Bcategory$.
%
One recovers in this way the familiar axiom-cut annihilation
of multiplicative proof-nets in linear logic, turned upside-down
and formulated in the algebraic language of string diagrams:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=53mm]{dessins/axiom-cut/linear-axiom-cut-1-a.pdf}
&
\hspace{1em} \raisebox{25mm}{\Large{$\stackrel{(a)}{=}$}} \hspace{1em}
&
\includegraphics[height=53mm]{dessins/axiom-cut/linear-axiom-cut-1-b.pdf}
\end{tabular}
\end{center}
%
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=55mm]{dessins/axiom-cut/linear-axiom-cut-2-a.pdf}
&
\hspace{1em} \raisebox{25mm}{\Large{$\stackrel{(b)}{=}$}} \hspace{1em}
&
\includegraphics[height=55mm]{dessins/axiom-cut/linear-axiom-cut-2-b.pdf}
\end{tabular}
\end{center}
%
The purpose of each transjunction introduced in Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}
is thus to refine the basic adjunction of $\ast$-autonomous categories
in the presence of the explicit negation functors~$L$ and $R$ of dialogue chiralities.
%
Conversely, the axiom-cut annihilation of $\ast$-autonomous categories 
is obtained by ``depolarizing'' the dialogue chirality into a situation
where its two sides~$\Acategory$ and~$\Bcategory$ are equal, and the negation functors~$L$ and~$R$ disappear.

\medbreak 

\noindent

The refinement of linear logic into tensorial logic works surprisingly well
in the case of the axiom-cut annihilation.
%
One thus wonders whether the two other fundamental equations
of multiplicative proof nets --- namely the tensor-par and the $\mathbf{1}$-$\bot$
annihilation rules --- may be upgraded to tensorial logic in the same way.
%
The two equations~$(c)$ and~$(d)$ are recalled below as commutative diagrams.
%
As the reader will readily check, they express together 
that the family of adjunctions~(\ref{equation/linear-logic/family-of-adjunction})
is monoidal in its parameter~$m$.
%
$$
\vcenter{\xymatrix @-1.3pc {
m\tensor (n \tensor (\rightcomplementary{n}\llpar (\rightcomplementary{m}\llpar b))
\ar[rrrrrr]^-{\cut{n}}
&&&&&&
m\tensor (\rightcomplementary{m}\llpar b)
\ar[dddd]^-{\cut{m}}
\\
\\
(m\tensor n) \tensor ((\rightcomplementary{n}\llpar \rightcomplementary{m})\llpar b)
\ar[uu]^-{associativity}
&
\ar@{}[rrrr]|-{(c)}
&&&&&
\\
\\
(m\tensor n) \tensor (\rightcomplementary{(m\tensor n)}\llpar b)
\ar[uu]^-{monoidality}
\ar[rrrrrr]_-{\cut{m\tensorialand n}}
&&&&&&
b
}}
$$
$$\vcenter{\xymatrix @-.8pc{
b
\ar[rrrr]^-{id}
\ar@{}[rrrrdd]|-{(d)}
&&&&
b
\\
&&&&
\mathbf{1}\tensor b
\ar[u]_-{unit}
\\
\mathbf{1}\tensor (\rightcomplementary{\mathbf{1}}\llpar b)
\ar[rrrr]_-{monoidality}
\ar[uu]^-{\cut{\mathbf{1}}}
&&&&
\mathbf{1}\tensor 
(\bot\llpar b)
\ar[u]_-{unit}
}}
$$
These two equations~$(c)$ and~$(d)$ of linear logic are depicted below,
once again turned upside-down and formulated in the appropriate language of string diagrams.
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=45mm]{dessins/axiom-cut/linear-cut-tensor-cotensor-1.pdf}
&
\hspace{2em} \raisebox{18mm}{\Large{$\stackrel{(c)}{=}$}} \hspace{2em}
&
\includegraphics[height=45mm]{dessins/axiom-cut/linear-cut-tensor-cotensor-2.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=40mm]{dessins/axiom-cut/linear-cut-true-false-1.pdf}
&
\hspace{2em} \raisebox{17mm}{\Large{$\stackrel{(d)}{=}$}} \hspace{2em}
&
\includegraphics[height=40mm]{dessins/axiom-cut/linear-cut-true-false-2.pdf}
\end{tabular}
\end{center}
%
One benefit of the algebraic approach is to provide a nice and simple answer to this question
of upgrading~$(c)$ and~$(d)$ to tensorial logic.
%
We have already seen that the solution for adapting the axiom-cut annihilation equations~$(a)$ and~$(b)$
is entirely conveyed by the first part of Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}.
%
Similarly, it turns out that the second part of Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}
describes how to adapt the two equations~$(c)$ and~$(d)$ to tensorial logic.
%
The fact that the coherence diagrams~(\ref{equation/family-of-transjunctions-monoidality}) 
and~(\ref{equation/family-of-transjunctions-unit}) provide the expected solution
becomes apparent when one depicts them as string diagrams:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=50mm]{dessins/axiom-cut/cut-tensor-cotensor-1.pdf}
&
\hspace{2em} \raisebox{20mm}{\Large{$\stackrel{(c)}{=}$}} \hspace{2em}
&
\includegraphics[height=50mm]{dessins/axiom-cut/cut-tensor-cotensor-2.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=40mm]{dessins/axiom-cut/cut-true-false-1.pdf}
&
\hspace{2em} \raisebox{17mm}{\Large{$\stackrel{(d)}{=}$}} \hspace{2em}
&
\includegraphics[height=40mm]{dessins/axiom-cut/cut-true-false-2.pdf}
\end{tabular}
\end{center}
%
As in the case of the two diagrams~$(a)$ and~$(b)$, 
one recovers the two equations~$(c)$ and~$(d)$ of linear logic by ``depolarizing''
the corresponding equations of tensorial logic.
%
Diagrammatically speaking, depolarization amounts to replacing the blue area for~$\Acategory$ 
and the red area for~$\Bcategory$ by a unique brown area for~$\Ccategory$,
and by removing accordingly the separating frontiers~$L$ and~$R$ between~$\Acategory$ and~$\Bcategory$.
%, by turning in that way
%a dialogue chirality~$(\Acategory,\Bcategory)$ into a $\ast$-autonomous category~$\Ccategory$.
%

\medbreak

As already mentioned, a basic principle of dialogue chiralities
is that every coherence diagram comes with a mirror image.
%
A typical illustration is provided by diagram~$(a)$ whose mirror image
is diagram~$(b)$.
%
Similarly, the mirror image of the two diagrams~$(c)$ and~$(d)$ 
is provided by the coherence diagrams~(\ref{equation/tensorial-eta-expansion-diagram})
and~(\ref{equation/tensorial-eta-expansion-diagram-unit}) depicted below
as two equations~$(e)$ and~$(f)$ between string diagrams:
%
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-1.pdf}
&
\hspace{2em} \raisebox{20mm}{\Large{$\stackrel{(e)}{=}$}} \hspace{2em}
&
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-2.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=40mm]{dessins/axiom-cut/axiom-true-false-1.pdf}
&
\hspace{2em} \raisebox{17mm}{\Large{$\stackrel{(f)}{=}$}} \hspace{2em}
&
\includegraphics[height=40mm]{dessins/axiom-cut/axiom-true-false-2.pdf}
\end{tabular}
\end{center}
%
These diagrams refine the familiar $\eta$-expansion rule of multiplicative proof-nets
in linear logic, which may be recovered by ``depolarizing'' them in the expected way:
%to a situation where the two sides~$\Acategory$ and~$\Bcategory$ are equal,
%and where the functors~$L$ and~$R$ are equal to the identity.
%--- which we call here tensor-par creation equation.

\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=45mm]{dessins/axiom-cut/linear-axiom-tensor-cotensor-1.pdf}
&
\hspace{2em} \raisebox{17mm}{\Large{$\stackrel{(e)}{=}$}} \hspace{2em}
&
\includegraphics[height=45mm]{dessins/axiom-cut/linear-axiom-tensor-cotensor-2.pdf}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=35mm]{dessins/axiom-cut/linear-axiom-true-false-1.pdf}
&
\hspace{2em} \raisebox{15mm}{\Large{$\stackrel{(f)}{=}$}} \hspace{2em}
&
\includegraphics[height=35mm]{dessins/axiom-cut/linear-axiom-true-false-2.pdf}
\end{tabular}
\end{center}
%
This series of elementary observations leads to the idea that the general theory of proof-nets 
in linear logic can be adapted to a similar theory of proof-nets in tensorial logic.
%
A preliminary step in this programme is performed in~\cite{mellies:tensorial-logic-1}
where a notion of tensorial proof-net is introduced at the crossroad of linear logic
and game semantics.
%
In that respect, the depolarization of a tensorial proof-net deserves
the name of ``detemporalization'' or ``desequentialization'' since
it removes the flow of execution and time described by the functors~$R$ and~$L$
in order to recover a multiplicative proof-net of linear logic.

\section{Bimodulations}\label{section/bimodulations}
We recall the notion of \emph{bimodulation}
between two modulations (also called lax actions or parametric monads)
introduced in a previous paper on dialogue categories~\cite{mellies:tensorial-logic-3}.
%
%As was explained there, t
One main reason for introducing the notion of bimodulation
is that it unifies the two fundamental notions of \emph{monadic strength}
on the one hand, and of \emph{distributivity law} between monads
on the other hand.
%
We start by recalling the notions of modulation and of bimodulation
in~\S\ref{section/modulations} and in~\S\ref{section/bimodulations-between-modulations}.
%
The precise definition of a dialogue chirality on the right (rather than on the left)
is then formulated in~\S\ref{section/dialogue-chiralities-on-the-right}.
%
This leads us to \S\ref{section/illustration-of-bimodulation} where we illustrate
the notion of bimodulation with the example of the continuation bimodulation
associated to any such dialogue chirality.
% in every such dialogue chirality.
%

\subsection{Modulations}\label{section/modulations}
The notion of modulation enables us to parametrize a formal monad~$T$
in a 2-category~$\Wbicategory$ by a monoidal category~$(\INDEX,\tensor,\oneINDEX)$
in the expected way.
%
\begin{definition}[modulation]
A modulation in a 2-category~$\Wbicategory$
%in a category~$\Acategory$ parametrized
%by a monoidal category~$\INDEX$
is defined as a $0$-cell~$\Acategory$ equipped with a lax monoidal functor
$$(T,m):\INDEX\morph{}\Endofunctors{\Acategory}.$$
%
The monoidal category~$\INDEX$ is called the parameter category
of the $\INDEX$-modulation; and an object~$j$ of~$\INDEX$ is called a parameter.
%
%A parametric monad with parameter category~$\INDEX$
%is also called a $\INDEX$-monad for short.
\end{definition}
%
%
Hence, a $\INDEX$-modulation~$(T,m)$ consists of
\begin{itemize}
\item a $1$-cell $\, T_j \, : \, \Acategory \, \morph{} \, \Acategory$
for every parameter~$j$ and a $2$-cell $\, T_f \, : \, T_j \, \Rightarrow \, T_k$
for every morphism~$f:j\morph{}k$ between such parameters,
\item a $2$-cell $m_{\oneINDEX} \, : \,\IDCATa{} \, \Rightarrow \, T_{\oneINDEX}$
called the unit of the modulation,
\item a $2$-cell $\, m_{j,k} \, : \, T_{j}\circ T_{k}\, \Rightarrow\, T_{j\tensor k}$
called the $(j,k)$-component of the multiplication of the modulation, for every pair of parameters~$j$ and~$k$.
\end{itemize}
%
These data are moreover required to make a series of coherence diagrams
commute in the category~$\Endofunctors{\Acategory}$.
%
First, the diagrams
\begin{center}
\begin{tabular}{ccc}
$\vcenter{\xymatrix@-1pc{
&& T_k\ar@/^1pc/[rrd]^{T_g}
\\
T_j\ar@/^1pc/[rru]^{T_f}
\ar@/_1pc/[rrrr]_{T_{g\circ f}}
&&
&&
T_l
}}
$
&&
$\vcenter{\xymatrix{
T_j\ar@/^1pc/[rr]^{\id{T_j}}
\ar@/_1pc/[rr]_{T_{\id{j}}}
&&
T_j
}}
$
\end{tabular}
\end{center}
%
express the functoriality of~$T$;
then, the diagrams
%
\begin{center}
$\vcenter{\xymatrix@-.1pc{
T_j\circ T_k
\ar[rr]^{T_f\circ T_g}
\ar[d]_{m_{j,k}}
&&
T_{j'}\circ T_{k'}
\ar[d]^{m_{j',k'}}
\\
T_{j\tensor k}
\ar[rr]^{T_{f\tensor g}}
&&
T_{j'\tensor k'}
}}
$
\end{center}
express the naturality of~$m$;
and finally the diagrams
%
%\begin{equation}
%\label{equation/coherence-diagrams-monoidality}
$$
\vcenter{\xymatrix@-.5pc{
T_j\circ T_k\circ T_l
\ar[rrrr]^-{m_{j,k}\circ T_l}
\ar[dd]_-{T_j\circ m_{k,l}}
&&&&
T_{j\tensor k}\circ T_l
\ar[dd]^-{m_{j\tensor k,l}}
\\
\\
T_{j}\circ T_{k\tensor l}
\ar[rr]^-{m_{j,k\tensor l}}
&&
T_{j\tensor (k\tensor l)}
\ar[rr]^-{\alpha}
&&
T_{(j\tensor k)\tensor l}
}}
$$
and
$$
\vcenter{\xymatrix @-.5pc{
&&
T_{\oneINDEX}\circ T_j
\ar@/^1pc/[rrd]^{m_{\oneINDEX,j}}
&&
\\
T_j\ar[rrrr]|-{\id{T_j}}
\ar@/_1pc/[rrd]_{T_j\circ m_{\oneINDEX}}
\ar@/^1pc/[rru]^{m_{\oneINDEX}\circ T_j}
&&
&&
T_j
\\
&&
T_j\circ T_{\oneINDEX}
\ar@/_1pc/[rru]_{m_{j,\oneINDEX}}
}}
$$
%\end{equation}
express the monoidality of~$m$, for all indices~$j,j',k,k',l$
and morphisms~$f,g,h$ in the parameter category~$\INDEX$.
%
%Note that we have slightly simplified the last sequence
%~(\ref{equation/coherence-diagrams-monoidality})
%of coherence diagrams by supposing that the category~$\INDEX$ is
%strictly monoidal.
%
Note that a modulation~$T$ parametrized by the trivial monoidal category~$\mathbf{1}$
with exactly one object~$\ast$ and exactly one morphism (thus equal to the identity morphism
of $\ast$) is the same thing as a formal monad in the 2-category~$\Wbicategory$
in the sense of Street~\cite{street:formal-monad-theory}.

\subsection{Bimodulations between modulations}\label{section/bimodulations-between-modulations}
%
From now on, we suppose given a $0$-cell~$\Ccategory$ in a 2-category~$\Wbicategory$ 
equipped with a $\INDEX$-modulation
$$T = \bullet \quad : \quad \INDEX \quad \morph{} \quad \Endofunctors{\Ccategory}$$
and a $\Mcategory^{\, op(0)}$-modulation
$$S = \circ \quad : \quad \Mcategory^{\, op(0)} \quad \morph{} \quad \Endofunctors{\Ccategory}$$
with parameters taken in the monoidal categories~$(\Jcategory,\tensor,e)$ and~$(\Mcategory,\tensor,u)$.
%
\begin{definition}[bimodulation]
A bimodulation between the two modulations~$T=\bullet$ and~$S=\circ$ is defined as a natural transformation
$$
\kappa \quad : \quad S \, \circ \,  T \quad \Rightarrow \quad T \, \circ \, S \quad : \quad \Jcategory\times\Mcategory^{\, op(0)} \quad \morph{} \quad \Endofunctors{\Ccategory}
$$
%$$
%-\bullet (-\circ -) \quad \Rightarrow \quad (-\bullet -)\circ - \quad : \quad \Jcategory\times\Ccategory\times\Mcategory \quad \morph{} \quad \Ccategory
%$$
%family of morphisms
%$$
%\kappa_{i,m,A} \quad : \quad i\bullet (A\circ m) \quad \morph{} \quad (i\bullet A)\circ m
%$$
%natural in the object~$i$ of the category~$\Jcategory$, the object~$m$ of the category~$\Mcategory$
%and the object~$A$ of the category~$\Ccategory$.
making the four diagrams below commute
\begin{center}
\includegraphics[width=33em]{dessins/parametric-monad-distributivity-law/commutator-coherence-1-reverse.pdf}
\end{center}
\begin{center}
\includegraphics[width=33em]{dessins/parametric-monad-distributivity-law/commutator-coherence-2-reverse.pdf}
\end{center}
for all objects~$i,j$ of the category~$\Jcategory$
and all objects~$m,n$ of the category~$\Mcategory$.
\end{definition}

\paragraph{Remark.}
In the particular case when $\Wbicategory=\mathbf{Cat}$,
a bimodulation may be alternatively defined as a natural transformation
$$
\kappa \quad : \quad
(-\bullet -)\circ - \quad \Rightarrow \quad -\bullet (-\circ -) \quad : \quad \Jcategory\times\Ccategory\times\Mcategory \quad \morph{} \quad \Ccategory
$$
with components
$$
\kappa_{i,m,A} \quad : \quad (i\bullet  A)\circ m \quad \morph{} \quad i\bullet (A\circ m)
$$
parametrized by the objects~$i$ of the category~$\Jcategory$, $m$ of the category~$\Mcategory$ and
$A$ of the category~$\Ccategory$.
%
As such, the bimodulation~$\kappa$ may be seen as a lax version
of a $(\Jcategory,\Mcategory)$-bimodule.
%
This is represented in string diagrams by depicting the bimodulation~$\kappa$
as a braiding
%
$$
\includegraphics[width=13em]{dessins/parametric-monad-distributivity-law/distributivity-monad-parametric-braiding-reverse.pdf}
$$
commuting the string representing the modulation~$\bullet$ under the string representing the modulation~$\circ$.
%
The notation enables to depict the coherence diagrams of the bimodulation~$\kappa$
as a series of topologically intuitive equations, permuting the multiplication and unit
of a modulation under or over the string representing the other modulation.
%
Typically, the first series of equations in the definition of a bimodulation ``permutes''
the multiplication~$\mu_{\bullet}$ over the modulation~$\circ$
\begin{center}
\includegraphics[width=23em]{dessins/parametric-monad-distributivity-law/distributivity-monad-parametric-string-diagrams-1-a-reverse.pdf}
\end{center}
\begin{center}
\includegraphics[width=20em]{dessins/parametric-monad-distributivity-law/distributivity-monad-parametric-string-diagrams-1-b-reverse.pdf}
\end{center}
while the second series of equations ``permutes'' the multiplication~$\mu_{\circ}$
under the modulation~$\bullet$
\begin{center}
\includegraphics[width=23em]{dessins/parametric-monad-distributivity-law/distributivity-monad-parametric-string-diagrams-2-a-reverse.pdf}
\end{center}
\begin{center}
\includegraphics[width=21em]{dessins/parametric-monad-distributivity-law/distributivity-monad-parametric-string-diagrams-2-b-reverse.pdf}
\end{center}
%
\paragraph{Remark.} 
A comodulation parametrized by the monoidal category~$(\INDEX,\tensor,\oneINDEX)$
in a 2-category~$\Wbicategory$ is defined as a $\INDEX$-modulation in the 2-category~$\Wbicategory^{\,op(2)}$.
%
Here, the notation~$\Wbicategory^{\,op(2)}$ is for the 2-category obtained from~$\Wbicategory$
by reversing the orientation of its 2-cells.
%
Similarly, a bimodulation between comodulations is defined as a bimodulation
between the corresponding modulations in the 2-category~$\Wbicategory^{\,op(2)}$.
%
A notion of bimodulation between a modulation and a comodulation may be also 
introduced in order to generalize the notion of distributivity law between a monad and a comonad.

\subsection{Dialogue chiralities on the right}\label{section/dialogue-chiralities-on-the-right}
%
We have recalled in \S\ref{section/dialogue-chiralities} the original definition
of dialogue chirality as it appears in~\cite{mellies:tensorial-logic-2}.
%
However, it is mentioned in this paper
%in the very same paper~\cite{mellies:tensorial-logic-2}
that there is an element of choice in the definition of dialogue chirality.
%
In particular, if we call dialogue chirality \emph{on the left} the notion of dialogue chirality
recalled in \S\ref{section/dialogue-chiralities}, every dialogue category~$\Ccategory$
induces such a dialogue chirality, obtained by defining~$L$ and~$R$ as the negation functors
$$L : x \mapsto \bot\rightpop x
\quad\quad\quad\quad
R : x \mapsto x\leftpop \bot.
$$
On the other hand, the other choice of negation functors
$$L : x \mapsto x\leftpop \bot
\quad\quad\quad\quad
R : x \mapsto \bot\rightpop x
$$
induces a dialogue chirality \emph{on the right}.
%
The notion of dialogue chirality on the right
is a mirror image of the notion of dialogue chirality
\emph{on the left}.
%
\begin{definition}
A dialogue chirality on the right is defined as a pair of monoidal categories
$$
(\Acategory,\tensorialand,\tensorialtrue)
\quad \quad\quad \quad
(\Bcategory,\tensorialor,\tensorialfalse)
$$
equipped with a monoidal functor
$$
\xymatrix @-1.8pc {
\Acategory
&\ar[rrrrrrrr]^{\companionleftcomplementary{(-)}}
&&&&
&&&&
&
\Bcategory^{\, op(0,1)}}
$$
with an adjunction
%\begin{equation}\label{equation/dialogue-categories-monoidal-equivalence}
$$
\xymatrix @-1.9pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory
}
$$
%\end{equation}
%whose unit and counit are denoted as
%$$\eta\hspace{.5em} :\hspace{.5em} Id \hspace{.5em} \morph{} \hspace{.5em} R\circ L
%\quad\quad\quad\quad
%\varepsilon \hspace{.5em} : \hspace{.5em} L\circ R \hspace{.5em} \morph{}  \hspace{.5em}Id$$
and with a family of bijections
$$
\currify{m}{a}{b} \quad : \quad \distributor{a\tensorialand m}{b}
\quad \morph{} \quad \distributor{a}{b\tensorialor\companionleftcomplementary{m}}
$$
natural in $m$, $a$, $b$.
%
In the same way as in the case of a dialogue chirality on the left,
the bracket~$\distributor{a}{b}$ denotes the set of morphisms
from~$a$ to $R(b)$ in the category~$\Acategory$:
$$
\distributor{a}{b} \quad = \quad \dialoguedistributor{a}{b}.
$$
%
The family~$\currifyalone$ is moreover required to make the diagram
$$
\vcenter{\xymatrix @-1pc {
\distributor{a\tensorialand (m\tensorialand n)}{b}
\ar[rrrr]^-{\currifyone{m\tensorialand n}} \ar[ddd]|-{associativity}
&&&& 
\distributor{a}{b\tensorialor{\companionleftcomplementary{(m\tensorialand n)}}}
\\
\\
\\
\distributor{(a\tensorialand m) \tensorialand n}{b}
\ar[rr]^-{\currifyone{n}}
&&
\distributor{a\tensorialand m}{b\tensorialor {\companionleftcomplementary{n}}}
\ar[rr]^-{\currifyone{m}}
&&
\distributor{a}{(b\tensorialor {\companionleftcomplementary{n}})
\tensorialor{\companionleftcomplementary{m}}}
\ar[uuu]|-{\begin{tiny}\begin{array}{c}associativity\\ monoidality\ of\ negation\end{array}\end{tiny}}
}}
$$
commute for all objects~$a,m,n$ of the category~$\Acategory$,
and all objects~$b$ of the category~$\Bcategory$.
%
\end{definition}
%
Every dialogue chirality on the left induces a dialogue chirality
on the right (and conversely) by applying the involution
$$
\Acategory \mapsto \Bcategory^{\, op(0,1)}
\quad\quad\quad
\Bcategory \mapsto \Acategory^{\, op(0,1)}
\quad\quad\quad
L\mapsto R^{\, op(0,1)}
\quad\quad\quad
R\mapsto L^{\, op(0,1)}.
$$
See~\cite{mellies:tensorial-logic-2} for a discussion.
%
%
\subsection{The continuation bimodulation}\label{section/illustration-of-bimodulation}
%
An important reason for introducing the notion of bimodulation~\cite{mellies:tensorial-logic-3} 
is that every dialogue chirality (on the right) comes equipped with a bimodulation
$$\contau \quad : \quad S\, \circ \, T \quad \morph{}   \quad T\, \circ \,  S$$
between the modulations (also called lax actions or parametric monads)
$$
\begin{array}{ccccccccc}
T & \quad : \quad & (b,a) & \mapsto & R(b\tensorialor L(a)) & \quad : \quad & \Bcategory\times\Acategory & \morph{} & \Acategory
\\
S & \quad : \quad & (a,m) & \mapsto & a\tensorialand m & \quad : \quad & \Acategory\times\Acategory & \morph{} & \Acategory
\end{array}
$$
%
Symmetrically, every dialogue chirality (on the right) comes equipped with
a bimodulation
$$\distau \quad : \quad K\, \circ \, J \quad \morph{}   \quad J\, \circ \, K.$$
between the two comodulations (also called oplax actions or parametric comonads)
below:
$$
\begin{array}{ccccccccc}
J & \quad : \quad & (b,n) & \mapsto & b\tensorialor n & \quad : \quad & \Bcategory\times\Bcategory & \morph{} & \Bcategory
\\
K & \quad : \quad & (a,b) & \mapsto & L(a\tensorialand R(b)) & \quad : \quad & \Acategory\times\Bcategory & \morph{} & \Bcategory
\end{array}
$$
This pair of bimodulations will play a central role in the definition
of a linearly distributive chirality in the following section.

\section{Linearly distributive chiralities}\label{section/linearly-distributive-chirality}
%
At this point, we are ready to articulate the formal definition of linearly distributive chirality discussed in the introduction.
%
The reader will find it fully exposed in~\S\ref{section/linearly-distributive-chirality/definition}.
%
We then proceed by analogy with linearly distributive categories, and introduce 
in \S\ref{section/linearly-distributive-chirality/right-dualities}
a notion of right duality adapted to linearly distributive chiralities.
%
The main technical result of the paper appears in \S\ref{section/linearly-distributive-chirality/main-theorem}.
%
We establish there that every linearly distributive chirality equipped with a right duality
defines a dialogue chirality in the sense of \S\ref{section/dialogue-chiralities-original-definition}.
%
Finally, we conclude in \S\ref{section/linearly-distributive-chiralities-comparison}
by showing the notion of linearly distributive chirality (and of right duality)
coincides with the traditional notion of linearly distributive category (and of right duality)
in the ``depolarized'' case when the two sides~$\Acategory$ and~$\Bcategory$ of the chirality coincide,
and the two functors $L$ and $R$ are equal to the identity functor.
%which provides the key definition of the paper.

\subsection{Definition}\label{section/linearly-distributive-chirality/definition}
A \emph{linearly distributive chirality} is defined as a pair of monoidal categories
$$
(\Acategory,\tensorialand,\tensorialtrue)
\quad \quad\quad \quad
(\Bcategory,\tensorialor,\tensorialfalse)
$$
equipped with an adjunction
$$\xymatrix @-1.9pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory
}$$
together with two bimodulations
\begin{equation}\label{equation/bimonads}
\begin{array}{ccccc}
\contau
& \quad : \quad &
R(b\tensorialor L(a)) \tensorialand m
& \quad \morph{} \quad &
R(b\tensorialor L(a\tensorialand m))
\\
\distau & \quad : \quad &
L(a\tensorialand R(b\tensorialor n))
& \quad \morph{} \quad &
L(a\tensorialand R(b))\tensorialor n
\end{array}
\end{equation}
%Cela permet de garder la dualité à droite...
%
%\begin{equation}\label{equation/bimonads}
%\begin{array}{ccccc}
%\contau
%& \quad : \quad &
%m\tensorialand R(L(a)\tensorialor b)
%& \quad \morph{} \quad &
%R(L(m\tensorialand a)\tensorialor b)
%\\
%\distau & \quad : \quad &
%L(R(n\tensorialor b)\tensorialand a)
%& \quad \morph{} \quad &
%n\tensorialor L(R(b)\tensorialand a)
%\end{array}
%\end{equation}
between
\begin{itemize}
\item the $\Bcategory$-modulation~$T_{b}:a\mapsto R(L(b)\tensorialand a)$
and the $\Acategory$-modulation $S_m:a\mapsto a\tensorialand m$
on the category~$\Acategory$ in the case of $\contau$,
\item the $\Bcategory$-comodulation~$K_{n}:b\mapsto b\tensorialor n$
and the $\Acategory$-comodulation~$L_{a}:b\mapsto L(a\tensorialor R(b))$
on the category~$\Bcategory$ in the case of $\distau$.
\end{itemize}
%
According to the definition of a bimodulation, this means
that $2\times 4$ diagrams are required to commute.
%
We review them in turn.
%
First of all, the fact that~$\contau$ defines a bimodulation means that the four diagrams
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-conjunction-12.pdf}
\end{center}
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-conjunction-34.pdf}
\end{center}
commute for all objects~$a,m,n$ in~$\Acategory$ and $b,b_1,b_2$ in~$\Bcategory$.
%
Symmetrically, the fact that $\distau$ defines a bimodulation means that the four diagrams
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-disjunction-12.pdf}
\end{center}
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-disjunction-34.pdf}
\end{center}
commute for all objects~$a,a_1,a_2$ in~$\Acategory$ and $b,m,n$ in~$\Bcategory$.
%
Besides this series of eight commutative diagrams, we ask that the diagram
\begin{center}
\includegraphics[width=20em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-mysterious.pdf}
\end{center}
commutes for all objects~$a,m,n$ of the category~$\Acategory$ and all object~$b$ of the category~$\Bcategory$.
%
Symmetrically, we ask that its mirror image
\begin{center}
\includegraphics[width=20em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-distributivity-mysterious-reverse.pdf}
\end{center}
commutes for any object~$a$ of the category~$\Acategory$ and all objects~$b,m,n$ of the category~$\Bcategory$.
%

\medbreak

\noindent
In contrast to the eight other coherence diagrams 
which are prescribed by the two bimodulations~$\contau$ and~$\distau$
--- the algebraic nature of
these last two coherence diagrams remains somewhat mysterious 
at the current stage.
%
In particular, these two diagrams are not justified by the previous discussions
on bimodulations since their purpose is precisely to relate
the two bimodulations~$\contau$ and~$\distau$.
%
We know (see~\S\ref{section/illustration-of-bimodulation})
that every dialogue chirality on the right is equipped with two such bimodulations.
%
It is not difficult to check that these last two diagrams are also satisfied
by any dialogue chirality on the right.
%
From this follows that
%
\begin{proposition}
Every dialogue chirality on the right defines a linearly distributive chirality.
\end{proposition}

%This result provides a justification for the notion of linearly distributive chirality.

\subsection{Right duality in linearly distributive chiralities}\label{section/linearly-distributive-chirality/right-dualities}
A right duality in a linearly distributive chirality~$(\Acategory,\Bcategory)$
is defined as a monoidal functor
$$
\xymatrix @-1.8pc {
\Acategory
&\ar[rrrrrrrr]^{\rightcomplementary{(-)}}
&&&&
&&&&
&
\Bcategory^{\, op(0,1)}}
$$
%$$
%\xymatrix @-1.8pc {
%\Acategory
%&\ar@/^1.2pc/[rrrrrrrr]^{\rightcomplementary{(-)}}
%\ar@{}[rrrrrrrr]|-{\begin{tiny}
%\begin{array}{c}
%monoidal
%\\
%equivalence
%\end{array}
%\end{tiny}}
%&&&&
%&&&&
%\ar@/^1.2pc/[llllllll]^{\leftcomplementary{(-)}}
%&
%\Bcategory^{\, op(0,1)}}
%$$
thus equipped with natural isomorphisms
$$
\rightcomplementary{(a_1\tensorialand a_2)} \cong \rightcomplementary{a_2}\tensorialor \rightcomplementary{a_1}
\quad \quad \quad \quad \quad \quad 
\rightcomplementary{\tensorialtrue} \cong \tensorialfalse
$$
satisfying a series of coherence diagrams, together with two families of morphisms
$$
\AX{m} \quad : \quad \tensorialtrue \quad \morph{} \quad \rightadjoint \, ( \,  \rightcomplementary{m} \, \tensorialor \, \leftadjoint \, ( \, m \, ) \, )
$$
$$
\CUT{m} \quad : \quad \leftadjoint \, ( \,  m \, \tensorialand \,  \rightadjoint \, ( \, \rightcomplementary{m} \, ) \, ) 
\quad \morph{} \quad \tensorialfalse
$$
each of them parametrized by the objects~$m$ of the category~$\Acategory$.
%
These morphisms are required to make a series of $4\times 2$ coherence diagrams commute,
each of the four pairs consisting of a diagram and of its mirror image.
%
The first pair of diagrams adapts the usual triangular axiom of adjunctions
to the combinators~$\AX{-}$ and~$\CUT{-}$:
\begin{equation}\label{equation/right-duality-1a}
\raisebox{-4em}{\includegraphics[width=20em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-1-reverse.pdf}}
\end{equation}
%One also requires that the mirror image commutes:
\begin{equation}\label{equation/right-duality-1b}
\raisebox{-4em}{\includegraphics[width=20em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-1.pdf}}
\end{equation}
The second pair of coherence diagrams expresses
that the two combinators~$\AX{-}$ and $\CUT{-}$ are dinatural:
\begin{equation}\label{equation/right-duality-2a}
\raisebox{-4em}{\includegraphics[width=19em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-2.pdf}}
\end{equation}
%together with its mirror image:
\begin{equation}\label{equation/right-duality-2b}
\raisebox{-4em}{\includegraphics[width=19em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-2-reverse.pdf}}
\end{equation}
The third pair of coherence diagrams expresses 
that the combinators~$\AX{-}$ and~$\CUT{-}$ are monoidal:
\begin{equation}\label{equation/right-duality-3a}
\raisebox{-6em}{\includegraphics[width=25em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-3.pdf}}
\end{equation}
\begin{equation}\label{equation/right-duality-3b}
\raisebox{-6em}{\includegraphics[width=25em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-3-reverse.pdf}}
\end{equation}
The fourth and last pair of coherence diagrams expresses
that the combinators~$\AX{-}$ and~$\CUT{-}$ are monoidal,
this time with respect to the units:
\begin{equation}\label{equation/right-duality-4a}
\raisebox{-3em}{\includegraphics[width=28em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-4.pdf}}
\end{equation}
\begin{equation}\label{equation/right-duality-4b}
\raisebox{-3em}{\includegraphics[width=28em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-duality-4-reverse.pdf}}
\end{equation}
These diagrams are required to commute for all objects~$m,n$ and all morphisms~$f:m\to n$ of the category~$\Acategory$.
%


\subsection{Main statement}\label{section/linearly-distributive-chirality/main-theorem}
%
At this stage, we are ready to establish the main result of the paper
which states that 
\begin{proposition}\label{proposition/main-proposition}
Every linearly distributive chirality~$(\Acategory,\Bcategory)$
with a right duality defines a dialogue chirality on the left.
\end{proposition}
%
%
%
This statement provides a natural justification for the two notions of 
linearly distributive chirality and of right duality, which have been
carefully carved in order to establish the result.
%
%IThis is also the reason why we found convenient to slightly weaken
%the notion of dialogue chirality introduced in~\cite{mellies:tensorial-logic-2}
%
We start by establishing an important preliminary property:
\begin{proposition}\label{proposition/main-adjunction-of-the-right-duality}
%A dialogue chirality (on the left and on the right) is the same thing
%as a discursive pair equipped with a duality (on the left and on the right).
In a linearly distributive chirality~$(\Acategory,\Bcategory)$ equipped with a right duality,
the functor 
$$L(m\tensorialand -) \quad : \quad \Acategory \quad \morph{} \quad \Bcategory$$
is left adjoint to the functor
$$R(\rightcomplementary{m}\tensorialor -) \quad : \quad \Bcategory \quad \morph{} \quad \Acategory$$
for every object~$m$ of the category~$\Acategory$.
%
The family of adjunctions is moreover natural in the parameter~$m$.
\end{proposition}
\textbf{Proof.} We have seen in Proposition~\ref{equation/transjunction-as-adjunction}
that such an adjunction may be alternatively formulated as a transjunction
between~$m\tensorialand -$ and~$\rightcomplementary{m}\tensorialor -$
accross the adjunction~$L\dashv R$.
%
We find convenient to use this formulation here.
%
Hence, given a linearly distributive chirality with a right duality,
we introduce the two categorical combinators~$\axiom{-}$ and~$\cut{-}$
defined in such a way as to make the diagrams below commute:
$$
\xymatrix @-1pc {
\leftadjoint(\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint m)\tensorialand a)
\ar[rrrr]^{\contau}
&&&&
\leftadjoint\rightadjoint(\rightcomplementary{m}\tensorialor\leftadjoint (m\tensorialand a))
\ar[dd]^-{\varepsilon}
\\
\\
\leftadjoint(a) \ar[rrrr]^-{\axiom{m}} 
\ar[uu]^{\AX{m}}
&&&& 
\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand a)}
}
$$
$$
\xymatrix @-1pc {
\rightadjoint\leftadjoint(m\tensorialand\rightadjoint (\rightcomplementary{m}\tensorialor b))
\ar[rrrr]^-{\distau}
&&&&
\rightadjoint(\leftadjoint(m\tensorialand\rightadjoint (\rightcomplementary{m}))\tensorialor b)
\ar[dd]^-{\CUT{m}}
\\
\\
m\tensorialand \rightadjoint (\rightcomplementary{m}\tensorialor b)
\ar[rrrr]^-{\cut{m}}
\ar[uu]^-{\eta}
&&&&
\rightadjoint (b)
}
$$
Note that the very definition of the families~$\axiom{-}$ and~$\cut{-}$ 
ensures that they are natural in~$a$ and~$b$ respectively.
%
there remains to check that the two coherence diagrams~$(a)$ and~$(b)$
commute in~(\ref{equation/coherence-diagrams-for-transjunctions})
in order to establish that this pair of combinators defines a transjunction.
%
To that purpose, one constructs the diagram chase below
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-proof-diagram-3-preliminary.pdf}
\end{center}
completed by the following one:
\begin{center}
\includegraphics[width=30em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-proof-diagram-3-post.pdf}
\end{center}
%
This establishes that the coherence diagram~$(a)$
commutes in~(\ref{equation/coherence-diagrams-for-transjunctions}).
%
The fact that the other coherence diagram~$(b)$
commutes in~(\ref{equation/coherence-diagrams-for-transjunctions})
is proved in exactly the same way, by replacing each diagram chase
by its mirror image.
%
This proves that the pair of morphisms~$\axiom{m}$ and~$\cut{m}$ defines a transjunction,
and thus an adjunction between $L(m\tensorialand-)$ and $R(\rightcomplementary{m}\tensorialor-)$.
%
The fact that this family of adjunctions is natural in~$m$ boils down to the fact
that the family of combinators~$\axiom{-}$ and~$\cut{-}$ are dinatural in~$m$.
%
This last assertion follows from the very definition of these combinators
and from the requirement that
the coherence diagrams~(\ref{equation/right-duality-1a}) and~(\ref{equation/right-duality-1b})
commute in the definition of a right duality.
%
This concludes the proof of Proposition~\ref{proposition/main-adjunction-of-the-right-duality}.

\medbreak 

\noindent
\textbf{Proof of Proposition~\ref{proposition/main-proposition}.}
%
At this stage, there remains to establish the two additional facts required 
in the statement of Proposition~\ref{proposition/dialogue-chirality-by-transjunctions}.
%
This is achieved by the two diagram chases below, which establish that the family~$\axiom{-}$ is dinatural in~$m$:
\begin{center}
\includegraphics[width=130mm]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-proof-diagram-1.pdf}
\end{center}
and at the same time monoidal:
\begin{center}
\includegraphics[width=34em]{dessins/combinatorial-presentation-of-dialogue/discursive-pair-proof-diagram-2.pdf}
\end{center}
This concludes the proof that the family of transjunctions~$\axiom{-}$ and~$\cut{-}$ 
provides a dialogue chirality structure to the linearly distributive chirality~$(\Acategory,\Bcategory)$.
%

\paragraph{Remark.}
%
It may come as a surprise to the careful reader that only four of the $4\times 2$
coherence diagrams required of a right duality --- namely equations~(\ref{equation/right-duality-1a}), 
(\ref{equation/right-duality-1b}), (\ref{equation/right-duality-2a}) and (\ref{equation/right-duality-3a})
--- are used in the proof of Proposition~\ref{proposition/main-proposition}.
%
We keep the four other coherence diagrams in the definition of a right duality
because each of them 
% four coherence diagrams~(\ref{equation/right-duality-2b}), 
%(\ref{equation/right-duality-3b}), (\ref{equation/right-duality-4a}) and (\ref{equation/right-duality-4b})
makes perfect sense, either as the mirror image of another coherence diagram
--- in the case of (\ref{equation/right-duality-2b}) and (\ref{equation/right-duality-3b}) ---
or as the degenerate case for units of another coherence diagram
--- in the case of (\ref{equation/right-duality-4a}) and (\ref{equation/right-duality-4b}).
%
On the other hand, it follows from Proposition~\ref{proposition/main-proposition} that
the four coherence diagrams~(\ref{equation/right-duality-2b}), 
(\ref{equation/right-duality-3b}), (\ref{equation/right-duality-4a}) and (\ref{equation/right-duality-4b})
are automatically valid when the coherence diagrams~(\ref{equation/right-duality-1a}), 
(\ref{equation/right-duality-1b}), (\ref{equation/right-duality-2a}) and (\ref{equation/right-duality-3a})
hold in a linearly distributive chirality.
%The second reason is that it is not clear how to recover the four coherence diagrams
%~(\ref{equation/right-duality-2b}), (\ref{equation/right-duality-3b}), (\ref{equation/right-duality-4a})
%and (\ref{equation/right-duality-4b}) from 
%that the three other coherence diagrams --- in contrast
%to its counterpart diagram~(\ref{equation/coherence-diagram-for-units-not-necessary})
%in the definition of dialogue categories based on transjunctions.


\subsection{A comparison with linearly distributive categories}\label{section/linearly-distributive-chiralities-comparison}
%
According to the general philosophy of depolarization, we should recover the notions
of linearly distributive category (and of right duality) by depolarizing the corresponding notions
in tensorial logic.
In order to proceed with the comparison, we introduce the notion of depolarized linearly distributive chirality.
\begin{definition}
A linearly distributive chirality is called \emph{depolarized} when
its two sides $\Acategory$ and $\Bcategory$ are equal and when
the two functors~$L$ and~$R$ are identity functors.
\end{definition}
%
It is essentially immediate to check that
%
\begin{proposition}
A linearly distributive category is the same thing as a depolarized linearly distributive chirality.
% where $\Acategory=\Bcategory$ and where the two functors~$L$ and~$R$ are identity functors.
\end{proposition}
The proof is based on a direct comparison of the coherence diagrams
for linearly distributive category in~\S\ref{section/linearly-distributive-category/definition}
and for linearly distributive chirality in~\S\ref{section/linearly-distributive-chirality/definition}.
It is easy to show that there is a one-to-one relationship between them, where each diagram~\S\ref{section/linearly-distributive-category/definition}
is obtained by depolarizing the corresponding diagram in~\S\ref{section/linearly-distributive-chirality/definition}.

%
\medbreak


A somewhat less obvious statement is that
\begin{proposition}\label{proposition/depolarization-of-right-dualities}
The notion of right duality in a linearly distributive category coincides with the notion
of right duality in a depolarized linearly distributive chirality.
\end{proposition}
Suppose given a linear distributive category~$\Ccategory$ and 
the corresponding depolarized linearly distributive chirality~$(\Ccategory,\Ccategory)$.
%
The easy direction of the proof is to show that every right duality in the sense of~\S\ref{section/linearly-distributive-chirality/right-dualities}
for the chirality~$(\Ccategory,\Ccategory)$ defines a right duality in the sense of~\S\ref{section/monoidal/dualities}
for the category~$\Ccategory$.
%
The essential point to observe is that the two coherence diagrams~$(a)$ and~$(b)$ in Equation~(\ref{equation/right-axiom-coherence-for-linearly-distributive-categories})
are obtained by instantiating (or depolarizing) the coherence diagrams~(\ref{equation/right-duality-1a}) and (\ref{equation/right-duality-1b}).
%
The other direction is less obvious, but the argument has been heavily prepared
in \S\ref{section/monoidal/dualities} and \S\ref{section/monoidality-of-right-duality}.
%
Indeed, suppose given a right duality in the sense of~\S\ref{section/monoidal/dualities}
for the linearly distributive category~$\Ccategory$.
%
Then, we have established in~\S\ref{section/monoidal/dualities} and \S\ref{section/monoidality-of-right-duality}
that $\rightcomplementary{(-)}$ defines a monoidal functor, and that all the coherence diagrams
required by the definition of a right duality in the sense of~\S\ref{section/linearly-distributive-chirality/right-dualities}
commute.
%
This concludes the proof of Proposition~\ref{proposition/depolarization-of-right-dualities}.
%is less obvious, although not really difficult either.
%




%%
%One recovers the theorem by Cockett and Seely:

%\subsection{Illustration}\label{section/linearly-distributive-chirality/illustration}

%
\section{Concluding remarks}\label{section/conclusion}
%
Despite the work done in this paper, we are still halfway of the complete story.
%
The technical difficulty comes from the fact that we decided to investigate
the most primitive notion of dialogue category where
the tensor product~$\tensor$ is not equipped with any braiding or symmetry.
%
This lack of structure implies that there are two \emph{different} choices
of adjunctions~$L\dashv R$.
%
The first choice $L(x)=\bot\rightpop x$ and $R(x)=x\leftpop\bot$ induces a dialogue chirality
on the left (see \S\ref{section/dialogue-chiralities-original-definition})
whereas the second choice $L(x)=x\leftpop\bot$ and $R(x)=\bot\rightpop x$
induces a dialogue chirality on the right (see \S\ref{section/dialogue-chiralities-on-the-right}).
%
Although this distinction between left and right dialogue chiralities is legitimate
and even fundamental, it induces a subtle mismatch in the present paper:
\begin{itemize}
\item on the one hand, we observe (see~\S\ref{section/illustration-of-bimodulation})
that every dialogue chirality \emph{on the right} defines
a linearly distributive chirality \emph{on the right},
%is typically obtained for every 
%--- rather than by a dialogue chirality \emph{on the left}...
\item then, we establish in Proposition~\ref{proposition/main-proposition}
(see \S\ref{section/linearly-distributive-chirality/main-theorem})
that in the presence of a right duality, every such linearly distributive chirality \emph{on the right}
defines a dialogue chirality \emph{on the left} --- rather than a dialogue chirality \emph{on the right}
as we would have naively expected...
\end{itemize}
% 
This mismatch explains why we keep Proposition~\ref{proposition/main-proposition}
as unsatisfactory it stands, and do not try to establish that a dialogue chirality is \emph{the same thing}
as a linearly distributive chirality equipped with an appropriate notion of left or right duality.
%
The difference between left and right dialogue chiralities is fundamental,
and the project would necessarily fail...
%
A tentative solution would be to shift to an extended notion of dialogue category~$\Ccategory$
with a \emph{binary} rather than a \emph{unary} negation, equipped
with a two-sided version of currification
$$
\varphi_{m,x,n} \quad : \quad \Ccategory(m\tensor x \tensor n,\bot) \quad \cong \quad \Ccategory(x,m\leftpop \bot\rightpop n)
$$
%
The solution is nice and appealing, but we prefer to explore here
a more sophisticated one, based on the idea that the left and the right negations $x\leftpop\bot$
and $\bot\rightpop x$ should coincide up to isomorphism.
%
This track leads us to the notion of \emph{helical} dialogue category
where the two negations are related by a natural isomorphism
$$
\mathbf{turn}_A \quad : \quad A\leftpop\bot \quad \morph{} \quad \bot\rightpop A
$$
satisfying a series of carefully chosen coherence diagrams.
%
This helical structure leads us to introduce
%of a \emph{twisting operation} on the negation functors~$R$ and~$L$.
%
a topological refinement of traditional game semantics,
where the control flow of the tensorial net represented
by the functors~$L$ and~$R$ may be ``twisted'' in the same way as a ribbon.
%
Following the principle of depolarization, one recovers the familiar notion
of cyclic proof-net when one specializes to the situation
of a self-dual dialogue chirality where the two sides~$\Acategory$ and~$\Bcategory$
coincide, and where the two functors~$L$ and~$R$ disappear.
%
These issues are treated in a companion paper~\cite{mellies:tensorial-logic-5}.

\medbreak

At this very last stage of the paper, we realize that the reader may find
frustrating to have done such a long way in the paper without getting
in the end a clearcut resolution of the questions raised in the introduction.
%
We should thus mention that a satisfactory answer exists for dialogue categories
in the symmetric case.
%
Let us start by the case of $\ast$-autonomous categories.
%
Recall that a linearly distributive category~$\Ccategory$ is called symmetric
when its tensor product is equipped with a symmetry.
%
\begin{proposition}[Cockett-Seely]
Every symmetric linearly distributive category~$\Ccategory$ with a right duality
defines a symmetric $\ast$-autonomous category.
\end{proposition}

\noindent
The proof is based on the observation that every right duality
defines a left duality (see \S\ref{section/left-dualities})
in the symmetric case, with combinators defined as:
%The combinators of the left duality are defined as follows:
$$
\xymatrix @-1.87pc {
\distributiveleftaxiom{x} & : & 
\unitt\ar[rrrrr]^-{\distributiverightaxiom{x}} &&&&& \rightdual{x}\cotensor x\ar[rrrrr]^-{symmetry} &&&&& x\cotensor\rightdual{x}
&&&&&
\distributiveleftcut{x} & : & \rightdual{x}\tensor x\ar[rrrrr]^-{symmetry} &&&&& x\tensor\rightdual{x}\ar[rrrrr]^-{\distributiverightcut{x}} &&&&& \bot}
$$
%
From this follows that every symmetric linearly distributive category~$\Ccategory$ 
with a right duality is also equipped with a left duality --- and thus defines
a $\ast$-autonomous category by Proposition~\ref{proposition/main-result-linearly-distributive-categories-on-both-sides}.
%
In fact, one may show that the two notions of symmetric $\ast$-autonomous category
and of symmetric linearly distributive category~$\Ccategory$ with a duality (either left or right)
are equivalent in the appropriate 2-categorical sense.

\medbreak

Let us see how this result may be adapted to the case of dialogue chiralities
in the original sense of~\cite{mellies:tensorial-logic-2}.
%
We declare that such a dialogue chirality~$(\Acategory,\Bcategory)$ is \emph{symmetric}
when the monoidal categories~$(\Acategory,\tensorialand,\tensorialtrue)$
and~$(\Bcategory,\tensorialor,\tensorialfalse)$ are both equipped with a symmetry,
and when the original equivalence of monoidal categories~(\ref{equation/negation-as-equivalence})
becomes in this way an equivalence of \emph{symmetric} monoidal categories:
\begin{equation}\label{equation/negation-as-symmetric-monoidal-equivalence}
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{\rightcomplementary{(-)}}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
sym. monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{\leftcomplementary{(-)}}
&
\Bcategory^{\, op(0,1)}}
\end{equation}
Similarly, we declare that a linearly distributive chirality~$\Ccategory$ 
%(in the sense of \S\ref{section/linearly-distributive-chirality})
is \emph{symmetric}
when the monoidal categories~$(\Acategory,\tensorialand,\tensorialtrue)$
and~$(\Bcategory,\tensorialor,\tensorialfalse)$ are both equipped with a symmetry.
%
A right duality~$a\mapsto \rightcomplementary{a}$
on such a symmetric linearly distributive chirality is called \emph{complemented}
when it comes with an equivalence~(\ref{equation/negation-as-symmetric-monoidal-equivalence})
of symmetric monoidal categories.
%
The key observation is that in that case:
%, together with a right duality structure
%for every object~$\rightcomplementary{a}$.


\begin{proposition}
Every symmetric linearly distributive chirality~$(\Acategory,\Bcategory)$
equipped with a complemented right duality defines a symmetric dialogue chirality.
\end{proposition}
%
In fact, one could show that the notion of symmetric dialogue chirality
is equivalent in the appropriate 2-categorical sense to the notion
of symmetric linearly distributive chirality equipped with a complemented right duality.
%
This closes the circle in the symmetric case since it can be also shown
by adapting~\cite{mellies:tensorial-logic-2} that the notion of symmetric dialogue
chirality is itself equivalent to the notion of symmetric dialogue category
in a 2-categorical sense.

%%
%We would like to conclude the paper by pointing out a difficulty
%related to the status of the left and of the right negation
%in a non commutative framework.
%%framework like dialogue categories.
%%
%As it stands, our definition of dialogue category does not require
%the right negation functor~$x\mapsto (x\leftpop\bot)$ to coincide
%with the left negation functor~$x\mapsto (\bot\rightpop x)$
%even up to isomorphism.
%%
%Accordingly, a non symmetric $\ast$-autonomous category
%is defined as a dialogue category where the canonical morphisms
%$$
%x \hspace{.2em} \morph{} \hspace{.4em} (\bot\rightpop x)\leftpop\bot
%\quad\quad\quad\quad\quad
%x \hspace{.2em} \morph{} \hspace{.4em} \bot\rightpop (x\leftpop\bot)
%$$
%transporting~$x$ into its double negation are isomorphisms,
%for every object~$x$ of the dialogue category.
%%
%In that case, the object~$\bot$ is called dualizing.
%%
%As in the symmetric case, the two functors
%$$
%\begin{array}{ccccccc}
%(-)^{\bot} & \quad : \quad & x & \quad \mapsto \quad & x\leftpop\bot & \quad : \quad & \Ccategory \quad \morph{} \quad \Ccategory^{\, op}
%\\
%^{\bot}(-) & \quad : \quad & x & \quad \mapsto \quad & \bot\rightpop x & \quad : \quad & \Ccategory^{\,op} \quad \morph{} \quad \Ccategory
%\end{array}
%$$
%%associated to such a dualizing object~$\bot$ 
%defines in that case an equivalence
%\begin{equation}\label{equation/star-autonomous-categories-equivalence}
%\xymatrix @-1.8pc {
%\Ccategory
%&\ar@/^1.2pc/[rrrrrrrr]^{(-)^{\bot}}
%\ar@{}[rrrrrrrr]|-{\begin{tiny}
%\begin{array}{c}
%equivalence
%\end{array}
%\end{tiny}}
%&&&&
%&&&&
%\ar@/^1.2pc/[llllllll]^{^{\bot}(-)}
%&
%\Ccategory^{\, op}}
%\end{equation}
%between the category~$\Ccategory$ and its opposite category~$\Ccategory^{\, op}$.
%%
%The difficulty is that 
%
%%
%A typical example is provided by the dialogue category~$\mathbf{Mod}_{H}$
%of  representations (not necessarily finite dimensional) of a Hopf algebra~$H$
%with a reversible antipode~$S$, with inverse noted~$\tilde{S}$.
%%
%Define~$\bot$ as the base field~$k$ with trivial $H$-action.
%%
%In that case, the category~$\mathbf{Mod}_{H}$ defines a dialogue category
%with negation functor~$x\mapsto (\bot\rightpop x)$ defined using the antipode~$S$
%and the negation while its inverse~$\tilde{S}$ defines a negation functor~$x\mapsto (x\leftpop\bot)$.
%
%%
%In that case, the antipode define with inverse 
%
%An important observation at this point is that the linearly distributive chirality~$(\Acategory,\Bcategory)$
%cannot be recovered from the dialogue chirality structure, because the dialogue chirality structure 
%deals with right actions of~$\Acategory$ and~$\Bcategory$, whereas the linearly distributive
%chirality structure~(\ref{equation/bimonads}) is concerned with their left actions.
%%
%A natural way to resolve this problem is to start from a linearly distributive chirality~$(\Acategory,\Bcategory)$
%generated by left and right actions, and then to reconstruct an equivalent notion
%of dialogue chirality also based on left and right actions.
%%
%However, the problem of properly correlating the left and right actions of~$\Acategory$ and~$\Bcategory$
%is far more subtle than it seems.
%%
%In particular, it requires to introduce a natural isomorphism between the two negations
%$$
%\mathbf{turn}_A \quad : \quad A\leftpop\bot \quad \morph{} \quad \bot\rightpop A
%$$
%satisfying a series of appropriate coherence diagrams.
%%
%This leads to the axiomatic investigation of helical, cyclic, braided or symmetric notions of dialogue category.
%%
%This is done in a companion paper.
%
%
%
%defined as a monoidal biclosed category~$\Ccategory$
%equipped with a dualizing object~$\bot$, see~\cite{barr:non-symmetric-star-autonomous}
%for details.
%%
%Recall that an object~$\bot$ of a biclosed monoidal category~$\Ccategory$
%is called \emph{dualizing} when the two canonical morphisms
%$$
%x \hspace{.2em} \morph{} \hspace{.4em} (\bot\rightpop x)\leftpop\bot
%\quad\quad\quad\quad\quad
%x \hspace{.2em} \morph{} \hspace{.4em} \bot\rightpop (x\leftpop\bot)
%$$
%transporting~$x$ into its double negation is an isomorphism, for every object~$x$ of the category.
%%
%The terminology itself of ``dualizing object'' comes from the fact that the pair of
%negation functors
%$$
%\begin{array}{ccccccc}
%(-)^{\bot} & \quad : \quad & x & \quad \mapsto \quad & x\leftpop\bot & \quad : \quad & \Ccategory \quad \morph{} \quad \Ccategory^{\, op}
%\\
%^{\bot}(-) & \quad : \quad & x & \quad \mapsto \quad & \bot\rightpop x & \quad : \quad & \Ccategory^{\,op} \quad \morph{} \quad \Ccategory
%\end{array}
%$$
%%associated to such a dualizing object~$\bot$ 
%defines in that case an equivalence
%\begin{equation}\label{equation/star-autonomous-categories-equivalence}
%\xymatrix @-1.8pc {
%\Ccategory
%&\ar@/^1.2pc/[rrrrrrrr]^{(-)^{\bot}}
%\ar@{}[rrrrrrrr]|-{\begin{tiny}
%\begin{array}{c}
%equivalence
%\end{array}
%\end{tiny}}
%&&&&
%&&&&
%\ar@/^1.2pc/[llllllll]^{^{\bot}(-)}
%&
%\Ccategory^{\, op}}
%\end{equation}
%between the category~$\Ccategory$ and its opposite category~$\Ccategory^{\, op}$.
%%
%This establishes that every $\ast$-autonomous category~$\Ccategory$ is self-dual,
%in the technical sense that it is equivalent to its opposite category.
%%
%In order to avoid unnecessary complications, we will often restrict ourselves
%to the case of symmetric $\ast$-autonomous categories, whose underlying
%monoidal closed category~$\Ccategory$ is symmetric.
%%
%Note that such a symmetric $\ast$-autonomous category may be defined as
%a symmetric monoidal closed category~$\Ccategory$ equipped with a dualizing
%object~$\bot$, itself defined as an object such that the canonical morphism
%$$
%x\quad \morph{} \quad (x\leftpop \bot)\leftpop \bot
%$$
%is an isomorphism for every object~$x$ of the category~$\Ccategory$.
%
%
\begin{thebibliography}{}
%\begin{scriptsize}
\begin{small}

\bibitem{baez-dolan:hda3}
John Baez and James Dolan.
Higher-Dimensional Algebra III: $n$-Categories and the Algebra of Opetopes.
Adv. Math. 135 (1998), 145-206.

\bibitem{barr:non-symmetric-star-autonomous}
Michael Barr.
Non-symmetric $\ast$-autonomous categories.
Theoret. Comput. Sci., Volume 139, Number 1-2, p.115--130 (1995)

\bibitem{cockett-seely:weakly-distributive-categories}
Robin Cockett, Robert Seely.
Weakly Distributive Categories.
Journal of Pure and Applied Algebra 114 (1997) 2, pp 133-173.

\bibitem{blute-cockett-seely-trimble}
Richard Blute, Robin Cockett, Robert Seely, and Todd Trimble. 
Natural deduction and coherence  for weakly distributive categories.
Journal of Pure and Applied Algebra, 113:229-296, 1996. 

%\bibitem{cockett-seely:games}
%Robin Cockett, Robert Seely.
%Polarized category theory, modules, and game semantics.
%Theory and Applications of Categories 18~(2) (2007) 4--101.

\bibitem{girard:ll}
Jean-Yves Girard.
Linear Logic.
Theoretical Computer Science, London Mathematical 50:1, pp. 1-102, 1987

\bibitem{girard:synsem}
Jean-Yves Girard.
Linear Logic, its syntax and semantics.
Advances in Linear Logic, eds Girard, Lafont, Regnier, London Mathematical Society Lecture Notes Series 222, Cambridge University Press 1995. 

\bibitem{girard:lc}
Jean-Yves Girard. 
A new constructive logic: Classical logic, Mathematical
Structures in Computer Science 1~(3) (1991) 255--296.

%\bibitem{girard:ludics}
%Jean-Yves Girard. 
%Locus Solum.
%Mathematical Structures in Computer Science 11, pp. 301-506, 2001. 


%\bibitem{hofmann-streicher02}
%Martin Hofmann, Thomas Streicher. Completeness of continuation models for
%$\lambda\mu$-calculus, Information and Computation 179~(2) (2002) 332--355.

%\bibitem{maclane-kelly}
%Max Kelly, Saunders MacLane. 
%Coherence in closed categories.
%Journal of Pure and Applied Algebra, 1(1):97?140, 1971. 

%\bibitem{kelly-laplaza:coherence-for-compact-closed}
%G.~M. Kelly, M.~L. Laplaza, Coherence for compact closed categories,
%Journal of Pure and Applied Algebra 19 (1980) 193--213.



\bibitem{kelly-street}
Max Kelly, Ross Street.
Review of the elements of 2-categories, in Kelly (ed.), Category Seminar, LNM 420.

\bibitem{mellies:survey}
Paul-Andr\'e Melli\`es. Categorical semantics of linear logic.
Published in \emph{Interactive models of computation and program behaviour}.
Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, Paul-Andr\'e Melli\`es.
Panoramas et Synth\`eses 27, Soci\'et\'e Math\'ematique de France, 2009. 

\bibitem{mellies:tensorial-logic-1}
Paul-Andr\'e Melli\`es.
Game semantics in string diagrams.
Proceedings of the Twenty-Seventh Annual ACM/IEEE Symposium on
Logic In Computer Science (LICS 2012).

\bibitem{mellies:tensorial-logic-2}
Paul-Andr\'e Melli\`es.
Dialogue categories and chiralities.
Submitted. Manuscript available on the author's webpage.

\bibitem{mellies:tensorial-logic-3}
Paul-Andr\'e Melli\`es.
The parametric continuation monad.
Submitted. Manuscript available on the author's webpage.

\bibitem{mellies:tensorial-logic-5}
Paul-Andr\'e Melli\`es.
%Helical and braided negation.
A micrological study of negation continued.
In preparation.
%Submitted. Manuscript available on the author's webpage.

%\bibitem{mellies:tensorial-logic-6}
%Paul-Andr\'e Melli\`es.
%Braided notions of dialogue categories.
%Submitted. Manuscript available on the author's webpage.

\bibitem{street:formal-monad-theory}
Ross Street.
The formal theory of monads, J. Pure Appl. Alg. 2:149-168, 1972.

\end{small}
%\end{scriptsize}
\end{thebibliography}

\newpage

\tableofcontents


\end{document}
