%
%
%A FAIRE = s'occuper du mate (ou de son inverse)
%
%
% A FAIRE = 
% presenter la 2-categorie des chiralites helicoidales de la seconde maniere
% au moyen de la paire de currification gauche et droite
%
% decrire la 2-categorie des paires discursives, des paires discursives helicoidales
% et la 2-categorie des paires discursives helicoidales avec dualite
% montrer un résultat d'équivalence / isomorphisme
%
% etudier une toute derniere presentation des chiralités hélicoidales
% ou les transjonctions sont comparees a travers la dualite.
%
% conclure sur la loi eta pour la negation
%
%
\documentclass[12pt]{article}
%\usepackage{latex8}
%\usepackage{newcent}
%\usepackage{palatcm}
%\usepackage{palatino}
%\usepackage[mathscr]{euscript}
\usepackage{bussproofs}
%\usepackage{times}
%\usepackage{mathabx}
\usepackage{bbm}
\usepackage{pxfonts}
\usepackage{lmodern}
\usepackage{newcent}
\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.4em}
\addtolength{\voffset}{-1.7em}
%\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{\leftcomplementary}[1]{{^{\ast}#1}}
\newcommand{\rightcomplementary}[1]{{#1^{\ast}}}
\newcommand{\leftambicomplementary}[1]{{^{\circledast}#1}}
\newcommand{\rightambicomplementary}[1]{{#1^{\circledast}}}
\newcommand{\companionleftcomplementary}[1]{{#1^{\circledast}}}
\newcommand{\companionrightcomplementary}[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{\Mcategory}{\mathscr{M}}
\newcommand{\Ncategory}{\mathscr{N}}
\newcommand{\Wcategory}{\mathscr{W}}
\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}{A}
\newcommand{\MonCata}{M}
%\newcommand{\Unit}{A}
%\newcommand{\Unit}{\eta}
\newcommand{\Counit}{\epsilon}
\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{true}}
\newcommand{\tensorialfalse}{\mathbf{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{\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}
\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{\Chiralities}{\mbox{\textit{\textbf{Chir}}}}
%\newcommand{\MonChiralities}{\mbox{\textit{\textbf{MonChir}}}}
%\newcommand{\MirChiralities}{\mbox{\textit{\textbf{Ref\hspace{.1em}Chir}}}}
\newcommand{\DialogueChiralities}{\mbox{\textit{\textbf{DiaChir}}}}
%\newcommand{\RefCat}{\mbox{\textit{\textbf{Ref\hspace{.15em}Cat}}}}
%\newcommand{\Dial}{\mbox{\textit{\textbf{DiaCat}}}}
\newcommand{\verticalproof}[1]{\begin{array}{c}#1\vspace{-.5em}\\ \vdots\end{array}}
\newcommand{\HeliCat}{\mbox{\textit{\textbf{HeliCat}}}}
\newcommand{\HeliChir}{\mbox{\textit{\textbf{HeliChir}}}}
\newcommand{\AmbiChir}{\mbox{\textit{\textbf{AmbiChir}}}}

%\newcommand{\helix}{\sigma}
\newcommand{\helix}{\mathbf{\mathit{helix}}}

\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 helix negation}
%Tensorial logic 1\\
%A combinatorial presentation\\
%of dialogue categories\\
%------ part two ------}
%\\
%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.}}

\maketitle

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


\begin{abstract}
%
This paper is the second part of the micrological study of negation
initiated in our companion paper.
%
We have encountered there a discrepancy
between left and right dialogue chiralities
which we resolve here by introducing
the notion of ambidextrous dialogue chirality.
%
One main purpose of the paper is to disclose
the topological nature of this logical notion.
%
More specifically, we establish that an ambidextrous chirality
is the same thing as a left chirality equipped
with an helical structure on its tensorial negation.
%
This topological insight enables us to conclude the project
initiated in our companion paper, and to present
ambidextrous chiralities in a purely combinatorial way.
\end{abstract}

\section{Introduction}
Among the several equivalent definitions of \emph{dialogue chirality}
formulated in our companion paper~\cite{mellies:tensorial-logic-4},
one finds a definition directly inspired by proof-theory
and based on the following combinators:
$$
\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}$$
%
Besides the requirement that these combinators define a transjunction
accross the adjunction~$L\dashv R$ for every object~$m$
of the category~$\Acategory$, one requires that they satisfy a monoidality property,
expressed by the following coherence diagram for the $\axiom{-}$ combinator:
\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}
%
As expected, this diagram is required to commute for all objects~$a,m,n$ of the category~$\Acategory$.
%
Looking at it with linear and tensorial proof-nets in mind, 
this coherence diagram may be understood as an $\eta$-expansion law for the axiom link.
%
This point becomes even clearer when one translates~(\ref{equation/tensorial-eta-expansion-diagram})
in the graphical language of string diagrams:
\begin{equation}\label{equation/tensorial-axiom-cut-left-hand-side}
\begin{tabular}{ccc}
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-1.pdf}
&
\hspace{1em} \raisebox{22mm}{\Large{$\stackrel{}{=}$}} \hspace{1em}
&
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-2.pdf}
\end{tabular}
\end{equation}
%
As should be clear from the picture, the purpose of  the $\eta$-expansion law
is to decompose the $\axiom{m\tensorialand n}$ link
into the pair of more elementary $\axiom{m}$ and $\axiom{n}$ links.
%
A natural question is whether there exists a similar $\eta$-expansion law
for the axiom link
\begin{equation}\label{equation/left-axiom-link-for-Rm}
\xymatrix @-1pc {
La
&
\ar[rrrrrrr]^-{\leftaxiom{Rm}}
&&&&&&&
&
\rightcomplementary{(Rm)}
\tensorialor
L((Rm)\tensorialand a)
}
\end{equation}
associated to the negation~$Rm$ of an object~$m$ of the category~$\Bcategory$.
%
The idea would be to deduce it from the axiom link of the object~$m$ itself.
%
However, the object~$m$ lives in the category~$\Bcategory$ and thus needs
to be translated back to the object~$\leftcomplementary{m}$ which lives 
in the other side~$\Acategory$ of the dialogue chirality.
%
Recall that the two monoidal categories~$(\Acategory,\tensorialand,\tensorialtrue)$
and~$(\Bcategory,\tensorialor,\tensorialfalse)$ of a dialogue chirality
are related by a 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)}}
$$
%
See~\cite{mellies:tensorial-logic-2} for details.
%
Note that we are careful here to indicate in~(\ref{equation/left-axiom-link-for-Rm})
that we consider the \emph{left} axiom link.
%
The reason is that, in order to define an $\eta$-expansion for~$Rm$, 
one needs to be careful about orientations and to start from the \emph{right} axiom link
$$
\xymatrix @-.8pc {
L(\tensorialtrue)
&
\ar[rrrrr]^-{\rightaxiom{m}}
&&&&&
&
L(\leftcomplementary{m})
\tensorialor
m
}
$$
associated to the object~$m$ in the category~$\Bcategory$.
%
This morphism induces in turn the morphism
$$
\xymatrix @-1.2pc {
La 
&
\ar[rr]^-{\eta}
&&
&
L(
RL(\tensorialtrue)
\tensorialand 
a)
&
\ar[rrrr]^-{map}
&&&&
&
L(R(L(\leftcomplementary{m})\tensorialor m)\tensorialand a)
}
$$
which may be composed with the distributivity law
$$
\xymatrix @-1.4pc {
L(R(L(\leftcomplementary{m})\tensorialor m)\tensorialand a)
&
\ar[rrrrrrr]^-{distributivity}
&&&&&&&
&
L(\leftcomplementary{m})
\tensorialor
L((Rm)\tensorialand a)
}$$
%
The resulting morphism
%from~$La$ to $L(\leftcomplementary{m})\tensorialor L((Rm)\tensorialand a)$
\begin{equation}\label{equation/the-composite-for-eta-expansion}
\xymatrix @-.8pc {
La 
&
\ar[rrrr]^-{}
&&&&
&
L(\leftcomplementary{m})
\tensorialor
L((Rm)\tensorialand a)
}
\end{equation}
may be depicted in the following way:
\begin{center}
\begin{tabular}{c}
\includegraphics[height=90mm]{dessins/micrological-of-twisted-negation/3d-diagram-axiom-Rm-couleur.pdf}
\end{tabular}
\end{center}
%
The different shades of blue and red are here to separate
the different instances of categories~$\Acategory$ and~$\Bcategory$
appearing in the 2-categorical diagram.
%
Note that for graphical convenience, we depict a variant 
%
$$
\xymatrix @-1.9pc {
L(\tensorialtrue\tensorialand a)
\ar[rrrr]^-{}
&&&&
L(
R(
L(
\tensorialtrue
\tensorialand
\leftcomplementary{m}
)
\tensorialor
m)
\tensorialand a
)
\ar[rrrr]^-{}
&&&&
L(\tensorialtrue\tensorialand\leftcomplementary{m})
\tensorialor
L((Rm)\tensorialand a)}
$$
of the morphism~(\ref{equation/the-composite-for-eta-expansion}).
%
The last step in order to complete the construction
is to require the existence of a family of isomorphisms
%
\begin{equation}\label{equation/helical-morphism}
\xymatrix{
L(\leftcomplementary{m})
&
\ar[rrrr]^-{isomorphism}
&&&&
&
\rightcomplementary{(Rm)}
}
\end{equation}
%
natural in~$m$.
%
In this way, by composing~(\ref{equation/the-composite-for-eta-expansion})
with~(\ref{equation/helical-morphism}),
one obtains a morphism
\begin{equation}\label{equation/candidate-for-left-axiom-link-for-Rm}
\xymatrix @-1.4pc {
La
&
\ar[rrrrrrr]^-{}
&&&&&&&
&
\rightcomplementary{(Rm)}
\tensorialor
L((Rm)\tensorialand a)
}
\end{equation}
with the expected source and target.
%
There remains to understand whether the resulting morphism
coincides with the original axiom link~(\ref{equation/left-axiom-link-for-Rm}).
%associated to the negation of the object~$m$ in~$\Bcategory$.
%
Although the answer to this question is positive in many situations of interest,
it appears that nothing compels the two morphisms to coincide in general.
%
This technical point is subtle but fundamental because it reveals
that logical negation may be \emph{twisted} in exactly
the same way as a topological ribbon.
%
We will see that the two morphisms~(\ref{equation/left-axiom-link-for-Rm})
and~(\ref{equation/candidate-for-left-axiom-link-for-Rm})
are equal modulo a twist of angle~$2\pi$ of the negation strand.
%
This observation puts topology at the heart of logic.
%he secretly topological nature of logical negation.
%

\medbreak

%
Our primary purpose in this work is to shed light on
these topological aspects of the logical negation
by transferring ideas coming from functorial knot theory
and representation theory of quantum groups.
%
Recall that the notion of ribbon category axiomatizes
the properties of the category~$Mod(H)$ of finite dimensional representations
of a quantum group~$H$, defined here as a quasi-triangular
and twisted Hopf algebra.
%
Every object~$\bot$ in such a ribbon category~$\Ccategory$
defines a pair of negation functors
%\newcommand{\leftstar}[1]{{}^{\ast}{#1}}
%\newcommand{\rightstar}[1]{{#1}^{\ast}}
\newcommand{\leftstar}[1]{{#1}^{\vee}}
\newcommand{\rightstar}[1]{{#1}^{\wedge}}
$$
x\leftpop\bot := \rightstar{x}\tensor\bot
\quad\quad\quad\quad\quad\quad\quad
\bot\rightpop x := \bot\tensor\leftstar{x}
$$
where~$\rightstar{x}$ denotes the right dual and 
$\leftstar{x}$ denotes the left dual of the object~$x$
in the ribbon category.
%
These negation functors equip the ribbon category~$\Ccategory$
with the structure of a dialogue category.
%
The associated dialogue chirality~$(\Acategory,\Bcategory)$ has monoidal sides
defined as
%
$$
(\Acategory,\tensorialand,\tensorialtrue)=(\Ccategory,\tensor,\mathbf{1})
\quad\quad\quad
(\Bcategory,\tensorialor,\tensorialfalse)=(\Ccategory,\tensor,\mathbf{1})^{\, op(0,1)}
$$
with monoidal equivalence~$\rightcomplementary{(-)}$ and~$\leftcomplementary{(-)}$
defined as the identity on~$\Ccategory$.
%
We wish to give a little precedence to the right axiom combinator
and thus define~$L$ and~$R$ as the negation functors
%There are two adjunctions, on the left and on the right...
%
$$
Lx=x\leftpop \bot = \rightstar{x}\tensor \bot
\quad\quad\quad\quad\quad\quad
Rx=\bot\rightpop x=\bot\tensor\leftstar{x}.
$$
The right axiom associated to the object~$m$ in the category~$\Ccategory$
$$
\xymatrix @-1pc {
La=\rightstar{a}\tensor\bot
&
\ar[rrrr]^-{\leftaxiom{m}}
&&&&
&
L(a\tensorialand \leftcomplementary{m})
\tensorialor
m
& \cong &
m\tensor \rightstar{m}\tensor\rightstar{a}\tensor\bot
}
$$
lives in the category~$\Bcategory=\Ccategory^{\, op}$ and is thus defined
as the counit of the dual pair $x\dashv\rightstar{x}$ and depicted as follows
in the category~$\Ccategory$:
\begin{center}
\begin{tabular}{ccc}
\raisebox{8mm}{$\rightaxiom{m}$}
& 
\quad \raisebox{8mm}{$=$}  \quad\quad
&
\includegraphics[height=22mm]{dessins/micrological-of-twisted-negation/right-axiom-ribbon-illustration.pdf}
\end{tabular}
\end{center}
%
The left axiom associated an object~$m$
$$
\xymatrix @-1pc {
La=\rightstar{a}\tensor\bot
&
\ar[rrrr]^-{\leftaxiom{m}}
&&&&
&
\rightcomplementary{m}
\tensorialor
L(m\tensorialand a)
& \cong &
\rightstar{a} \tensor \rightstar{m} \tensor \bot \tensor m
}
$$
requires a braiding:
\begin{center}
\begin{tabular}{ccc}
\raisebox{12mm}{$\leftaxiom{m}$}
& 
\quad \raisebox{12mm}{$=$}  \quad\quad
&
\includegraphics[height=25mm]{dessins/micrological-of-twisted-negation/left-axiom-ribbon-illustration.pdf}
\end{tabular}
\end{center}
where we may for simplicity identify the left dual~$\leftstar{x}$
and the right dual~$\rightstar{x}$ of the object~$x$ at the condition
of adding the equality:
$$
\includegraphics[height=8em]{dessins/ribbon-categories-xyz/left-dual-as-right-dual-counit.pdf}
$$

The two morphisms are not equal... but equal modulo a twist.
\begin{center}
\begin{tabular}{ccc}
\raisebox{14mm}{$\leftaxiom{Rm}$}
& 
\quad \raisebox{14mm}{$=$}  \quad\quad
&
\includegraphics[height=32mm]{dessins/micrological-of-twisted-negation/ribbon-illustration.pdf}
\end{tabular}
\end{center}
On the other hand, the composite map is equal to:
\begin{center}
\begin{tabular}{ccc}
\raisebox{22mm}{composite morphism~(\ref{equation/candidate-for-left-axiom-link-for-Rm})}
& 
\quad \raisebox{22mm}{$=$}  \quad\quad
&
\includegraphics[height=48mm]{dessins/micrological-of-twisted-negation/ribbon-illustration-bis.pdf}
\end{tabular}
\end{center}
%
This shows that the two morphisms~(\ref{equation/left-axiom-link-for-Rm})
and~(\ref{equation/candidate-for-left-axiom-link-for-Rm}) are different
in the particular case of ribbon categories.
%
They differ of a twist on the object~$\bot$.

$$\xymatrix @-1.4pc {
La=\rightstar{a}\tensor\bot
&
\ar[rrrrrrr]^-{}
&&&&&&&
&
\rightcomplementary{(Rm)}
\tensorialor
L(
(Rm)\tensorialand a
)
&
\cong
&
(\rightstar{a}
\tensor
\bot
\tensor
\leftstar{m}
)
\tensor\bot
\tensor
\bot\tensor\leftstar{m}
}$$

The twist may be obtained in any dialogue category !!!

As we will see, this additional combinator has a topological content,
and may be interpreted as an \emph{helical} structure on the tensorial negation
of the underlying dialogue category~$\Ccategory$.
%
This helical structure generalizes the familiar notion
of pivotal or cyclic monoidal category.
%
This requires to integrate this helical map in the general theory
of distributivity laws developed in our companion paper~\cite{mellies:tensorial-logic-4}.
%
We will see that the two morphisms are not equal,
that one needs to twist the negation functors~$R$ and~$L$.


\section{Helical dialogue categories and chiralities}
%
The notion of helical dialogue category was introduced
in the companion paper~\cite{mellies:tensorial-logic-6}
among a series alternative notions of dialogue categories
motivated by topology.
%
The notion of helical dialogue category is important
because it appears (at least in our current understanding)
as the most primitive instance of these topological notions
of dialogue categories.
%
In particular, every cyclic or ribbon dialogue category
is helical in a canonical way.
%
Our main purpose in this section is to introduce and to justify
the corresponding notion of \emph{helical dialogue chirality.}
%
In order to validate this 2-sided account of helical dialogue categories,
we proceed in exactly the same way as for the notion
of dialogue chirality, see~\cite{mellies:tensorial-logic-2} for details.
%
We thus construct a 2-category~$\HeliCat$ of helical dialogue categories
in~\S\ref{section/a-2-category-of-helical-dialogue-categories}
and a 2-category~$\HeliChir$ of helical dialogue chiralities
in~\S\ref{section/helical-dialogue-chiralities} and~\S\ref{section/a-2-category-of-helical-dialogue-chiralities}.
%
Finally, we exhibit a 2-dimensional equivalence between the pair of 2-categories
in~\S\ref{section/biequivalence-between-the-2-categories}.
%

\subsection{Helical dialogue categories}
%Recall from~\cite{mellies:tensorial-logic-1,mellies:tensorial-logic-2}
A dialogue category is defined as a monoidal category~$(\Ccategory,\tensor,\tensorialunit)$
equipped with an object~$\bot$ coming together with a representation
$$
\varphi_{x,y} \quad : \quad 
\Ccategory(x\otimes y, \bot) \quad \cong \quad \Ccategory(y,x\leftpop\bot)
$$
of the functor
$$y\mapsto \Ccategory(x\otimes y, \bot) \quad : \quad \Ccategory^{op} \longrightarrow Set$$
for each object~$x$, and with a representation
$$
\psi_{x,y} \quad : \quad 
\Ccategory(x\otimes y, \bot) 
\quad \cong \quad \Ccategory(x,\bot\rightpop y)
$$
of the functor
$$x\mapsto \Ccategory(x\otimes y, \bot) \quad : \quad \Ccategory^{op} \longrightarrow Set$$ 
for each object~$y$.
%
The following notion of dialogue category is introduced in~\cite{mellies:tensorial-logic-4}.
\begin{definition}[helical dialogue category]
A helical dialogue category is a dialogue category~$\Ccategory$ equipped with a family of bijections
$$
\RefutationCycle{x}{y} \quad : \quad
\Ccategory(x\tensor y,\bot) 
\quad \morph{} \quad
\Ccategory(y\tensor x,\bot) 
$$
natural in~$x$ and~$y$ and required to make the diagram
%
\begin{equation}\label{equation/coherence-dialogue-wheel}
\vcenter{\xymatrix @-1.2pc {
\Ccategory((y\tensor z)\tensor x,\bot)
\ar[rrrrr]^-{associativity}
&&&&&
\Ccategory(y\tensor (z\tensor x),\bot)
\ar[dd]^-{\RefutationCycle{y}{z\tensor x}}
\\
\\
\Ccategory(x\tensor (y\tensor z),\bot)
\ar[uu]^-{\RefutationCycle{x}{y\tensor z}}
\ar[dd]_-{associativity}
&&&&&
\Ccategory((z\tensor x)\tensor y,\bot)
\\
\\
\Ccategory((x\tensor y) \tensor z,\bot)
\ar[rrrrr]^-{\RefutationCycle{x\tensor y}{z}}
&&&&&
\Ccategory(z\tensor (x\tensor y),\bot)
\ar[uu]_-{associativity}
}}
\end{equation}
%
commute for all objects $x,y,z$ of the category~$\Ccategory$.
%
\end{definition}
\begin{equation}\label{equation/roue-par-dessous}
\begin{tabular}{cccc}
\raisebox{3em}{$\RefutationCycle{x}{y} \quad : \quad$} 
&
\raisebox{.2em}{\includegraphics[height=6em]{dessins/helical-chiralities/wheel-helical-dialogue-categories-1.pdf}}
&
\raisebox{3em}{$\quad \large{\mapsto}\quad$}
&
\includegraphics[height=6.5em]{dessins/helical-chiralities/wheel-helical-dialogue-categories-2.pdf}
\end{tabular}
\end{equation}
In that graphical formulation, the coherence diagram expresses that the diagram below commutes:
\begin{center}
\fbox{$\begin{array}{ccc}
\\
\quad & \includegraphics[height=16em]{dessins/helical-chiralities/wheel-helical-dialogue-categories-coherence-diagram.pdf} &
\quad
\\
\\
\end{array}$}
\end{center}
\vspace{1em}
It is not very difficult to deduce from the coherence diagram~(\ref{equation/dialogue-coherence-wheel}) that the diagram
$$
\xymatrix @-.5pc {
\Ccategory(x\tensor\tensorialunit,\bot)
\ar[rrrrr]^-{\RefutationCycle{x}{\tensorialunit}}
&&&&&
\Ccategory(\tensorialunit\tensor x,\bot)
\ar[d]^-{associativity}
\\
\Ccategory(x,\bot)
\ar[u]^-{associativity}
\ar[rrrrr]^{id}
&&&&&
\Ccategory(x,\bot)
}
$$
commutes in any helical refutation category.
%(hint: take $x=y=\unit$).
%
On the other hand, the other expected coherence diagram
\begin{equation}\label{equation/other-helical-expected-diagram}
\raisebox{2em}{
\xymatrix @-.5pc {
\Ccategory(\tensorialunit\tensor x,\bot)
\ar[rrrrr]^-{\RefutationCycle{\tensorialunit}{x}}
&&&&&
\Ccategory(x\tensor\tensorialunit,\bot)
\ar[d]^-{associativity}
\\
\Ccategory(x,\bot)
\ar[u]^-{associativity}
\ar[rrrrr]^{id}
&&&&&
\Ccategory(x,\bot)
}}
\end{equation}
%
does not commute in general.
%
As a matter of fact, this is an important aspect of our definition:
we will see in \S\,\ref{section/dialogical-twist}
that this lack of coherence reflects the existence
of a topological ``twist'' on the negation
arising as follows:
\begin{center}
\begin{tabular}{cccc}
\raisebox{3em}{$\RefutationCycle{x}{\unit}\quad : \quad$} &
\includegraphics[height=8em]{dessins/helical-chiralities/helical-dialogue-categories-dialogical-twist-1.pdf}
&
\raisebox{3em}{$\quad \large{\mapsto}\quad$}
&
\includegraphics[height=8em]{dessins/helical-chiralities/helical-dialogue-categories-dialogical-twist-2.pdf}
\end{tabular}
\end{center}


\subsection{A 2-category of helical dialogue categories}
\label{section/a-2-category-of-helical-dialogue-categories}
We define a 2-category $\HeliCat$ with
\begin{itemize}
\item helical dialogue categories as 0-cells, 
\item helical functors as 1-cells,
\item dialogue natural transformations as 2-cells.
\end{itemize}

\paragraph{The 1-dimensional cells.}
%\begin{definition}[helical functor]
A helical functor between two helical dialogue categories
is defined as a lax monoidal functor
$$
F \quad : \quad \Ccategory \quad \morph{} \quad \Dcategory
$$
equipped with a morphism
$$
\bot_{F} \quad : \quad F(\bot) \quad \morph{} \quad \bot
$$
such that the diagram
\begin{equation}\label{equation/helical-functors-compatibility}
\vcenter{\xymatrix @-.8pc {
\Ccategory(x\tensor y,\bot)
\ar[rr]^- {F}
\ar[dd]_-{\RefutationCycle{x}{y}}
&&
\Dcategory(F(x\tensor y),F(\bot))
\ar[rrr]^-{coercion}
&&&
\Dcategory(F(x)\tensor F(y),\bot)
\ar[dd]^-{\RefutationCycle{F(x)}{F(y)}}
\\
\\
\Ccategory(y\tensor x,\bot)
\ar[rr]^-{F}
&&
\Dcategory(F(y\tensor x),F(\bot))
\ar[rrr]^-{coercion}
&&&
\Dcategory(F(y)\tensor F(x),\bot)
}}
\end{equation}
commutes for all objects~$x$, $y$ of the category~$\Ccategory$.
%
In this diagram, the two coercion maps are deduced
by precomposing with the lax monoidal structure of the functor~$F$
$$
m_{x,y} \quad : \quad F(x)\tensor F(y) \quad \morph{} \quad F(x\tensor y)
$$
and by postcomposing with the map $\bot_{F}$.

\paragraph{The 2-dimensional cells.}
The 2-cells are defined in the same way as in the case of dialogue categories,
see~\cite{mellies:tensorial-logic-2} for details.
%
A dialogue natural transformation 
$$
\theta \quad : \quad (F,\bot_{F}) \quad \Rightarrow \quad (G,\bot_{G})
%\quad : \quad \Ccategory \quad \morph{} \quad \Dcategory
$$
is defined there as a natural transformation
$$
\theta \quad : \quad F \quad \Rightarrow \quad G
$$
making the diagram
$$
\xymatrix @-.8pc {
F(\bot)
\ar[dd]_-{\theta_{\bot}}
\ar[rrd]^-{\bot_F}
\\
&& \bot
\\
G(\bot)
\ar[rru]_-{\bot_G}
}
$$
commute.
%
We leave the reader check that the expected notions
of (horizontal and vertical) identity and composition
define a 2-category $\HeliCat$ together with a forgetful 2-functor
$$
U \quad : \quad \HeliCat \quad \morph{} \quad \Dial
$$
to the 2-category~$\Dial$ of dialogue categories
constructed in~\cite{mellies:tensorial-logic-2}.
%
Note that by construction, the 2-functor~$U$ is fully faithful on 2-dimensional cells.

\subsection{Helical dialogue chiralities}\label{section/helical-dialogue-chiralities}
Recall from~\cite{mellies:tensorial-logic-2,mellies:tensorial-logic-4}
that a dialogue chirality is defined as a pair of monoidal categories
$$
(\Acategory,\tensorialand,\tensorialtrue)
\quad \quad\quad \quad
(\Bcategory,\tensorialor,\tensorialfalse)
$$
equipped with an adjunction~$L\dashv R$ and with a monoidal equivalence
$$
\xymatrix @-1.9pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory
}
\quad\quad\quad\quad\quad\quad
\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)}}
$$
together with a family of bijections
\begin{equation}\label{equation/currification}
\currify{m}{a}{b} \quad : \quad \distributor{m\tensorialand a}{b}
\quad \morph{} \quad \distributor{a}{\rightcomplementary{m}\tensorialor b}
\end{equation}
natural in $a$ and $b$, where $\distributor{a}{b}$ is defined as
$$
\distributor{a}{b} \quad = \quad \Acategory(\, a \, , \, \rightadjoint \, b \, ).
$$
%
The family~$\currifyalone$ is moreover required to make the diagram
%
\begin{equation}\label{equation/coherence/currify-one-dialogue}
\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.
%
A helical dialogue chirality is then defined as a dialogue category
equipped with a natural family of bijections~$\helix$ permuting
the two sides of the evaluation bracket~$\distributor{-}{-}$.
%
\begin{definition}[helical chirality]\label{definition/helical-dialogue-chirality}
%[helical dialogue chirality]
A helical structure in a dialogue chirality is defined as a family of bijections
$$
\helix_{a,b} \quad : \quad \distributor{a}{b} 
\quad \morph{} \quad \distributor{\leftcomplementary{b}}{\rightcomplementary{a}}
$$
natural in~$a$ and $b$, and making the diagram below commute:
\begin{equation}\label{equation/coherence-diagram-helix}
\vcenter{\xymatrix @-.4pc {
\distributor{a_1\tensorialand a_2}{b}
\ar[d]_-{\currify{a_1}{a_2}{b}}
\ar[rrr]^-{\helix}
&&&
\distributor{\leftcomplementary{b}}{\rightcomplementary{(a_1\tensorialand a_2)}}
\ar@{=}[rr]
&&
\distributor{\leftcomplementary{b}}{\rightcomplementary{a_2}\tensorialor\rightcomplementary{a_1}}
\\
\distributor{a_2}{\rightcomplementary{a_1}\tensorialor b}
\ar[d]_-{\helix}
&&&
&&
\distributor{a_2\tensorialand \leftcomplementary{b}}{\rightcomplementary{a_1}}
\ar[u]_-{\currify{a_2}{\leftcomplementary{b}}{\rightcomplementary{a_1}}}
\\
\distributor{\leftcomplementary{(\rightcomplementary{a_1}\tensorialor b)}}{\rightcomplementary{a_2}}
\ar@{=}[d]
&&&
&&
\distributor{\leftcomplementary{(b\tensorialor \rightcomplementary{a_2})}}{\rightcomplementary{a_1}}
\ar@{=}[u]
\\
\distributor{\leftcomplementary{b}\tensorialand a_1}{\rightcomplementary{a_2}}
\ar[rrr]^-{\currify{{\leftcomplementary{b}}}{a_1}{\rightcomplementary{a_2}}} 
&&&
\distributor{a_1}{\rightcomplementary{(\leftcomplementary{b})}\tensorialor \rightcomplementary{a_2}}
\ar@{=}[rr]
&&
\distributor{a_1}{b\tensorialor \rightcomplementary{a_2}}
\ar[u]_-{\helix}}}
\end{equation}
where every double edge is meant to describe a canonical coercion isomorphism
induced by the monoidal equivalence between~$\Acategory$ and~$\Bcategory^{\,op(0,1)}$.
%
A helical dialogue chirality is then defined as a dialogue chirality equipped with a helical structure.
\end{definition}
%
The family~$\helix$ induces a series of bijections
$$
\xymatrix @-1.1pc {
\Acategory(a,Rb)
 \ar[rr]^-{\helix} 
&& 
\Acategory(a, \leftcomplementary{(L(\leftcomplementary{b})}))
\ar[rrrr]^-{equivalence}
&&&&
\Bcategory(L(\leftcomplementary{b}),\rightcomplementary{a})
\ar[rrr]^-{adjunction} 
&&&
\Acategory(\leftcomplementary{b},R(\rightcomplementary{a}))
}
$$
each of them, and thus their composite, natural in~$a$ and~$b$.
%
From this follows by the usual Yoneda argument
that the natural family of bijections~$\helix$ may be
alternatively formulated as a family of isomorphisms
$\leftcomplementary{(L(\leftcomplementary{b}))}\to Rb$
natural in~$b$,
%$$\xymatrix @-1pc {Rb & \ar[rrrr] &&&& &\leftcomplementary{(L(\leftcomplementary{b}))}}$$
or equivalently, as a family of isomorphisms
\begin{equation}\label{equation/helical-as-reversed-turn}
\xymatrix @-1.3pc {\helix_a & : & \leftcomplementary{(La)}
& \ar[rrrr] &&&& &
R(\rightcomplementary{a})}
\end{equation}
natural in~$a$.

\paragraph{Remark.}
It should be noted that a dialogue chirality is typically obtained from a dialogue category
by defining the negation functors~$L$ and~$R$ as $Lx=\bot\rightpop x$
and $Rx=x\leftpop\bot$.
%
In that case, the family~(\ref{equation/helical-as-reversed-turn}) amounts to 
a family of isomorphisms 
\begin{equation}\label{equation/orientation-of-helix}
\helix_x \quad : \quad \bot\rightpop x \quad \morph{} \quad x\leftpop\bot.
\end{equation}
%
This choice of orientation is essentially arbitrary, so much arbitrary in fact
that we take the reverse one in our companion paper~\cite{mellies:tensorial-logic-6}.
%
However, there is a reason for making the particular choice~(\ref{equation/orientation-of-helix})
when one starts from the notion of dialogue chirality~(\ref{equation/coherence-diagram-helix})
considered here, with currification~(\ref{equation/currification}) acting on the left.
%
Thanks to that particular choice, we are able to keep ``positive'' all the instances of the combinators~$\helix$
and $\currifyalone$ in the coherence diagram~(\ref{equation/coherence-diagram-helix}).
%
Another choice would have been to reverse the orientation of $\helix_{a,b}$,
to take decurrification (the reverse of currification) as primitive
and to start from~$\distributor{a}{b_1\tensorialor b_2}$
in the coherence diagram~(\ref{equation/coherence-diagram-helix}).

\begin{center}
\begin{tabular}{cccc}
\raisebox{3em}{$\RefutationCycle{x}{\unit}\quad : \quad$} &
\includegraphics[height=8em]{dessins/helical-chiralities/helix-helical-dialogue-chiralities-1.pdf}
&
\raisebox{3em}{$\quad \large{\mapsto}\quad$}
&
\includegraphics[height=8em]{dessins/helical-chiralities/helix-helical-dialogue-chiralities-2.pdf}
\end{tabular}
\end{center}


\subsection{A 2-category of helical dialogue chiralities}
\label{section/a-2-category-of-helical-dialogue-chiralities}
%
We define a 2-category $\HeliChir$ with helical dialogue chiralities as objects
(or 0-dimensional cells).
%
This construction will be compared in~\S\ref{section/biequivalence-between-the-2-categories}
with the 2-category~$\HeliCat$ of helical categories just constructed in~\S\ref{section/a-2-category-of-helical-dialogue-chiralities}.

\paragraph{The 1-dimensional cells.}
%
A 1-dimensional cell in $\HeliChir$
$$
F \quad : \quad (\Acategory_1,\Bcategory_1)
\quad \morph{} \quad (\Acategory_2,\Bcategory_2)
$$
is defined in essentially the same way as a 1-dimensional cell in the 2-category $\DialogueChiralities$
of dialogue chiralities constructed in~\cite{mellies:tensorial-logic-2}.
Hence, it is a quadruple $F=(\functor{F},\functorco{F},\functorcell{F},
\functorcellbracketspecial{F})$ consisting of a lax monoidal functor~$\functor{F}:\Acategory_1\morph{}\Acategory_2$,
an oplax monoidal functor~$\functorco{F}:\Bcategory_1\morph{}\Bcategory_2$,
a monoidal natural isomorphism
\begin{equation}\label{equation/helical-chiralities/functorcell}
\vcenter{\xymatrix @-1.95pc {
\Acategory_1 \ar[rrrrrrrrrrrrrrrr]^-{\functor{F}}
\ar[dddddddd]_-{\rightcomplementary{(-)}}
\ar@{}[rrrrrrrrrrrrrrrrdddddddd]|-{\functorcell{F}}
&&&&&&&&&&&&&&&&
\Acategory_2
\ar[dddddddd]^-{\rightcomplementary{(-)}}
\\
\\
\\
\\
&&&&&&&&
&&&&&&&
\ar@{=>}@/_.7pc/[dddlll]
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Bcategory_1^{\, op(0,1)} \ar[rrrrrrrrrrrrrrrr]_-{\functorco{F}^{\, op(0,1)}}
&&&&&&&&
&&&&&&&& \Bcategory_2^{\, op(0,1)}
}}
\end{equation}
together with a natural transformation:
\begin{equation}\label{equation/helical-chiralities/functorcellbracketspecial}
\vcenter{\xymatrix @-1.95pc {
\Acategory_1 \ar[rrrrrrrrrrrrrrrr]^-{\functor{F}}
&&&&&&&&&&&&&&&&
\Acategory_2
\\
&&&&&&&&
&&&&
\ar@{=>}@/_.7pc/[dddrrr]_-{\functorcellbracketspecial{F}}
&&&
\\
\\
\\
&&&&&&&&
&&&&&&&
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Bcategory_1 \ar[rrrrrrrrrrrrrrrr]_-{\functorco{F}}
\ar[uuuuuuuu]^-{R}
&&&&&&&&
&&&&&&&&
\Bcategory_2
\ar[uuuuuuuu]_-{R}
}}
\end{equation}
making the diagram
\begin{equation}\label{equation/refraction-chiralities/monoidal-coherence-diagram}
\vcenter{\xymatrix @-1.2pc {
\distributor{m\tensorialand a}{b}
\ar[rrrr]^-{\currifyone{m}}
\ar[dd]_-{F_{m\tensorialand a,b}}
&&&&
\distributor{a}{\rightcomplementary{m}\tensorialor b}
\ar[dd]^-{F_{a,\rightcomplementary{m}\tensorialor b}}
\\
\\
\distributor{\functor{F}(m\tensorialand a)}{\functorco{F}(b)}
\ar[dddd]_-{\begin{tiny}monoidality\, o\hspace{-.12em}f\, \functor{F}\end{tiny}}
&&&&
\distributor{\functor{F}(a)}{\functorco{F}(\rightcomplementary{m}\tensorialor b)}
\ar[dd]^-{\begin{tiny}monoidality\, o\hspace{-.12em}f\, \functorco{F}\end{tiny}}
\\
\\
&&&&
\distributor{\functor{F}(a)}{
\functorco{F}(\rightcomplementary{m})
\tensorialor\functorco{F}(b)}
\ar[dd]^-{\functorcell{F}}
\\
\\
\distributor{\functor{F}(m)\tensorialand \functor{F}(a)}{\functorco{F}(b)}
\ar[rrrr]^-{\currifyone{\functor{F}(m)}}
&&&&
\distributor{\functor{F}(a)}{\rightcomplementary{\functor{F}(m)}\tensorialor\functorco{F}(b)}}}
\end{equation}
commute for all objects~$a,m$ in~$\Acategory_1$ and~$b$ in~$\Bcategory_1$.
%
Here, the map
$$
F_{a,b} \quad : \quad  \distributor{a}{b}  \quad \morph{} \quad \distributor{\functor{F}(a)}{\functorco{F}(b)}
$$
is defined as the composite
$$
\xymatrix @-1.9pc {
\distributor{a}{b}
\ar@{=}[dd]
\ar[rrrrrrrrrrrrrr]^-{F_{a,b}}
&
&&&&&&&&&&&&
&
\distributor{\functor{F}(a)}{\functorco{F}(b)}
\\
\\
\Acategory_1(a,Rb)
&
\ar[rrrrr]^-{\functor{F}}
&&&&&
&
\Acategory_2(\functor{F}(a),\functor{F}(Rb))
&
\ar[rrrrr]^-{\functorcellbracketspecial{F}}
&&&&&
&
\Acategory_2(\functor{F}(a),R\functorco{F}(b))
\ar@{=}[uu]
}
$$
%
The only additional requirement compared to a 1-dimensional cell
in~$\DialogueChiralities$ is that the diagram below commutes:
%We simply ask in addition that the diagram below commutes:
%
\begin{equation}\label{equation/additional-requirement-for-helical-1-cells}
\vcenter{\xymatrix @-.5pc {
\distributor{a}{b}
\ar[rrrr]^-{F_{a,b}}
\ar[dd]_-{\helix_{a,b}}
&&&&
\distributor{\functor{F}(a)}{\functorco{F}(b)}
\ar[dd]^-{\helix_{\functor{F}(a),\functorco{F}(b)}}
\\
\\
\distributor{\leftcomplementary{b}}{\rightcomplementary{a}}
\ar[rr]^-{F_{\leftcomplementary{b},\rightcomplementary{a}}}
&&
\distributor{\functor{F}(\leftcomplementary{b})}{\functorco{F}(\rightcomplementary{a})}
\ar[rr]^-{\functorcell{F}}
&&
\distributor
{\leftcomplementary{(\functorco{F}(b))}}
{\rightcomplementary{(\functor{F}(a))}}
}}
\end{equation}
%
Here, the map~$\functorcell{F}_{b,a}$ is defined
by applying the natural isomorphism~$\functorcell{F}$
on the object~$\functorco{F}(\rightcomplementary{a})$
in order to get the object~$\rightcomplementary{(\functor{F}(a))}$
and \emph{at the same time} its mate
$$
\functorcell{F}_{mate} 
\quad : \quad \functor{F}\circ \leftcomplementary{(-)}
\quad \Rightarrow \quad
\leftcomplementary{(-)}\circ \functorco{F}
\quad
:
\quad
\Bcategory_1^{\,op(0,1)} \quad \morph{} \quad \Acategory_2$$
on the object~$\functor{F}(\leftcomplementary{b})$
in order to get the object~$\leftcomplementary{(\functorco{F}(b))}$.
%
%Recall that the notion of mate was introduced by Street
%in his seminal work on formal monads~\cite{street:formal-monads}.
%


\paragraph{The 2-dimensional cells.}
%
A 2-dimensional cell in $\HeliChir$
$$
\theta \quad : \quad F \Rightarrow G \quad : \quad 
(\Acategory_1,\Bcategory_1) \quad \morph{} \quad (\Acategory_2,\Bcategory_2)
$$
is defined in exactly the same way as a 2-dimensional cell in the 2-category~$\DialogueChiralities$
of dialogue chiralities constructed in~\cite{mellies:tensorial-logic-2}.
%
It is a pair~$(\naturaltransformation{\theta},\naturaltransformationco{\theta})$
of monoidal natural transformations $\naturaltransformation{\theta}:\functor{F}\Rightarrow \functor{G}$
and $\naturaltransformationco{\theta}:\functorco{G}\Rightarrow \functorco{F}$
satisfying the two equations below:
%
\begin{equation}\label{equation/refraction-chiralities/two-cells-one}
\begin{array}{ccc}
\hspace{-1em}
\vcenter{
\xymatrix @-2pc {
&&&&&&&
\ar@{=>}[dd]^-{\naturaltransformation{\theta}}
&&&&&&&
\\
\Acategory_1 
\ar@/^1.4pc/[rrrrrrrrrrrrrr]^-{\functor{F}}
\ar@/_1.6pc/[rrrrrrrrrrrrrr]_-{\functor{G}}
\ar[dddddddd]_-{\rightcomplementary{(-)}}
&&&&&&&&&&&&&&
\Acategory_2
\ar[dddddddd]^-{\rightcomplementary{(-)}}
\\
&&&&&&&
\\
\\
\\
%\ar@{}[rrrrrrrrrrrrrrrrdddd]|-{\functorcell{G}}
\\
&&&&&&
&&&&&&&
\ar@{=>}@/_.7pc/[dddlll]_-{\functorcell{G}}
&
\\
\\
&&&&&&&&&&&&&&
\\
\Bcategory_1^{\, op(0,1)}
\ar@/_1.4pc/[rrrrrrrrrrrrrr]_-{\functorco{G}^{\, op(0,1)}}
&&&&&&&
&&&&&&& \Bcategory_2^{\, op(0,1)}
}}
&
= 
&
\vcenter{
\xymatrix @-2pc {
\Acategory_1 
\ar@/^1.4pc/[rrrrrrrrrrrrrr]^-{\functor{F}}
\ar[dddddddd]_-{\rightcomplementary{(-)}}
&&&&&&&&&&&&&&
\Acategory_2
\ar[dddddddd]^-{\rightcomplementary{(-)}}
\\
&&&&&&&
\\
&&&&&&
&&&&&&&
\ar@{=>}@/_.7pc/[dddlll]_-{\functorcell{F}}
&
\\
\\
%\ar@{}[rrrrrrrrrrrrrrrrdddd]|-{\functorcell{G}}
\\
&&&&&&
&&&&&&&
\\
\\
&&&&&&&
\ar@{=>}[dd]^-{\naturaltransformationco{\theta}^{\, op(0,1)}}
&&&&&&&
\\
\Bcategory_1^{\, op}
\ar@/^1.4pc/[rrrrrrrrrrrrrr]^-{\functorco{F}^{\, op(0,1)}}
\ar@/_1.6pc/[rrrrrrrrrrrrrr]_-{\functorco{G}^{\, op(0,1)}}
&&&&&&&
&&&&&&&
\Bcategory_2^{\, op(0,1)}
\\
&&&&&&&
}}
\end{array}
\end{equation}
%
\begin{equation}\label{equation/special-refraction-chiralities/two-cells-two}
\begin{array}{ccc}
\vcenter{
\xymatrix @-2.1pc {
\Acategory_1 \ar[rrrrrrrrrrrrrrrr]^-{\functor{F}}
&&&&&&&&&&&&&&&&
\Acategory_2
\\
&&&&&&&&
&&&& 
\ar@{=>}@/_.7pc/[dddrrr]_-{\functorcellbracketspecial{F}}
&&&
\\
\\
\\
&&&&&&&&
&&&&&&&
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Bcategory_1 \ar[rrrrrrrrrrrrrrrr]_-{\functorco{F}}
\ar[uuuuuuuu]^-{R}
&&&&&&&&
&&&&&&&&
\Bcategory_2
\ar[uuuuuuuu]_-{R}
}}
&
\quad
=
\quad
&
\vcenter{\xymatrix @-2.1pc {
&&&&&&&&
\ar@{=>}[ddddd]^-{\naturaltransformation{\theta}}
\\
\\
\\
&&&&&&&&
\\
&&&&&&&&
\\
\Acategory_1
\ar@/^2.2pc/[rrrrrrrrrrrrrrrr]^-{\functor{F}}
\ar[rrrrrrrrrrrrrrrr]_-{\functor{G}}
&&&&&&&&&&&&&&&&
\Acategory_2
\\
&&&&&&&&
&&&&
\ar@{=>}@/_.7pc/[dddrrr]_-{\functorcellbracketspecial{G}}
&&&
\\
\\
\\
&&&&&&&&
&&&&&&&
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&
\\
\Bcategory_1
\ar[rrrrrrrrrrrrrrrr]^-{\functorco{G}}
\ar@/_2.2pc/[rrrrrrrrrrrrrrrr]_-{\functorco{F}}
\ar[uuuuuuuu]^-{R}
&&&&&&&&
\ar@{=>}[dddd]^-{\naturaltransformationco{\theta}}
&&&&&&&&
\Bcategory_2
\ar[uuuuuuuu]_-{R}
\\
\\
\\
\\
&&&&&&&
&&&&&&&
}}
\end{array}
\end{equation}
As in the case of the 2-category~$\HeliCat$ in \S\ref{section/a-2-category-of-helical-dialogue-categories},
we let the reader check that the expected notions of (horizontal and vertical) identity and composition
define a 2-category $\HeliChir$ together with a forgetful 2-functor
$$
U' \quad : \quad \HeliChir \quad \morph{} \quad \DialogueChiralities
$$
to the 2-category~$\DialogueChiralities$ of dialogue chiralities
constructed in~\cite{mellies:tensorial-logic-2}.
%
As in the case of the forgetful 2-functor from~$\HeliCat$
in \S\ref{section/a-2-category-of-helical-dialogue-categories},
the forgetful 2-functor~$U$ is fully faithful on 2-dimensional cells.

%\section{Equivalence between $\HeliCat$ and $\HeliChir$}
\section{Construction of the 2-categorical equivalence}
%Equivalence between $\HeliCat$ and $\HeliChir$}
% categories and chiralities}
\label{section/biequivalence-between-the-2-categories}
%
In this section, we show that the 2-categories $\HeliCat$ and~$\HeliChir$
are equivalent in the appropriate 2-dimensional sense.
%
The construction is a direct adaptation of the 2-dimensional
equivalence between $\Dial$ and $\DialogueChiralities$ 
exhibited in our companion paper~\cite{mellies:tensorial-logic-2}.
%
So, it is not particularly difficult, but it should done with great care.
%
%
%\medbreak
%
In the same way as in the original case of dialogue categories,
the equivalence may be understood as a coherence theorem
for helical dialogue chiralities.
%
In particular, it provides a general recipe to strictify a helical dialogue chirality
into an equivalent helical dialogue category.
%in the 2-category~$\HeliChir$.
Recall that a dialogue chirality~$(\Acategory,\Bcategory)$
is called \emph{strict} when $\Bcategory=\Acategory^{\,op(0,1)}$
and moreover, the two functors~$\leftcomplementary{(-)}$ and $\rightcomplementary{(-)}$
and their monoidal equivalence are trivial --- that is, equal to the identity on~$\Acategory$.

\subsection{From dialogue categories to dialogue chiralities}
We start by constructing a 2-functor 
$$
\Ftwofunctor \quad : \quad \HeliCat \quad \morph{} \quad \HeliChir
$$
from the 2-category~$\HeliCat$ of helical dialogue categories
to the 2-category $\DialogueChiralities$ of helical dialogue chiralities.

\paragraph{Definition of $\Ftwofunctor$ : the 0-dimensional cells.}
%\paragraph{[$\, \mathbf{\Ftwofunctor}\, $]\, the 0-dimensional cells.}
%\paragraph{$\Ftwofunctor\, \rhd$ the 0-dimensional cells.}
To every helical dialogue category~$\Ccategory$, the 2-functor
$\Ftwofunctor$ associates the helical dialogue chirality defined 
in exactly the same way as in the case of basic dialogue categories:
$$
(\Acategory,\tensorialand,\tensorialtrue)
\hspace{.5em} := \hspace{.5em}  (\Ccategory,\otimes,\tensorialunit)
\quad\quad\quad\quad
(\Bcategory,\tensorialor,\tensorialfalse)
\hspace{.5em}  := \hspace{.5em}  (\Ccategory,\otimes,\tensorialunit)^{op(0,1)}.
$$
The monoidal equivalence between $\Acategory$
and $\Bcategory^{op(0,1)}$ is defined as the identity functor
on the monoidal category~$\Ccategory$.
%, since
%$$
%\Acategory \quad = \quad \Ccategory \quad = \quad \Bcategory^{op(0,1)}.
%$$
%
The two adjoint functors~$L$ and~$R$ are defined as
$$\leftadjoint:x\mapsto \bot\rightpop x
\quad\quad\quad\quad
\rightadjoint: x\mapsto x\leftpop\bot$$
%
with the adjunction~$L\dashv R$ witnessed by the series of bijections
$$
\begin{array}{ccc}
\Acategory(x, \rightadjoint(y))
& \quad = \quad &
\Ccategory(x, y\leftpop\bot) 
\\
& \quad \cong \quad &
\Ccategory(y\tensor x,\bot)
\\
& \quad \cong \quad &
\Ccategory(y,\bot\rightpop x)
\\
& \quad = \quad &
\Bcategory(\leftadjoint(x),y)
\end{array}
$$
natural in~$x$ and~$y$.
%
The bijection~$\currify{m}{x}{y}$ is defined as the composite
$$
\xymatrix @-.3pc {
\Ccategory(m\tensor x, y\leftpop\bot)
\ar[rr]^-{\varphi^{-1}_{x\tensor m,y}}
&&
\Ccategory(y\tensor m\tensor x,\bot)
%\ar[rrrr]^-{associativity}
%&&&&
%\Ccategory((y\tensor m)\tensor x,\bot)
\ar[rr]^-{\varphi_{y\tensor m,x}}
&&
\Ccategory(x,(y\tensor m)\leftpop\bot)}
$$
where for simplicity, we forget the associativity map
between $y\tensor(m\tensor x)$ and $(y\tensor m)\tensor x$.
%
Up to that stage, the 2-functor~$\Ftwofunctor$ is defined in exactly the same way
in the original case of dialogue categories, see~\cite{mellies:tensorial-logic-2} for details.
%
This already ensures that the data introduced for~$(\Acategory,\Bcategory)$ define
a dialogue chirality.
%
The only novelty is the definition of the helical structure
$$\xymatrix @-1.6pc {
\distributor{a}{b}
=
\Acategory(a,Rb)
=
\Ccategory(a,b\leftpop\bot)
&\ar[rrrr]^-{\helix_{a,b}}
&&&&
&
\Ccategory(b,a\leftpop\bot)
=
\Acategory(\leftcomplementary{b},R\rightcomplementary{a})
=
\distributor{\leftcomplementary{b}}{\rightcomplementary{a}}
}$$
as the natural family of isomorphisms
$$
\xymatrix @-1.2pc {
\Ccategory(a,b\leftpop\bot)
\ar[rrr]^-{\varphi^{-1}_{b,a}}
&&&
\Ccategory(b\tensor a,\bot)
\ar[rrrr]^-{\RefutationCycle{a}{b}^{-1}}
&&&&
\Ccategory(a\tensor b,\bot)
\ar[rrr]^-{\varphi_{a,b}}
&&&
\Ccategory(a,b\leftpop\bot)
}
$$
%
It is not difficult to check that this defines a helical dialogue chirality~$(\Acategory,\Bcategory)$.
%
The point is that the two coherence diagrams~(\ref{equation/coherence-dialogue-wheel})
for dialogue categories and~(\ref{equation/coherence-diagram-helix}) for dialogue chiralities
essentially coincide.
%FACT-TO-CHECK-NUMBER-1
%Note that 
%$$\distributor{\leftcomplementary{b}}{\rightcomplementary{a}}=
%\Acategory(\leftcomplementary{b},R\rightcomplementary{a})=
%\Ccategory(b,a\leftpop\bot)
%\quad\quad\quad\quad
%\distributor{a}{b}=\Acategory(a,Rb)=\Ccategory(a,b\leftpop\bot)$$
%
%It is not difficult to deduce from the naturality 
%of the family~$\currifyalone$ that it satisfies
%Equation~(\ref{equation/coherence/currify-one-dialogue})
%and~(\ref{equation/coherence/currify-two})
%required by the notion of refraction chirality.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\blackhole{This follows from
$$
\xymatrix @-1.2pc {
\Ccategory(x\tensor (m\tensor n),\bot\rightpop y)
\ar[rrrr]^-{\currifyone{m\otimes n}} \ar[dd]|-{associativity}
&&&& 
\Ccategory(x,\bot \rightpop (m\tensor n)\tensor y)
\\
\\
\Ccategory((x\tensor m)\tensor n,\bot\rightpop y)
\ar[rr]^-{\currifyone{n}}
&&
\Ccategory(x\tensor m,\bot\rightpop n\tensor y)
\ar[rr]^-{\currifyone{m}}
&&
\Ccategory(x,\bot\rightpop m\tensor (n\tensor y))
\ar[uu]|-{associativity}
}
$$
commutes. This comes from the fact that MacLane's pentagon
$$
\xymatrix @-.9pc {
(x\tensor (m\tensor n))\tensor y
\ar[rrrr]
&&&& 
x\tensor ((m\tensor n)\tensor y)
\ar[dd]
\\
\\
((x\tensor m)\tensor n)\tensor y
\ar[rr]\ar[uu]
&&
(x\tensor m)\tensor (n\tensor y)
\ar[rr]
&&
x\tensor(m\tensor(n\tensor y))
}
$$
commutes in the monoidal category~$\Ccategory$,
together with naturality of the family of bijections~$\psi$.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{Definition of $\Ftwofunctor$ : the 1-dimensional cells.}
%\paragraph{The 1-dimensional cells.}
To every dialogue functor
$$
(F,\dialoguefunctorcell{F}) \quad : \quad (\Ccategory,\bot_{\Ccategory}) \quad \morph{} \quad
(\Dcategory,\bot_{\Dcategory})
$$
the 2-functor~$\Ftwofunctor$ associates the 1-dimensional cell
$\Ftwofunctor(F)$
defined as the quadruple consisting of the lax monoidal functor
$$
\functor{\Ftwofunctor(F)} 
\hspace{.4em} : \hspace{.4em} \Ccategory
\hspace{.4em}\morph{F} \hspace{.4em} \Dcategory
$$
the oplax monoidal functor
$$
\functorco{\Ftwofunctor(F)} 
\hspace{.4em} : \hspace{.4em} \Ccategory^{\, op(0,1)} \hspace{.4em}
\morph{F^{\, op(0,1)}} \hspace{.4em} \Dcategory^{\, op(0,1)}
$$
the monoidal isomorphism~$\functorcell{\Ftwofunctor(F)}$
defined as the identity on the functor~$F$, and
the natural transformation
$$
\functorcellbracketspecial{\Ftwofunctor(F)} \quad : \quad
\rightadjoint \circ F
\quad \morph{} \quad
F \circ \rightadjoint
$$
whose components
$$
F(x\leftpop\bot_{\Ccategory}) 
\quad \morph{} \quad
F(x)\leftpop\bot_{\Dcategory}
$$
is associated by currification~$\varphi_{F(x),F(x\leftpop\bot_{\Ccategory})}$
to the morphism
$$
F(x)\tensor F(x\leftpop\bot_{\Ccategory})
\hspace{.3em} \morph{} \hspace{.3em}
F(x\tensor (x\leftpop\bot_{\Ccategory}))
\hspace{.3em} \morph{} \hspace{.3em}
F(\bot_{\Ccategory})
\hspace{.3em} \morph{} \hspace{.3em}
\bot_{\Dcategory}.
$$
%
We know from~\cite{mellies:tensorial-logic-2} that
this defines a 1-dimensional cell between dialogue chiralities.
%
There remains to show that $\Ftwofunctor(F)$ is compatible
with the helical structure, in the technical sense that 
diagram~(\ref{equation/additional-requirement-for-helical-1-cells}) commutes.
%
This fact is essentially immediate to deduce from the fact
that~$F$ is compatible with~$\ReflectionCycleAlone$
in the technical sense that diagram~(\ref{equation/helical-functors-compatibility}) commutes.
%FACT-TO-CHECK-NUMBER-2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{Definition of $\Ftwofunctor$ : the 2-dimensional cells.}
%\paragraph{The 2-dimensional cells.}
The 2-functor~$\Ftwofunctor$ acts on 2-cells in exactly the same way
as in the original case of dialogue categories considered in~\cite{mellies:tensorial-logic-2},
see that paper for details.
%
%We thus refer the reader to that paper for details.

\subsection{From dialogue chiralities to dialogue categories}
Now that the 2-functor~$\Ftwofunctor$ has been constructed,
we complement it with a 2-functor in the reverse direction:
$$
\Gtwofunctor \quad : \quad \HeliChir \quad \morph{} \quad \HeliCat
$$
from the 2-category
%~$\DialogueChiralities$ 
of helical dialogue chiralities
to the 2-category
%~$\Dial$ 
of helical dialogue categories.
%

\paragraph{Definition of $\Gtwofunctor$ : the 0-dimensional cells.}
%\paragraph{The 0-dimensional cells.}
The 2-functor transports every helical dialogue chirality~$(\Acategory,\Bcategory)$
to the helical dialogue category defined as
$$
(\Ccategory,\tensor,\unit) \quad := \quad (\Acategory,\tensorialand,\tensorialtrue)
$$
equipped with the tensorial pole
$$\bot \quad := \quad \rightadjoint(\tensorialfalse).
$$
together with the functors:
$$
\bot\rightpop x  
\hspace{.4em} =  \hspace{.4em} \leftcomplementary{(\leftadjoint(x))}
\quad\quad\quad\quad\quad
x\leftpop\bot 
\hspace{.4em} =  \hspace{.4em} \rightadjoint(\rightcomplementary{x}).
$$
The natural bijections~$\varphi$ and $\psi$ are then defined
by composing the series of natural bijections
$$
\begin{array}{ccccl}
\Ccategory(x\otimes y,\bot)
& = &
\Acategory(x\tensorialand y,\rightadjoint{(\tensorialfalse)})
&&
\mbox{by definition of~$\Ccategory$ and of~$\bot$,}
\\
& \cong &
\Acategory(y,\rightadjoint{(\rightcomplementary{x}\tensorialor\tensorialfalse)})
&&
\mbox{by applying $\currify{x}{y}{\tensorialfalse}$,}
\\
& \cong &
\Acategory(y,\rightadjoint{({\rightcomplementary{x}})})
&&
\mbox{by applying the unit law in~$\Bcategory$,}
\\
& \cong &
\Bcategory(\leftadjoint{(y)}, {\rightcomplementary{x}})
&&
\mbox{by the adjunction~$\leftadjoint{}\dashv\rightadjoint{}$,}
\\
& \cong &
\Acategory(x, {\leftcomplementary{(\leftadjoint{(y)})}})
&&
\mbox{by the adjunction~$\rightcomplementary{(-)}\dashv\leftcomplementary{(-)}$,}
\\
& = & 
\Ccategory(x, {\leftcomplementary{(\leftadjoint{(y)})}})
&&
\mbox{by definition of~$\Ccategory$.}
\end{array}
$$
$$
\begin{array}{ccccl}
\Ccategory(x\otimes y,\bot)
& = &
\Acategory(x\tensorialand y, \rightadjoint{(\tensorialfalse)})
&&
\mbox{by definition of~$\Ccategory$ and of~$\bot$,}
\\
& \cong & 
\Acategory(y,\rightadjoint{(\rightcomplementary{x}\tensorialor\tensorialfalse)})
&& 
\mbox{by applying $\currify{x}{y}{\tensorialfalse}$,}
\\
& \cong & 
\Acategory(y, \rightadjoint{({\rightcomplementary{x}})})
&&
\mbox{by applying the unit law in~$\Bcategory$,}
\\
& = & 
\Ccategory(y, \rightadjoint{({\rightcomplementary{x}})})
&&
\mbox{by definition of~$\Ccategory$.}
\end{array}
$$
%
The helical structure~$\ReflectionCycleAlone$ on the dialogue category~$\Ccategory$
is defined as the composite of natural bijections:
$$
\xymatrix @-1pc {
\Ccategory(x\tensor y,\bot)
\ar[rrrrrrr]^-{\ReflectionCycle{x}{y}}
\ar[dd]_-{\varphi_{x,y}}
&&&&&&&
\Ccategory(y\tensor x,\bot)
\\
\\
\Ccategory(y,x\leftpop\bot)
\ar@{=}[rr]
&&
\distributor{\leftcomplementary{y}}{\rightcomplementary{x}}
\ar[rrr]^-{\helix_{x,y}^{-1}}
&&&
\distributor{x}{y}
\ar@{=}[rr]
&&
\Ccategory(x,y\leftpop\bot)
\ar[uu]_-{\varphi^{-1}_{y,x}}
}
$$
The fact that this defines a helical structure is essentially immediate:
the reason already mentioned is that
the two coherence diagrams~(\ref{equation/coherence-dialogue-wheel})
for dialogue categories and~(\ref{equation/coherence-diagram-helix}) for dialogue chiralities
essentially coincide modulo translation of one into the other.
%FACT-TO-CHECK-NUMBER-3

\paragraph{Definition of $\Gtwofunctor$ : the 1-dimensional cells.}
%\paragraph{The 1-dimensional cells.}
Every 1-dimensional cell
$$F=(\functor{F},\functorco{F},\functorcell{F},\functorcellbracketspecial{F})
\quad : \quad 
(\Acategory_1,\Bcategory_1) 
\quad \morph{} \quad 
(\Acategory_2,\Bcategory_2) 
$$
is transported to the dialogue functor $(\functor{F},\dialoguefunctorcell{F})$
consisting of the functor
$$
\functor{F} \quad : \quad \Acategory_1 \quad \morph{} \quad \Acategory_2
$$
and of the morphism
$$
\dialoguefunctorcell{F} \quad : \quad
\functor{F}(\bot_{\Acategory_1})
\quad
\morph{}
\quad
\bot_{\Acategory_2}
$$
defined as the composite
$$
\xymatrix{
\functor{F}\circ\rightadjoint \, (\tensorialfalse)
\ar[rr]^-{\functorcellbracketspecial{F}_{\tensorialfalse}}
&&
\rightadjoint \circ \functorco{F} \, (\tensorialfalse)
\ar[rrr]^-{monoidality}
&&&
\rightadjoint \, (\tensorialfalse)
}
$$
%
There remains to show that $\Gtwofunctor(F)=\functor{F}$ is compatible
with the wheel structure, in the technical sense that 
diagram~(\ref{equation/helical-functors-compatibility}) commutes.
%
This fact is essentially immediate to deduce from the diagram chase below:
$$
\xymatrix @-1pc {
\Ccategory(x\tensor y,\bot)
\ar@{}[rrrrrdd]|-{(a)} 
\ar[rr]^-{F} 
\ar[dd]_-{\psi_{x,y}}
&& 
\Dcategory(F(x\tensor y),\bot)\ar[rrr]^-{coercion} &&&
\Dcategory(F(x)\tensor F(y),\bot)\ar[dd]^-{\psi_{Fx,Fy}}
\\
\\
\Ccategory(x,\bot\rightpop y)\ar[rr]^-{F}
\ar[dd]_-{\helix_{x,y}^{-1}}
\ar@{}[rrrrrdd]|-{(b)} 
 && 
\Dcategory(Fx,F(\bot\rightpop y)) \ar[rrr]^-{} &&&
\Dcategory(Fx,\bot\rightpop Fy)
\ar[dd]^-{\helix_{Fx,Fy}^{-1}}
\\
\\
\Ccategory(y,\bot\rightpop x)\ar[rr]^-{F}
\ar[dd]_-{\psi^{-1}_{y,x}}
\ar@{}[rrrrrdd]|-{(c)} 
&& 
\Dcategory(Fy,F(\bot\rightpop x)) \ar[rrr]^-{} &&&
\Dcategory(Fy,\bot\rightpop Fx)
\ar[dd]^-{\psi^{-1}_{Fy,Fx}}
\\
\\
\Ccategory(y\tensor x,\bot)\ar[rr]^-{F} && 
\Dcategory(F(y\tensor x),\bot)\ar[rrr]^-{coercion} &&& 
\Dcategory(F(y)\tensor F(x),\bot)
}
$$
whose hexagons~$(a)$ and~$(c)$ commute in every dialogue category,
and whose inner hexagon~$(b)$ commutes because 
diagram~(\ref{equation/additional-requirement-for-helical-1-cells}) commutes.
%
%FACT-TO-CHECK-NUMBER-4



\paragraph{Definition of $\Gtwofunctor$ : the 2-dimensional cells.}
%\paragraph{The 2-dimensional cells.}
The 2-functor~$\Gtwofunctor$ acts on 2-dimensional cells in exactly the same way
as in the original case of dialogue categories considered in~\cite{mellies:tensorial-logic-2}.
%
We refer the reader to that paper for details.
%
We simply recall here that every 2-dimensional cell $\theta=(\naturaltransformation{\theta},
\naturaltransformationco{\theta})$ is transported to the  dialogue transformation
$\naturaltransformation{\theta}$.
%

%


\subsection{The pseudo-natural transformation~$\Phi$}\label{section/definition-of-Phi}
The composite 2-functor
$$\HeliCat \quad \morph{\Ftwofunctor} \quad \HeliChir 
\quad \morph{\Gtwofunctor} \quad \HeliCat$$
coincides with the identity on the 2-category~$\HeliCat$ of helical dialogue categories.
%
In order to establish that $\HeliCat$ and $\HeliChir$ are biequivalent,
we construct a pair of pseudo-natural transformations
$$
\Phi \hspace{.5em} : \hspace{.5em} Id \hspace{.5em} \morph{}
\hspace{.5em} \Ftwofunctor\circ\Gtwofunctor
\quad\quad\quad\quad
\Psi \hspace{.5em} : \hspace{.5em} 
\Ftwofunctor\circ\Gtwofunctor
\hspace{.5em} \morph{} Id
$$
between the identity 2-functor on $\HeliChir$ and the 2-functor~$\Ftwofunctor\circ\Gtwofunctor$.
%
We then show that their components
$\Phi_{(\Acategory,\Bcategory)}$
and
$\Psi_{(\Acategory,\Bcategory)}$ define
an equivalence in the 2-category $\DialogueChiralities$,
for every helical dialogue chirality~$(\Acategory,\Bcategory)$.
%
Before proceeding further, we find convenient to give a detailed account
of the helical dialogue chirality~$(\Acategory,\Acategory^{\, op(0,1)})$
obtained by applying the 2-functor $\Ftwofunctor\circ\Gtwofunctor$
to a given dialogue chirality~$(\Acategory,\Bcategory)$.
%
The dialogue chirality~$(\Acategory,\Acategory^{\, op(0,1)})$
is equipped with the trivial monoidal equivalence:
$$
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{id}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{id}
&
(\Acategory^{\, op(0,1)})^{\, op(0,1)}}
$$
with the adjunction
$$
\xymatrix @-1.4pc {
&&&&
\\
\Acategory
&
\ar@/^1pc/[rrrr]^-{\leftadjoint}
\ar@{}[rrrr]|-{\bot}
&&&&
\ar@/^1pc/[llll]^-{\rightadjoint}
&
\Bcategory
&
\ar@/^1pc/[rrrr]^-{(\leftcomplementary{(-)})^{\, op(0,1)}}
\ar@{}[rrrr]|-{\bot}
&&&&
\ar@/^1pc/[llll]^-{(\rightcomplementary{(-)})^{\, op(0,1)}}
&
\Acategory^{\, op(0,1)}
}
$$
From this follows that
$$
\distributor{a_1}{a_2}_{(\Acategory,\Acategory^{\, op(0,1)})} \quad = \quad
\Acategory(a_1,\rightadjoint \, (\rightcomplementary{a_2}))
\quad = \quad
\distributor{a_1}{\rightcomplementary{a_2}}_{(\Acategory,\Bcategory)}
$$
The natural transformation
$\currifyalone_{(\Acategory,\Acategory^{\, op(0,1)})}$
at instance $(m,a,b)$ is defined as the composite function
$$
\xymatrix @-.5pc {
\distributor{m\tensorialand a_1}{\rightcomplementary{a_2}}
\ar[d]
&&&
\distributor{a_1}{\rightcomplementary{(a_2 \tensorialand m)}}
\\
\distributor{m\tensorialand a_1}{\rightcomplementary{a_2}\tensorialor\tensorialfalse}
\ar[d]_-{(\currifyalone_{(\Acategory,\Bcategory)})^{-1}}
&&&
\distributor{a_1}{\rightcomplementary{(a_2\tensorialand m)}\tensorialor\tensorialfalse}
\ar[u]
\\
\distributor{a_2\tensorialand (m\tensorialand a_1)}{\tensorialfalse}
\ar[rrr]
&&&
\distributor{(a_2\tensorialand m)\tensorialand a_1}{\tensorialfalse}
\ar[u]_-{\currifyalone_{(\Acategory,\Bcategory)}}
}
$$
Similarly, the dialogue chirality~$\Gtwofunctor\circ\Ftwofunctor(\Acategory,\Bcategory)$
has helical structure defined as
$$
\xymatrix @-.3pc {
\distributor{a_1}{\rightcomplementary{a_2}}_{(\Acategory,\Bcategory)}
\ar[rrr]^-{\helix_{a_1,\rightcomplementary{a_2}}}
&&&
\distributor{\leftcomplementary{(\rightcomplementary{a_2})}}{\rightcomplementary{a_1}}_{(\Acategory,\Bcategory)}
\ar[rrr]^-{equivalence}
&&&
\distributor{a_2}{\rightcomplementary{a_1}}_{(\Acategory,\Bcategory)}
}
$$
where~$\helix$ is the helical structure of the original dialogue chirality~$(\Acategory,\Bcategory)$.
%

\medbreak

After this detailed description of the ``strictified'' version $\Gtwofunctor\circ\Ftwofunctor(\Acategory,\Bcategory)$
obtained from the helical dialogue chirality~$(\Acategory,\Bcategory)$, we are ready to introduce
the pseudo-natural transformations~$\Phi$ and~$\Psi$.
%
The construction is exactly the same as for dialogue chiralities in~\cite{mellies:tensorial-logic-2}.
%
Our main concern is thus to check that the constructions are compatible with the helical structures
of the original dialogue chirality~$(\Acategory,\Bcategory)$ and of its strictified version.
%
\paragraph{The 1-dimensional cells $\Phi_{(\Acategory,\Bcategory)}$.}
%
Recall from~\cite{mellies:tensorial-logic-2} that to every dialogue chirality~$(\Acategory,\Bcategory)$
one associates the $1$-cell
$$\Phi_{(\Acategory,\Bcategory)}
\quad : \quad (\Acategory,\Bcategory) \quad \morph{} \quad
(\Acategory,\Acategory^{\, op(0,1)})$$
defined as the pair of monoidal functors
$$
\xymatrix @-1.7pc {
\functor{(\Phi_{(\Acategory,\Bcategory)})}
& : & 
\Acategory
\ar[rrrr]^-{id}
&&&& \Acategory
&&&&&
\functorco{(\Phi_{(\Acategory,\Bcategory)})}
& : & 
\Bcategory \ar[rrrrrrr]^-{(\leftcomplementary{(-)})^{\, op(0,1)}} 
&&&&&&&
\Acategory^{\, op(0,1)}}
$$
together with the monoidal natural isomorphism
$$
\begin{array}{ccc}
\functorcell{\Phi_{(\Acategory,\Bcategory)}}
& \quad = \quad &
\vcenter{\xymatrix @-2.05pc {
\Acategory \ar[rrrrrrrrrrrrrrrr]^-{id}
\ar[dddddddd]_-{\rightcomplementary{(-)}}
%\ar@{}[rrrrrrrrrrrrrrrrdddddddd]|-{\eta}
&&&&&&&&&&&&&&&&
\Acategory
\ar[dddddddd]^-{id}
\\
\\
\\
\\
&&&&&&&&
&&&&&&&
\ar@{=>}@/_.7pc/[dddlll]_-{\underline{\eta}}
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Bcategory^{\, op(0,1)} \ar[rrrrrrrrrrrrrrrr]_-{\leftcomplementary{(-)}}
&&&&&&&&
&&&&&&&& (\Acategory^{\, op(0,1)})^{\, op(0,1)}
}}
\end{array}
$$
and the natural transformation
$$
\begin{array}{ccc}
\functorcellbracketspecial{\Phi_{(\Acategory,\Bcategory)}}
&
\quad 
= 
\quad
&
\vcenter{\xymatrix @-2.05pc {
\Acategory \ar[rrrrrrrrrrrrrrrr]^-{id}
&&&&&&&&&&&&&&&&
\Acategory
\\
&&&&&&&&
&&&&
\ar@{=>}@/_.7pc/[dddrrr]_-{\underline{\varepsilon}^{\, op(0,1)}}
&&&
\\
\\
\\
&&&&&&&&
&&&&&&&&
\Bcategory\ar[uuuu]_-{R}
\\
&&&&&&&&
&&&&&&&&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Bcategory \ar[rrrrrrrrrrrrrrrr]_-{(\leftcomplementary{(-)})^{\, op(0,1)}}
\ar[uuuuuuuu]^-{R}
&&&&&&&&
&&&&&&&&
\Acategory^{\, op(0,1)}
\ar[uuuu]_-{(\rightcomplementary{(-)})^{\, op(0,1)}}
}}
\end{array}
$$
where $\underline{\eta}$ and $\underline{\varepsilon}$ denote the unit and counit
of the adjunction $\rightcomplementary{(-)}\dashv\leftcomplementary{(-)}$.
%
We know from~\cite{mellies:tensorial-logic-2} that~$\Phi$ defines a 1-dimensional cell
between the dialogue chirality~$(\Acategory,\Bcategory)$ and its strictified version.
%
There remains to check that this 1-dimensional cell is compatible
with the helical structures of the two dialogue chiralities.
%
Technically speaking, this simply means that
the coherence diagram~(\ref{equation/additional-requirement-for-helical-1-cells})
commutes when instantiated as follows:
$$
\xymatrix @-.6pc {
\distributor{a}{b}
\ar[rrrrrr]^-{\Phi_{a,b}}
\ar[dd]_-{\helix_{a,b}}
&&&&&&
\distributor{a}{\rightcomplementary{(\leftcomplementary{b})}}
\ar[d]^-{\helix_{a,\rightcomplementary{(\leftcomplementary{b})}}}
\\
&&&&&&
\distributor{\leftcomplementary{(\rightcomplementary{(\leftcomplementary{b})})}}{\rightcomplementary{a}}
\ar[d]^-{equivalence}
\\
\distributor{\leftcomplementary{b}}{\rightcomplementary{a}}
\ar[rrr]^-{\Phi_{\leftcomplementary{b},\rightcomplementary{a}}}
&&&
\distributor{\leftcomplementary{b}}{\rightcomplementary{(\leftcomplementary{(\rightcomplementary{a})})}}
\ar[rrr]^-{\functorcell{\Phi}_{\leftcomplementary{b},\rightcomplementary{a}}}
&&&
\distributor{\leftcomplementary{b}}{a}}
$$
We leave the reader check that this diagram commutes 
by naturality of~$\helix$ and because all the bijections
(except for the two instantiations of $\helix$) involved in it are deduced from the equivalence
$\rightcomplementary{(-)}\dashv\leftcomplementary{(-)}$.

%
%Once commutativity of~(\ref{equation/currification-comparison})
%established, one easily checks that this definition of $\Phi_{(\Acategory,\Bcategory)}$
%makes the diagram~(\ref{equation/coherence-diagram/spref-1-cells})
%commute, and thus provides a valid definition of a 1-cell in the 2-category~$\DialogueChiralities$.
%FACT-TO-CHECK-NUMBER-5

\paragraph{The 2-dimensional cells $\Phi_{F}$.}
Are constructed just as the 2-dimensional cells $\Phi_{F}$ in~\cite{mellies:tensorial-logic-2}.
From this follows that each of them defines a 2-cell in the 2-category $\HeliChir$
and that the family~$\Phi$ itself defines a pseudo-natural transformation.
%

\subsection{The pseudo-natural transformation $\Psi$}\label{section/definition-of-Psi}
\paragraph{The 1-dimensional cells $\Psi_{(\Acategory,\Bcategory)}$.}
To every dialogue chirality $(\Acategory,\Bcategory)$,
one associates the 1-cell $\Psi_{(\Acategory,\Bcategory)}$ 
%adjoint to the 1-cell $\Phi_{(\Acategory,\Bcategory)}$.
%
defined as the pair of functors
$$
\functor{(\Psi_{(\Acategory,\Bcategory)})}
\hspace{.4em} : \hspace{.4em} 
\Acategory \hspace{.4em} \morph{id} \hspace{.4em} \Acategory
\quad\quad\quad
\functorco{(\Psi_{(\Acategory,\Bcategory)})} \hspace{.4em}  : \hspace{.4em}
\Acategory^{\, op(0,1)}
\quad \morph{(\rightcomplementary{(-)})^{\, op(0,1)}} \quad 
\Bcategory
$$
equipped with the trivial monoidal natural isomorphism
$$
\begin{array}{ccc}
\functorcell{\Psi_{(\Acategory,\Bcategory)}}
&
\quad = \quad
&
\vcenter{\xymatrix @-1.95pc {
\Acategory \ar[rrrrrrrrrrrrrrrr]^-{id}
\ar[dddddddd]_-{id}
%\ar@{}[rrrrrrrrrrrrrrrrdddddddd]|-{\eta}
&&&&&&&&&&&&&&&&
\Acategory
\ar[dddddddd]^-{\rightcomplementary{(-)}}
\\
\\
\\
\\
&&&&&&&&
&&&&&&&
\ar@{=>}@/_.7pc/[dddlll]_-{id}
&
\\
&&&&&&&&
&&&&&&&
&
\\
\\
&&&&&&&&&&&&&&&&
\\
(\Acategory^{\, op(0,1)})^{\, op(0,1)}
\ar[rrrrrrrrrrrrrrrr]_-{\rightcomplementary{(-)}}
&&&&&&&&
&&&&&&&& \Bcategory^{\, op(0,1)}}}
\end{array}
$$
and with the trivial natural transformation
$$
\begin{array}{ccc}
\functorcellbracketspecial{\Psi_{(\Acategory,\Bcategory)}}
&
\quad 
= 
\quad
&
\vcenter{\xymatrix @-1.95pc {
\Acategory \ar[rrrrrrrrrrrrrrrr]^-{id}
&&&&&&&&&&&&&&&&
\Acategory
\\
&&&&&&&&
&&&&
\ar@{=>}@/_.7pc/[dddrrr]_-{id}
&&&
\\
\\
\\
\Bcategory\ar[uuuu]^-{R}
&&&&&&&&
&&&&&&&&
\\
&&&&&&&&
&&&&&&&&
\\
\\
&&&&&&&&&&&&&&&&
\\
\Acategory^{\, op(0,1)}
\ar[uuuu]^-{(\rightcomplementary{(-)})^{\, op(0,1)}}
\ar[rrrrrrrrrrrrrrrr]_-{(\rightcomplementary{(-)})^{\, op(0,1)}}
&&&&&&&&
&&&&&&&&
\Bcategory \ar[uuuuuuuu]_-{R}
}}
\end{array}
$$
%
We know from~\cite{mellies:tensorial-logic-2} that~$\Psi$
defines a 1-dimensional cell between the dialogue chirality~$(\Acategory,\Bcategory)$
and its strictified version.
%
So, just as in the case of the 1-dimensional cell~$\Phi$ in \S\ref{section/definition-of-Psi},
we only need to check that this 1-dimensional cell~$\Psi$
is compatible with the helical structures of the two dialogue chiralities.
%
The coherence diagram~(\ref{equation/additional-requirement-for-helical-1-cells})
is instantiated as follows in that case:
$$
\xymatrix @-.6pc {
\distributor{a_1}{\rightcomplementary{a_2}}
\ar[rrrrrr]^-{\Psi_{a_1,a_2}}
\ar[d]_-{\helix_{a_1,\rightcomplementary{a_2}}}
&&&&&&
\distributor{a_1}{\rightcomplementary{a_2}}
\ar[dd]^-{\helix_{a_1,\rightcomplementary{a_2}}}
\\
\distributor{\leftcomplementary{(\rightcomplementary{a_2})}}{\rightcomplementary{a_1}}
\ar[d]_-{equivalence}
&&&&&&
\\
\distributor{a_2}{\rightcomplementary{a_1}}
\ar[rrr]^-{\Psi_{a_2,a_1}}
&&&
\distributor{a_2}{\rightcomplementary{a_1}}
\ar[rrr]^-{\functorcell{\Psi}_{a_2,\rightcomplementary{a_1}}}
&&&
\distributor{\leftcomplementary{(\rightcomplementary{a_2})}}{\rightcomplementary{a_1}}}
$$
where we write~$\distributor{a}{b}$ for the evaluation bracket~$\distributor{a}{b}_{(\Acategory,\Bcategory)}$
of the original dialogue chirality.
%
We leave the reader check that this diagram commutes 
because $\Psi_{a_1,a_2}$ and $\Psi_{a_2,a_1}$ are
equal to the identity, and because 
$\functorcell{\Psi}_{a_2,\rightcomplementary{a_1}}$
is obtained by applying the unit~$\underline{\eta}$
of the equivalence 
$a_2\to\leftcomplementary{(\rightcomplementary{a_2})}$
inside the evaluation bracket.



%FACT-TO-CHECK-NUMBER-6
%Just as in the case of $\Phi_{(\Acategory,\Bcategory)}$,
%it is easy to check that this definition of $\Psi_{(\Acategory,\Bcategory)}$
%makes the diagram~(\ref{equation/coherence-diagram/spref-1-cells})
%commute once commutativity of~(\ref{equation/currification-comparison})
%is established.
%
%As such, it provides a valid definition of a 1-cell 
%in the 2-category~$\DialogueChiralities$.

\paragraph{The 2-dimensional cells $\Psi_{F}$.}
Are constructed just as the 2-dimensional cells $\Psi_{F}$ in~\cite{mellies:tensorial-logic-2}.
From this follows that each of them defines a 2-cell in the 2-category $\HeliCat$
and that the family~$\Psi$ itself defines a pseudo-natural transformation.

\subsection{Coherence theorem for helical dialogue chiralities}\label{section/main-theorem}
%
We have just established that
%
%This establishes the following
%
\begin{theorem}[coherence theorem]\label{theorem/coherence/dialogue-categories}
The pair of 2-functors $\Ftwofunctor$ and $\Gtwofunctor$ defines a biequivalence
between the 2-categories $\HeliCat$ and $\HeliChir$.
\end{theorem}
%
Note that the pair of forgetful 2-functors~$U$ and~$U'$
defines a homomorphism in the appropriate 2-dimensional sense
between the biequivalences:
$$
\xymatrix @-1.8pc {
\HeliCat
\ar[dddddd]_-{U}
&\ar@/^1.2pc/[rrrrrrrr]^-{\Ftwofunctor}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
2-dim
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{\Gtwofunctor}
&
\HeliChir
\ar[dddddd]^-{U'}
\\
\\
\\
\\
\\
\\
\Dial
&\ar@/^1.2pc/[rrrrrrrr]^-{\Ftwofunctor}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
2-dim
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{\Gtwofunctor}
&
\DialogueChiralities}
$$
%where the biequivalence below  for dialogue categories and dialogue chiralities
%is studied in full details in \cite{mellies:tensorial-logic-2}.
%
This homomorphism reflects the fact that strictification of a helical dialogue chirality~$(\Acategory,\Bcategory)$
is performed in the same way in~$\HeliChir$ and in~$\DialogueChiralities$.

\section{Ambidextrous chiralities}\label{section/ambi}
%
In this section, we introduce the notion of \emph{ambidextrous chirality}
which provides the most primitive notion of dialogue chirality equipped
with a left \emph{as well as} a righthand side currification.
%
The notion is introduced in~\S\ref{section/ambidextrous-chiralities}.
%
Following our general policy, we construct in~\S\ref{section/2-category-of-ambidextrous-chiralities}
a 2-category~$\AmbiChir$ of ambidextrous chiralities.
%
We establish in~\S\ref{section/helical-ambidextrous-isomorphism}
our main result of the section, which states that the 2-category
of ambidextrous chiralities is \emph{isomorphic}
to the 2-category~$\HeliChir$ of helical dialogue chiralities.
%
This very strong correspondance provides a purely logical justification
for the topological notion of helical dialogue category.
%
\subsection{Definition}\label{section/ambidextrous-chiralities}
\begin{definition}[ambidextrous chirality]\label{definition/helical-dialogue-chirality-bis}
An ambidextrous chirality is a pair of monoidal categories
$$
(\Acategory,\tensorialand,\tensorialtrue)
\quad \quad\quad \quad
(\Bcategory,\tensorialor,\tensorialfalse)
$$
equipped with a monoidal equivalence
$$
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^-{\rightambicomplementary{(-)}}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{\leftambicomplementary{(-)}}
&
\Bcategory^{\, op(0,1)}}
$$
and with two families of bijections
$$
\rightcurrify{m}{a}{b} \quad : \quad \distributor{a\tensorialand m}{b}
\quad \morph{} \quad \distributor{a}{b\tensorialor{\rightambicomplementary{m}}}
$$
$$
\leftcurrify{m}{a}{b} \quad : \quad \distributor{m\tensorialand a}{b}
\quad \morph{} \quad \distributor{a}{{\rightambicomplementary{m}}\tensorialor b}
$$
natural in $a$, $b$ and~$m$, where the evaluation bracket is defined as
$$
\distributor{-}{-}
\quad := \quad
\dialoguedistributor{-}{-}
 \quad : \quad \Acategory^{op}\times \Bcategory 
\quad \morph{} \quad Set
$$
%
The families~$\leftcurrifyalone$ and $\rightcurrifyalone$
are required to make the three diagrams commute:
\begin{equation}\label{equation/ambidextrous-coherence-L}
\vcenter{\xymatrix @-.5pc {
\distributor{(m\tensorialand n)\tensorialand a}{b}
\ar[rrrr]^-{\leftcurrifyone{m\tensorialand n}} \ar[dd]|-{associativity}
&&&& 
\distributor{a}{\rightambicomplementary{(m\tensorialand n)}\tensorialor b}
\\
\\
\distributor{m\tensorialand (n\tensorialand a)}{b}
\ar[rr]^-{\leftcurrifyone{m}}
&&
\distributor{n\tensorialand a}{\rightambicomplementary{m}\tensorialor b}
\ar[rr]^-{\leftcurrifyone{n}}
&&
\distributor{a}{
\rightambicomplementary{n}\tensorialor(\rightambicomplementary{m}\tensorialor b)}
\ar[uu]|-{\begin{tiny}\begin{array}{c}associativity\\ monoidality\ of\ negation\end{array}\end{tiny}}
\\
}}
\end{equation}
\begin{equation}\label{equation/ambidextrous-coherence-R}
\vcenter{\xymatrix @-.5pc {
\distributor{a\tensorialand (m\tensorialand n)}{b}
\ar[rrrr]^-{\rightcurrifyone{m\tensorialand n}} \ar[dd]|-{associativity}
&&&& 
\distributor{a}{b\tensorialor{\rightambicomplementary{(m\tensorialand n)}}}
\\
\\
\distributor{(a\tensorialand m) \tensorialand n}{b}
\ar[rr]^-{\rightcurrifyone{n}}
&&
\distributor{a\tensorialand m}{b\tensorialor {\rightambicomplementary{n}}}
\ar[rr]^-{\rightcurrifyone{m}}
&&
\distributor{a}{(b\tensorialor {\rightambicomplementary{n}})
\tensorialor{\rightambicomplementary{m}}}
\ar[uu]|-{\begin{tiny}\begin{array}{c}associativity\\ monoidality\ of\ negation\end{array}\end{tiny}}
}}
\end{equation}
%
%together with the additional coherence diagram between
%$\leftcurrifyalone$ and $\rightcurrifyalone$:
%
\begin{equation}\label{equation/ambidextrous-coherence-LR}
\vcenter{\xymatrix @-.6pc {
\distributor{(m\tensorialand a)\tensorialand n}{b}
\ar[rr]^-{\rightcurrifyone{n}}
\ar@{-}[dd]|-{associativity}
&&
\distributor{m\tensorialand a}{b\tensorialor \rightambicomplementary{n}}
\ar[rr]^-{\leftcurrifyone{m}}
&&
\distributor{a}{\rightambicomplementary{m}\tensorialor (b\tensorialor \rightambicomplementary{n})}
\ar@{-}[dd]|-{associativity}
\\
\\
\distributor{m\tensorialand(a\tensorialand n)}{b}
\ar[rr]^-{\leftcurrifyone{m}}
&&
\distributor{a\tensorialand n}{\rightambicomplementary{m}\tensorialor b}
\ar[rr]^-{\rightcurrifyone{n}}
&&
\distributor{a}{(\rightambicomplementary{m}\tensorialor b)\tensorialor \rightambicomplementary{n}}
}}
\end{equation}
for all objects~$a,m,n$ of the category~$\Acategory$
and all objects~$b$ of the category~$\Bcategory$.
\end{definition}
%
The two first coherence diagrams~(\ref{equation/ambidextrous-coherence-L})
and~(\ref{equation/ambidextrous-coherence-R}) may be seen as left
and right instances of the familiar coherence diagram~(\ref{equation/coherence/currify-one-dialogue})
for left currification in dialogue chiralities.
%
The last coherence diagram~(\ref{equation/ambidextrous-coherence-LR})
requires that the left and right currification are compatible in the expected sense.
%
We will see that this last requirement has the somewhat unexpected
consequence of equipping the ambidextrous chirality with a helical structure
described in~\S\ref{section/helical-ambidextrous-isomorphism}.
%We will see that this last diagram 
%together with the additional coherence diagram between
%$\leftcurrifyalone$ and $\rightcurrifyalone$:

\subsection{The 2-category of ambidextrous chiralities}
\label{section/2-category-of-ambidextrous-chiralities}
Here, we define the 2-category~$\AmbiChir$ whose
0-dimensional cells are the ambidextrous chiralities,
and whose 1 and 2-dimensional cells are defined
as follows.

\paragraph{The 1-dimensional cells.}
%
An ambidextrous homomorphism is defined as a quadruple 
$$F=(\functor{F},\functorco{F},\functorcell{F}, \functorcellbracketspecial{F})$$
consisting of a lax monoidal functor~$\functor{F}:\Acategory_1\morph{}\Acategory_2$,
an oplax monoidal functor~$\functorco{F}:\Bcategory_1\morph{}\Bcategory_2$,
a monoidal natural isomorphism~(\ref{equation/helical-chiralities/functorcell})
and a natural isomorphism~(\ref{equation/helical-chiralities/functorcellbracketspecial})
making the diagram~(\ref{equation/refraction-chiralities/monoidal-coherence-diagram})
commute for $\currifyalone=\leftcurrifyalone$ together with the corresponding diagram
for the right currification~$\rightcurrifyalone$, given below:
%
%A helical functor is a dialogue functor
%such that the diagram below commutes:
%$$
%\xymatrix @-1.4pc {
%\distributor{a_2}{\rightcomplementary{a_1}\tensorialor b}
%\ar[rr]^-{F}
%&&
%\distributor{\functor{F}(a_2)}{\functorco{F}(\rightcomplementary{a_2}\tensorialor b)}
%\ar[rrrrr]^-{monoidality}
%&&&&&
%\distributor{\functor{F}(a_2)}{\functorco{F}(\rightcomplementary{a_1})\tensorialor \functorco{F}(b)}
%\\
%\\
%\distributor{a_1\tensorialand a_2}{b}
%\ar[rr]^-{F}
%\ar[dd]_-{\rightcurrifyone{a_2}}
%\ar[uu]^-{\leftcurrifyone{a_1}}
%&&
%\distributor{\functor{F}(a_1\tensorialand a_2)}{\functorco{F}(b)}
%\ar[rrrrr]^-{monoidality}
%&&&&&
%\distributor{\functor{F}(a_1)\tensorialand \functor{F}(a_2)}{\functorco{F}(b)}
%\ar[dd]^-{\rightcurrifyone{a_2}}
%\ar[uu]_-{\leftcurrifyone{a_1}}
%\\
%\\
%\distributor{a_1}{b\tensorialor \rightcomplementary{a_2}}
%\ar[rr]^-{F}
%&&
%\distributor{\functor{F}(a_1)}{\functorco{F}(b\tensorialor \rightcomplementary{a_2})}
%\ar[rrrrr]^-{monoidality}
%&&&&&
%\distributor{\functor{F}(a_1)}{\functorco{F}(b)\tensorialor \functorco{F}(\rightcomplementary{a_2})}
%}
%$$
\begin{equation}\label{equation/refraction-chiralities/monoidal-coherence-diagram-right}
\vcenter{\xymatrix @-1.2pc {
\distributor{a\tensorialand m}{b}
\ar[rrrr]^-{\rightcurrifyone{m}}
\ar[dd]_-{F_{a\tensorialand m,b}}
&&&&
\distributor{a}{b\tensorialor\rightambicomplementary{m}}
\ar[dd]^-{F_{a,b\tensorialor\rightambicomplementary{m}}}
\\
\\
\distributor{\functor{F}(a\tensorialand m)}{\functorco{F}(b)}
\ar[dddd]_-{\begin{tiny}monoidality\, o\hspace{-.12em}f\, \functor{F}\end{tiny}}
&&&&
\distributor{\functor{F}(a)}
{\functorco{F}(b\tensorialor\rightambicomplementary{m})}
\ar[dd]^-{\begin{tiny}monoidality\, o\hspace{-.12em}f\, \functorco{F}\end{tiny}}
\\
\\
&&&&
\distributor{\functor{F}(a)}{\functorco{F}(b)\tensorialor\functorco{F}(\rightambicomplementary{m})}
\ar[dd]^-{\functorcell{F}}
\\
\\
\distributor{\functor{F}(a)\tensorialand \functor{F}(m)}{\functorco{F}(b)}
\ar[rrrr]^-{\rightcurrifyone{\functor{F}(m)}}
&&&&
\distributor{\functor{F}(a)}{\functorco{F}(b)\tensorialor\rightambicomplementary{\functor{F}(m)}}}}
\end{equation}


\paragraph{The 2-dimensional cells.}
The 2-dimensional cells are defined in exactly the same way 
as in the 2-categories~$\DialogueChiralities$ and~$\HeliChir$.


%\subsection{An isomorphism between ambidextrous and helical}\label{section/helical-ambidextrous-isomorphism}
\subsection{An isomorphism between $\AmbiChir$ and $\HeliChir$}\label{section/helical-ambidextrous-isomorphism}
%
We establish here that
\begin{theorem}\label{proposition/helical-dialogue-chirality-alternative}
The 2-category~$\AmbiChir$ of ambidextrous chiralities is isomorphic
to the 2-category~$\HeliChir$ of helical chiralities.
%formulated in Definitions~\ref{definition/helical-dialogue-chirality}
%and~\ref{definition/helical-dialogue-chirality-bis} are equivalent.
\end{theorem}
%
To that purpose, we construct a pair of 2-functors
$$
\Ftwofunctor \hspace{.4em} :  \hspace{.4em} \AmbiChir \hspace{.4em} \morph{} \hspace{.4em} \HeliChir
\quad\quad\quad\quad
\Gtwofunctor \hspace{.4em} : \hspace{.4em} \HeliChir \hspace{.4em} \morph{} \hspace{.4em} \AmbiChir
$$
and then show that they define an isomorphism between the 2-categories.

\paragraph{Ambidextrous $\Rightarrow$ Helical.}
The 2-functor~$\Ftwofunctor$ transports every
ambidextrous chirality~$(\Acategory,\Bcategory,\leftcurrifyalone,\rightcurrifyalone)$
to the underlying dialogue chirality~$(\Acategory,\Bcategory,\currifyalone)$
with left currification~$\currifyalone=\leftcurrifyalone$.
%
The dialogue chirality is moreover equipped with the following helical structure:
$$
\xymatrix{
\distributor{a}{b}
\ar@{=}[d]
\ar[rrrr]^-{\helix_{a,b}}
&&&&
\distributor{\leftambicomplementary{b}}{\rightambicomplementary{a}}
\\
\distributor{a}{\rightambicomplementary{(\leftambicomplementary{b})}\tensorialor\tensorialfalse}
\ar[rr]^{(\leftcurrifyone{{\leftambicomplementary{b}}})^{-1}}
&&
\distributor{\leftambicomplementary{b}\tensorialand a}{\tensorialfalse}
\ar[rr]^{\rightcurrifyone{a}}
&&
\distributor{\leftambicomplementary{b}}{\tensorialfalse\tensorialor\rightambicomplementary{a}}
\ar@{=}[u]
}
$$
In order to show that the coherence diagram~(\ref{equation/coherence-diagram-helix}) commutes
in every ambidextrous chirality, we decompose it into a jigsaw of four pieces:
%
$$
\xymatrix @-1pc {
\distributor{a_2}{\rightambicomplementary{a_1}\tensorialor b}
\ar[dd]_-{(\leftcurrifyone{\leftambicomplementary{b}\tensorialand a_1})^{-1}}
&&
\ar@{}[dd]|-{(a)}
&&
\distributor{a_1\tensorialand a_2}{b}\ar[dd]^-{(\leftcurrifyone{b})^{-1}}
\ar[llll]_-{\leftcurrifyone{a_1}}
\\
\\
\distributor{\leftambicomplementary{b}\tensorialand a_1\tensorialand a_2}{\tensorialfalse}
\ar[dd]_-{\rightcurrifyone{a_2}}
\ar@{=}[rrrr]
&&
\ar@{}[dd]|-{(b)}
&&
\distributor{\leftambicomplementary{b}\tensorialor a_1\tensorialand a_2}{\tensorialfalse}
\ar[dd]^-{\rightcurrifyone{a_1\tensorialand a_2}}
\\
\\
\distributor{\leftambicomplementary{b}\tensorialand a_1}{\rightambicomplementary{a_2}}
\ar[dddd]_-{\leftcurrifyone{\leftambicomplementary{b}}}
\ar@{=}[rr]
&
\ar@{}[dddd]|-{(a)}
&
\distributor{\leftambicomplementary{b}\tensorialand a_1}{\rightambicomplementary{a_2}}
\ar[rr]^-{\rightcurrifyone{a_1}}
&
\ar@{}[dddd]|-{(c)}
&
\distributor{\leftambicomplementary{b}}{\rightambicomplementary{a_2}\tensorialor\rightambicomplementary{a_1}}
\\
\\
\\
\\
\distributor{a_1}{b\tensorialor\rightambicomplementary{a_2}}
\ar[rr]^-{(\leftcurrifyone{a_2\tensorialand\leftambicomplementary{b}})^{-1}\,\,\,\,\,}
&&
\distributor{a_2\tensorialand \leftambicomplementary{b}\tensorialand a_1}{\tensorialfalse}
\ar[rr]^-{\rightcurrifyone{a_1}}
\ar[uuuu]_-{\leftcurrifyone{a_2}}
&&
\distributor{a_2\tensorialand \leftambicomplementary{b}}{\rightambicomplementary{a_1}}
\ar[uuuu]_-{\leftcurrifyone{a_2}}
}
$$
where each component~$(a)$, $(b)$ and $(c)$ commutes as an instance
of the coherence diagram~(\ref{equation/ambidextrous-coherence-L}),
(\ref{equation/ambidextrous-coherence-R}) and (\ref{equation/ambidextrous-coherence-LR}) respectively.
%
This establishes that $\Ftwofunctor$ transports every ambidextrous chirality
to a helical chirality.
%
Now, we would like to show that every ambidextrous homomorphism
$$F=(\functor{F},\functorco{F},\functorcell{F},\functorcellbracketspecial{F})
\quad : \quad (\Acategory_1,\Bcategory_1) \quad \morph{} \quad (\Acategory_2,\Bcategory_2)$$
between ambidextrous chiralities defines a helical homomorphism
between the corresponding helical chiralities.
%
To that purpose, we need to check that
the coherence diagram~(\ref{equation/additional-requirement-for-helical-1-cells}) commutes.
$$
\vcenter{\xymatrix @-1.2pc {
\distributor{a}{b}
\ar[rrrrrr]^-{F_{a,b}}
\ar[dd]_-{(\leftcurrifyone{\leftambicomplementary{b}})^{-1}}
&&&&&&
\distributor{\functor{F}(a)}{\functorco{F}(b)}
\ar[dddd]^-{(\leftcurrifyone{\leftambicomplementary{\functorco{F}(b)}})^{-1}}
%\ar[dd]^-{\helix_{\functor{F}(a),\functorco{F}(b)}}
\\
\\
\distributor{\leftambicomplementary{b}\tensorialand a}{\tensorialfalse}
\ar[rrrr]^-{F_{\leftambicomplementary{b}\tensorialand a,\tensorialfalse}}
\ar[dddddd]_-{\rightcurrifyone{a}}
&&
\ar@{}[dddddd]|-{(b)}
&&
\distributor{\functor{F}(\leftambicomplementary{b}\tensorialand a)}{\functorco{F}(\tensorialfalse)}
\ar@{}[rr]|-{(a)}
\ar[dd]|-{monoidality}
&&
\\
\\
&&&&
\distributor{\functor{F}(\leftambicomplementary{b})\tensorialand \functor{F}(a)}{\tensorialfalse}
\ar[rr]^-{\functorcell{F}}
\ar[dd]^-{\rightcurrifyone{\functor{F}(a)}}
&&
\distributor{\leftambicomplementary{(\functorco{F}(b))}\tensorialand \functor{F}(a)}{\tensorialfalse}
\ar[dddd]^-{\rightcurrifyone{\functor{F}(a)}}
\\
&&&&&&
\\
&&&&
\distributor{\functor{F}(\leftambicomplementary{b})}{\rightambicomplementary{(\functor{F}(a))}}
\ar[ddrr]^-{\functorcell{F}}
\ar@{}[rru]|-{(c)}
\\
\\
\distributor{\leftambicomplementary{b}}{\rightambicomplementary{a}}
\ar[rrrr]^-{F_{\leftambicomplementary{b},\rightambicomplementary{a}}}
&&&&
\distributor{\functor{F}(\leftambicomplementary{b})}{\functorco{F}(\rightambicomplementary{a})}
\ar[rr]^-{\functorcell{F}}
\ar[uu]_-{\functorcell{F}}
&&
\distributor
{\leftambicomplementary{(\functorco{F}(b))}}
{\rightambicomplementary{(\functor{F}(a))}}
}}
$$
where (a) commutes because of (\ref{equation/refraction-chiralities/monoidal-coherence-diagram})
(b) commutes because of (\ref{equation/refraction-chiralities/monoidal-coherence-diagram-right})
and (c) because of naturality of~$\rightcurrifyalone$.

\paragraph{Helical $\Rightarrow$ Ambidextrous.}
The 2-functor~$\Gtwofunctor$ transports every helical chirality
$(\Acategory,\Bcategory,\currifyalone)$ into the ambidextrous chirality
$(\Acategory,\Bcategory,\leftcurrifyalone,\rightcurrifyalone)$ 
with left currification~$\leftcurrifyalone$ defined 
as the currification~$\currifyalone$ of the original chirality,
and right currification $\rightcurrifyalone$ defined
as the composite morphism
\begin{equation}\label{equation/definition-of-right-currification-from-the-helix}
\vcenter{\xymatrix @-.5pc {
\distributor{a\tensorialand m}{b}
\ar[dd]_-{\currify{a}{m}{b}}
\ar[rrr]^-{\rightcurrify{m}{a}{b}}
&&&
\distributor{a}{b\tensorialor\rightcomplementary{m}}
\ar@{=}[rr]
&&
\distributor{a}{\rightcomplementary{(\leftcomplementary{b})}\tensorialor\rightcomplementary{m}}
\\
\\
\distributor{m}{\rightcomplementary{a}\tensorialor b}
\ar[rrr]^-{\helix}
&&&
\distributor{\leftcomplementary{(\rightcomplementary{a}\tensorialor b)}}{\rightcomplementary{m}}
\ar@{=}[rr]
&&
\distributor{\leftcomplementary{b}\tensorialand a}{\rightcomplementary{m}}
\ar[uu]_-{\currify{\leftcomplementary{b}}{a}{\rightcomplementary{m}}}
}}
\end{equation}
We need to establish that the two coherence diagrams~(\ref{equation/ambidextrous-coherence-R})
and~(\ref{equation/ambidextrous-coherence-LR}) of ambidextrous categories commute.
%
Once instantiated with the definitions just given,
the coherence diagram~(\ref{equation/ambidextrous-coherence-R})
looks as follows:
%
$$
\xymatrix @-1.82pc {
&&
\distributor{m\tensorialand n}{\rightcomplementary{a}\tensorialor b}
\ar[rrrrr]^-{\helix}
\ar[lldddddd]^-{\currifyone{m}}
&&&&&
\distributor{\leftcomplementary{b}\tensorialand a}{\rightcomplementary{n}\tensorialor\rightcomplementary{m}}
\ar[rrdd]^-{\currifyone{\leftcomplementary{b}}}
&&
\\
\\
\distributor{a\tensorialand m\tensorialand n}{b}
\ar[rruu]^-{\currifyone{a}}
\ar[dddd]_-{\currifyone{a\tensorialand m}}
&&
&&&&&
&&
\distributor{a}{b\tensorialor \rightcomplementary{n}\tensorialor\rightcomplementary{m}}
\\
\\
\ar@{}[rrrrrrrrr]|-{(\ast)}
&&&&&&
&&&&&&
\\
\\
\distributor{n}{\rightcomplementary{m}\tensorialor \rightcomplementary{a}\tensorialor b}
\ar[rrdd]_-{\helix}
&&&&
&&&
&&
\distributor{n\tensorialand\leftcomplementary{b}\tensorialand a}{\rightcomplementary{m}}
\ar[uuuu]_-{\currifyone{n\tensorialand\leftcomplementary{b}}}
\ar[lluuuuuu]^-{\currifyone{n}}
\\
\\
&&
\distributor{\leftcomplementary{b}\tensorialand a \tensorialand m}{\rightcomplementary{n}}
\ar[rrrrr]^-{\currifyone{a\tensorialand\leftcomplementary{b}}}
&&&&&
\distributor{m}{\rightcomplementary{a}\tensorialor b\tensorialor \rightcomplementary{n}}
\ar[rruu]_-{\helix}}
$$
The point is that the inner diagram~($\ast$) commutes 
because it coincides with~(\ref{equation/coherence-diagram-helix}).
%
The two triangles commute by definition of dialogue chiralities
and more specifically the coherence diagram~(\ref{equation/coherence/currify-one-dialogue}).
%
Once instantiated with the definition of~$\rightcurrifyalone$ above, 
the coherence diagram~(\ref{equation/ambidextrous-coherence-LR})
is easily shown to commute:
$$
\xymatrix @-1.8pc {
&&
\distributor{n}{\rightcomplementary{a}\tensorialor\rightcomplementary{m}\tensorialor b}
\ar[rrrrr]^-{\helix}
\ar@{=}[dddddddd]
&&&&&
\distributor{\leftcomplementary{b}\tensorialand m\tensorialand a}{\rightcomplementary{n}}
\ar[rrdd]^-{\currifyone{\leftcomplementary{b}}}
\ar@{=}[dddddddd]
&&
\\
\\
\distributor{m\tensorialand a\tensorialand n}{b}
\ar[rruu]^-{\currifyone{m\tensorialand a}}
\ar[dddd]_-{\currifyone{m}}
&&
&&&&&
&&
\distributor{m\tensorialand a}{b\tensorialor\rightcomplementary{n}}
\ar[dddd]^-{\currifyone{m}}
\\
\\
&&&&&
&&&&&&
\\
\\
\distributor{a\tensorialand n}{\rightcomplementary{m}\tensorialor b}
\ar[rrdd]_-{\currifyone{a}}
&&&&&
&&
&&
\distributor{a}{\rightcomplementary{m}\tensorialor b\tensorialor \rightcomplementary{n}}
\\
\\
&&
\distributor{n}{\rightcomplementary{a}\tensorialor\rightcomplementary{m}\tensorialor b}
\ar[rrrrr]^-{\helix}
&&&&&
\distributor{\leftcomplementary{b}\tensorialand m\tensorialand a}{\rightcomplementary{n}}
\ar[rruu]_-{\currifyone{{\leftcomplementary{b}}\tensorialand m}}}
$$
in every helical dialogue chirality.
%
This establishes that the 2-functor~$\Gtwofunctor$ transports every helical chirality
to an ambidextrous chirality.
%
Now, we want to prove that every helical homomorphism
$$
F=(\functor{F},\functorco{F},\functorcell{F},\functorcellbracketspecial{F})
\quad : \quad (\Acategory_1,\Bcategory_1) \quad \morph{} \quad (\Acategory_2,\Bcategory_2)
$$
defines an ambidextrous homomorphism between the underlying
ambidextrous chiralities~$\Gtwofunctor(\Acategory_1,\Bcategory_1)$
and~$\Gtwofunctor(\Acategory_2,\Bcategory_2)$.
%
To that purpose, we need to check that the
coherence diagram~(\ref{equation/refraction-chiralities/monoidal-coherence-diagram-right})
commutes for~$F$ with~$\rightcurrifyalone$ defined 
as in~(\ref{equation/definition-of-right-currification-from-the-helix}).
\begin{footnotesize}
$$
\xymatrix @-1.9pc {
&&
\distributor{m}{\rightcomplementary{a}\tensorialor b}
\ar[rrrrr]^-{\helix}
\ar[dddd]^-{F_{m,\rightcomplementary{a}\tensorialor b}}
&&&&&
\distributor{\leftcomplementary{b}\tensorialand a}{\rightcomplementary{m}}
\ar[rrdddd]^-{\,\,\,\currifyone{\leftcomplementary{b}}}
\ar[dddd]_-{F_{\leftcomplementary{b}\tensorialand a,\rightcomplementary{m}}}
&&
\\
\\
\\
\\
\distributor{a\tensorialand m}{b}
\ar[rruuuu]^-{\currifyone{a}\,\,\,}
\ar[dddd]_-{F_{a\tensorialand m,b}}
&&
\distributor{\functor{F}m}{\functorco{F}(\rightcomplementary{a}\tensorialor b)}
\ar[dddddddd]|-{monoidality}
&&&&&
\distributor{\functor{F}(\leftcomplementary{b}\tensorialand a)}{\functorco{F}\rightcomplementary{m}}
\ar[dddddddd]|-{monoidality}
&&
\distributor{a}{b\tensorialor \rightcomplementary{m}}
\ar[dddd]^-{F_{a,b\tensorialor\rightcomplementary{m}}}
\\
\\
&&&&&
&&&&&&
\\
\\
\distributor{\functor{F}(a\tensorialand m)}{\functorco{F}b}
\ar[dddd]|-{monoidality}
&&
&&&
&&
&&
\distributor{\functor{F}a}{\functorco{F}(b\tensorialor \rightcomplementary{m})}
\ar[dddd]|-{monoidality}
\\
\\
\\
\\
\distributor{\functor{F}a\tensorialand \functor{F}m}{\functorco{F}b}
\ar[rrdddd]_-{\currifyone{\functor{F}(a)}\,\,\,\,}
&&
\distributor{\functor{F}m}{\functorco{F}(\rightcomplementary{a})\tensorialor\functorco{F}b}
\ar[dddd]^-{\functorcell{F}}
&&&
&&
\distributor{\functor{F}(\leftcomplementary{b})\tensorialand\functor{F}a}{\functorco{F}\rightcomplementary{m}}
\ar[dddd]_-{\functorcell{F}}
&&
\distributor{\functor{F}a}{\functorco{F}b\tensorialor \functorco{F}\rightcomplementary{m}}
\\
\\
\\
\\
&&
\distributor{\functor{F}m}{\rightcomplementary{(\functor{F}a)}\tensorialor \functorco{F}b}
\ar[rrrrr]^-{\helix}
&&&&&
\distributor{\leftcomplementary{(\functorco{F}b)}\tensorialand \functor{F}a}{\rightcomplementary{(\functor{F}m)}}
\ar[rruuuu]_-{\,\,\,\,\currifyone{\leftcomplementary{\functorco{F}(b)}}}}
$$
\end{footnotesize}

\paragraph{Isomorphism.}
An easy computation convinces that $\Ftwofunctor$ and $\Gtwofunctor$
are reverse transformations and thus establish a one-to-one relationship
between the ambidextrous chiralities and the helical chiralities.
%
Moreover, the 2-functors do not alter the dialogue chirality
underlying a given ambidextrous or helical dialogue chirality.
%
From this follows that the isomorphism lives above the 2-category~$\DialogueChiralities$
in the sense that the diagram below commutes.
%
$$
\xymatrix @-1.7pc {
\AmbiChir
\ar[dddd]_-{U}
&\ar@/^1.2pc/[rrrrrrrr]^-{\Ftwofunctor}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
2-dim
\\
isomorphism
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^-{\Gtwofunctor}
&
\HeliChir
\ar[dddd]^-{U'}
\\
\\
\\
\\
\DialogueChiralities
&
\ar@{=}[rrrrrrrr]
&&&&
&&&&
&
\DialogueChiralities
}
$$


\section{Ambidextrous chiralities by transjunctions}
%
We proceed in the same way as we did for dialogue chiralities
in our companion paper~\cite{mellies:tensorial-logic-4}
and reformulate the notion of ambidextrous chirality
in the language of transjunctions.
%
A first presentation is given in~\S\ref{section/ambidextrous-chiralities-axioms}
with emphasis given to the properties of the axiom combinators, then a second one
with emphasis given to cut combinators in~\S\ref{section/ambidextrous-chiralities-cuts}.
%
One purpose of this presentation based on transjunctions is
to provide an algebraic counterpart to the notions of axiom
and cut links in proof-net of linear or tensorial logic.
%
The connection becomes visually explicit in the graphical account
of the coherence diagrams in string diagrams, 
see~\S\ref{section/ambidextrous-chiralities-in-string-diagrams} for details.

\subsection{Formulation based on the axiom combinator}\label{section/ambidextrous-chiralities-axioms}
%
It is not difficult to reformulate the notion of ambidextrous chirality
using the language of transjunctions.
%
An ambidextrous chirality is a pair of monoidal categories
$(\Acategory,\tensorialand,\tensorialtrue)$ and
$(\Bcategory,\tensorialor,\tensorialfalse)$
equipped with an adjunction~$L\dashv R$ and with a monoidal equivalence
$$
\xymatrix @-1.9pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{L}
&&&&\bot&&&&
\ar@/^1.2pc/[llllllll]^{R}
&
\Bcategory
}
\quad\quad\quad\quad\quad\quad
\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)}}
$$
together with two families of transjunctions
$$
\begin{array}{c}
\xymatrix @-1.6pc {
\leftaxiom{m} & : & \leftadjoint(a) & \ar[rrrr] &&&&
& \rightcomplementary{m}\tensorialor\leftadjoint(m\tensorialand a)}
\\
\xymatrix @-1.6pc {
\leftcut{m} & : 
&
m\tensorialand \rightadjoint (\rightcomplementary{m}\tensorialor b)
&
\ar[rrrr] &&&&
& \rightadjoint (b)
}
\end{array}$$
%
$$
\begin{array}{c}
\xymatrix @-1.6pc {
\rightaxiom{m} & : & \leftadjoint(a) & \ar[rrrr] &&&&
& (a\tensorialand m)\tensorialor \rightcomplementary{m}}
\\
\xymatrix @-1.6pc {
\rightcut{m} & : 
&
(b\tensorialor \rightcomplementary{m}) \tensorialand m
&
\ar[rrrr] &&&&
& \rightadjoint (b)
}
\end{array}$$
One requires moreover the two coherence diagrams for the left axiom combinator
$$
\xymatrix @-1.4pc {
&&&
\rightcomplementary{m}
\tensorialor
\leftadjoint{(m\tensorialand a)}
\ar@/^1.3pc/[rrdd]^-{f}
\\
\\
\leftadjoint{(a)}
\ar@/^1.3pc/[rrruu]^-{\leftaxiom{m}\,\,\,\,\,\,}
\ar@/_1.3pc/[rrrdd]_-{\leftaxiom{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/coherence-for-ambidextrous-chiralities-left-axiom}
\vcenter{\xymatrix @-1.2pc {
\rightcomplementary{n}
\tensorialor
\leftadjoint{(n\tensorialand a)}
\ar[rrrrrr]^-{\leftaxiom{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]^-{\leftaxiom{n}}
\ar[rrrrrr]^-{\leftaxiom{m\tensorialand n}}
&&&&&&
\rightcomplementary{(m\tensorialand n)}
\tensorialor \leftadjoint{((m\tensorialand n)\tensorialand a)}}}
\end{equation}
for every morphism~$f:m\morph{}n$ of the category~$\Acategory$,
followed by the two coherence diagrams for the right axiom combinator
%Two times the usual equations, for the left and the right side.
$$
\xymatrix @-1.4pc {
&&&
\leftadjoint{(a\tensorialand m)}
\tensorialor\rightcomplementary{m}
\ar@/^1.3pc/[rrdd]^-{f}
\\
\\
\leftadjoint{(a)}
\ar@/^1.3pc/[rrruu]^-{\rightaxiom{m}\,\,\,\,\,\,}
\ar@/_1.3pc/[rrrdd]_-{\rightaxiom{n}\,\,\,\,\,\,}
&&&&&
\leftadjoint{(a\tensorialand n)}
\tensorialor\rightcomplementary{m}
\\
\\
&&&
\leftadjoint{(a\tensorialand n)}
\tensorialor\rightcomplementary{n}
\ar@/_1.3pc/[rruu]_-{\rightcomplementary{f}}
}
$$
\begin{equation}\label{equation/coherence-for-ambidextrous-chiralities-right-axiom}
\vcenter{\xymatrix @-1.2pc {
\leftadjoint{(a\tensorialand m)}\tensorialor\rightcomplementary{m}
\ar[rrrrrr]^-{\rightaxiom{n}}
&&&&&&
(\leftadjoint{((a\tensorialand m)\tensorialand n)}\tensorialor\rightcomplementary{n})\tensorialor\rightcomplementary{m}
\ar[dd]^-{associativity}
\\
\\
&&&&&&
\leftadjoint{(a\tensorialand (m\tensorialand n))}\tensorialor(\rightcomplementary{n}\tensorialor\rightcomplementary{m})
\ar[dd]^-{monoidality}
\\
\\
\leftadjoint{a}
\ar[uuuu]^-{\rightaxiom{m}}
\ar[rrrrrr]^-{\rightaxiom{m\tensorialand n}}
&&&&&&
\leftadjoint{(a\tensorialand (m\tensorialand n))}\tensorialor\rightcomplementary{(m\tensorialand n)}
}}
\end{equation}
%
Finally, the important additional coherence diagram tells that
the left and the right axiom combinators may be commuted
in the following sense:
\begin{equation}\label{equation/transjunction-ambidextrous}
\vcenter{\xymatrix{
& 
\leftadjoint{(a\tensorialand n)}\tensorialor\rightcomplementary{n}
\ar[rrr]^-{\leftaxiom{m}}
&&&
\rightcomplementary{m}\tensorialor (\leftadjoint{(m\tensorialand (a\tensorialand n))}\tensorialor\rightcomplementary{n})
\ar@{=}[dd]^-{associativity}
\\
\leftadjoint{a}
\ar@/^1pc/[ru]^-{\rightaxiom{n}\,\,\,\,}
\ar@/_1pc/[rd]_-{\leftaxiom{m}\,\,\,\,}
\\
& 
\rightcomplementary{m}\tensorialor
\leftadjoint{(m\tensorialand a)}
\ar[rrr]^-{\rightaxiom{n}}
&&&
(\rightcomplementary{m}\tensorialor \leftadjoint{((m\tensorialand a)\tensorialand n)})\tensorialor\rightcomplementary{n}
}}
\end{equation}

\subsection{Alternative formulation based on cuts}
\label{section/ambidextrous-chiralities-cuts}
Here, for the sake of completeness, we review the alternative formulation
of ambidextrous chiralities based this time on the cut combinator.
%
Just as in the case of the formulation based on the axiom combinator,
it combines a series of two coherence diagrams for left cut:
$$
\vcenter{\xymatrix @-1.6pc {
&
m\tensorialand\rightadjoint{(\rightcomplementary{m}\tensorialor b)}
\ar@/^1.3pc/[rrrdd]^-{\hspace{.3em}\leftcut{m}}
\\
\\
m\tensorialand\rightadjoint{(\rightcomplementary{n}\tensorialor b)}
\ar@/^1.3pc/[ruu]^-{\rightcomplementary{f}}
\ar@/_1.3pc/[rdd]_-{f}
&&&&
\rightadjoint{(b)}
\\
\\
&
n\tensorialand\rightadjoint{(\rightcomplementary{n}\tensorialor b)}
\ar@/_1.3pc/[rrruu]_-{\hspace{.3em}\leftcut{n}}
}}
$$
$$
\vcenter{\xymatrix @-1pc {
m\tensorialand (n\tensorialand \rightadjoint{(\rightcomplementary{n}\tensorialor(\rightcomplementary{m}\tensorialor b))})
\ar[rrrrrr]^-{\leftcut{n}}
&&&&&&
m\tensorialand\rightadjoint{(\rightcomplementary{m}\tensorialor b)}
\ar[dddd]^-{\leftcut{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]^-{\leftcut{m\tensorialand n}}
&&&&&&
\rightadjoint{(b)}
}}
$$
with a series of two coherence diagrams for the right cut:
$$
\vcenter{\xymatrix @-1.6pc {
&
\rightadjoint{(b\tensorialor\rightcomplementary{m})}\tensorialand m
\ar@/^1.3pc/[rrrdd]^-{\hspace{.3em}\rightcut{m}}
\\
\\
\rightadjoint{(b\tensorialor\rightcomplementary{n})}\tensorialand m
\ar@/^1.3pc/[ruu]^-{\rightcomplementary{f}}
\ar@/_1.3pc/[rdd]_-{f}
&&&&
\rightadjoint{(b)}
\\
\\
&
\rightadjoint{(b\tensorialor\rightcomplementary{n})}\tensorialand n
\ar@/_1.3pc/[rrruu]_-{\hspace{.3em}\rightcut{n}}
}}
$$
$$
\vcenter{\xymatrix @-1pc {
(\rightadjoint{((b\tensorialor\rightcomplementary{n})\tensorialor\rightcomplementary{m})} \tensorialand m)\tensorialand n
\ar[rrrrrr]^-{\rightcut{m}}
&&&&&&
\rightadjoint{(b\tensorialor\rightcomplementary{n})} \tensorialand n
\ar[dddd]^-{\rightcut{n}}
\\
\\
\rightadjoint{(b\tensorialor(\rightcomplementary{n}\tensorialor\rightcomplementary{m}))} \tensorialand (m\tensorialand n)
\ar[uu]^-{associativity}
&&&&&&
\\
\\
\rightadjoint{(b\tensorialor\rightcomplementary{(m\tensorialand n)})}\tensorialand (m\tensorialand n)
\ar[uu]^-{monoidality}
\ar[rrrrrr]^-{\rightcut{m\tensorialand n}}
&&&&&&
\rightadjoint{(b)}
}}
$$
as well as an additional coherence diagram which ensures
that the left and the right cut commute in the following sense:
%
\begin{equation}\label{equation/permutation-of-the-cut}
\vcenter{\xymatrix @-1.5pc {
(m\tensorialand \rightadjoint{(\rightcomplementary{m}\tensorialor (a\tensorialor \rightcomplementary{n}))} )\tensorialand n
\ar[rrrrrr]^-{\leftcut{m}}
\ar@{-}[dddd]_-{associativity}
&&&&&&
\rightcomplementary{n}\tensorialor\rightadjoint{(n\tensorialand a)}
\ar[dd]^-{\rightcut{n}}
\\
\\
&&&&&&
\rightadjoint{(b)}
\\
\\
m\tensorialand( \rightadjoint{((\rightcomplementary{m}\tensorialor a)\tensorialor \rightcomplementary{n})} \tensorialand n)
\ar[rrrrrr]^-{\rightcut{n}}
&&&&&&
\rightcomplementary{m}\tensorialor\rightadjoint{(m\tensorialand a)}
\ar[uu]_-{\leftcut{m}}
}}
\end{equation}
These diagrams should commute for all objects~$a,m,n$ of the category~$\Acategory$,
all objects~$b$ of the category~$\Bcategory$ and all morphisms~$f:m\morph{}n$ of the category~$\Acategory$.
%

%
%\begin{equation}\label{equation/permutation-of-the-axiom}
%\vcenter{\xymatrix @-1.2pc {
%\rightcomplementary{m}\tensorialor\leftadjoint{(m\tensorialand a)}
%\ar[rrrrrr]^-{\rightaxiom{n}}
%&&&&&&
%(\rightcomplementary{m}\tensorialor \leftadjoint{((m\tensorialand a)\tensorialand n)}) \tensorialor \rightcomplementary{n}
%\ar@{-}[dddd]^-{associativity}
%\\
%\\
%\leftadjoint{a}
%\ar[uu]^-{\leftaxiom{m}}
%\ar[dd]_-{\rightaxiom{n}}
%\\
%\\
%\leftadjoint{(a\tensorialand n)} \tensorialor \rightcomplementary{n}
%\ar[rrrrrr]^-{\leftaxiom{m}}
%&&&&&&
%\rightcomplementary{m}\tensorialor( \leftadjoint{(m\tensorialand(a\tensorialand n))} \tensorialor \rightcomplementary{n})
%}}
%\end{equation}
%

%
%\paragraph{Remark.}
%This implies that this is true for units.
%$$
%\xymatrix{
%\leftadjoint{(a\tensorialand\tensorialtrue)}\tensorialor\rightcomplementary{\tensorialtrue}
%\ar[rrrr]^-{monoidality}
%&&&&
%\leftadjoint{(a\tensorialand\tensorialtrue)}\tensorialor\tensorialfalse
%\ar[dd]|-{associativity}
%\\
%\\
%\leftadjoint{a}
%\ar[rrrr]^{id}
%\ar[uu]^{\rightaxiom{\tensorialtrue}}
%&&&&
%\leftadjoint{a}
%}
%$$
%$$
%\xymatrix{
%\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]^{\leftaxiom{\tensorialtrue}}
%&&&&
%\leftadjoint{a}
%}
%$$

%\section{Eta law for negation}
%
%\subsection{Flexible negation}
%The following equation holds when the negation is twist-free
%+
%$$
%\xymatrix @-1pc {
%\rightcomplementary{(\rightadjoint{(\tensorialfalse)})} \tensorialor \leftadjoint{(\rightadjoint{(\tensorialfalse)}\tensorialand \tensorialtrue)}
%\ar[rr]
%&&
%\leftadjoint{(\tensorialtrue)}
%\tensorialor \leftadjoint{(\rightadjoint{(\tensorialfalse)})}
%\ar[dd]^-{\varepsilon}
%\\
%\\
%\leftadjoint{(\tensorialtrue)}
%\ar[uu]^-{axiom-left}
%\ar[dd]_-{axiom-right}
%\ar[rr]^-{id}
%&&
%\leftadjoint{(\tensorialtrue)}
%\\
%\\
%\leftadjoint{(\tensorialtrue\tensorialand\rightadjoint{(\tensorialfalse)})}
%\tensorialor
%\rightcomplementary{(\rightadjoint{(\tensorialfalse)})}
%\ar[rr]
%&&
%\leftadjoint{(\rightadjoint{(\tensorialfalse)})}
%\tensorialor
%\leftadjoint{(\tensorialtrue)}
%\ar[uu]_-{\varepsilon}
%}
%$$
\subsection{A pictorial account based on string diagrams}\label{section/ambidextrous-chiralities-in-string-diagrams}
%
The coherence diagram~(\ref{equation/coherence-for-ambidextrous-chiralities-left-axiom})
for the left axiom combinator has been already depicted as~(\ref{equation/tensorial-axiom-cut-left-hand-side})
in the introduction, while its righthand side variant~(\ref{equation/coherence-for-ambidextrous-chiralities-right-axiom})
is depicted in exactly the same way:
%
\begin{equation}
\begin{tabular}{ccc}
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-right-1.pdf}
&
\hspace{1em} \raisebox{22mm}{\Large{$\stackrel{}{=}$}} \hspace{1em}
&
\includegraphics[height=50mm]{dessins/axiom-cut/axiom-tensor-cotensor-right-2.pdf}
\end{tabular}
\end{equation}
%
The coherence diagram~(\ref{equation/transjunction-ambidextrous})
is drastically different from~(\ref{equation/coherence-for-ambidextrous-chiralities-left-axiom})
and~(\ref{equation/coherence-for-ambidextrous-chiralities-right-axiom})
and is depicted as
\begin{center}
\begin{tabular}{ccc}
\includegraphics[height=45mm]{dessins/axiom-cut/helical-axiom-1.pdf}
&
\hspace{1em} \raisebox{22mm}{\Large{$\stackrel{}{=}$}} \hspace{1em}
&
\includegraphics[height=45mm]{dessins/axiom-cut/helical-axiom-2.pdf}
\end{tabular}
\end{center}
where the apparent braiding is here to reflect the associativity rule which typically
permutes the actions of $(m\tensor-)$ with the action of $(-\tensor n)$.


\section{Linearly distributive chiralities}
In this section, we adapt to an ambidextrous situation
the notion of \emph{linearly distributive chirality}
introduced in~\cite{mellies:tensorial-logic-4}.
%
The adaptation is done in the most straightforward way 
in~\S\ref{section/linearly-distributive-chirality-definition}
since it essentially consists in putting side by side
a left and a right linearly distributive chirality
in the sense of~\cite{mellies:tensorial-logic-4}.
%
%Note however that the two chiralities share the same
%adjunction~$L\dashv R$.
%
The notion of duality introduced in~\cite{mellies:tensorial-logic-4}
is adapted accordingly.
%
Once again, the resulting definition of duality is obtained 
by putting together a right and a left duality --- except
for the apparition of the coherence diagram~(\ref{equation/axiom-helical-left-right-duality})
whose task is precisely to combine the left and the right axiom combinators.

\subsection{Definition}\label{section/linearly-distributive-chirality-definition}
A 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 the four bimonads
\begin{equation}\label{equation/bimonads}
\begin{array}{ccccc}
\leftcontau
& \quad : \quad &
m\tensorialand R(L(a)\tensorialor b)
& \quad \morph{} \quad &
R(L(m\tensorialand a)\tensorialor b)
\\
\leftdistau & \quad : \quad &
L(R(n\tensorialor b)\tensorialand a)
& \quad \morph{} \quad &
n\tensorialor L(R(b)\tensorialand a)
\\
\rightcontau & \quad : \quad &
R(b\tensorialor L(a))\tensorialand m
& \quad \morph{} \quad &
R(b\tensorialor L(a\tensorialand m))
\\
\rightdistau & \quad : \quad &
L(a\tensorialand R(b\tensorialor n))
& \quad \morph{} \quad &
L(a\tensorialand R(b)) \tensorialor n
\end{array}
\end{equation}
between the $\tensorialand$-tensor product and the $\Bcategory$-monad of~$\Acategory$
on the one hand, and between the $\tensorialor$-tensor product and the $\Acategory$-comonad
of~$\Bcategory$ on the other hand.
%
Besides the resulting series of commutative diagrams,
we ask that the two diagrams below commute
\begin{center}
\includegraphics[width=22em]{dessins/algebraic-presentation-of-dialogue/apdc-mysterious-axiome-left-discursive-pair.pdf}
\end{center}
\begin{center}
\includegraphics[width=22em]{dessins/algebraic-presentation-of-dialogue/apdc-mysterious-axiome-right-discursive-pair.pdf}
\end{center}
for all objects~$a,m,n$ of the category~$\Acategory$ and all object~$b$ of the category~$\Bcategory$.
%
Plus a series of other diagrams required in the proof of the following lemma.
%
\begin{center}
\includegraphics[width=22em]{dessins/algebraic-presentation-of-dialogue/apdc-second-mysterious-axiome-left-right-discursive-pair.pdf}
\end{center}
%
Note that these coherence diagrams are not justified by any of the previous discussions.


\subsection{Dualities}
We adapt the notion of duality introduced in~\cite{mellies:tensorial-logic-4}
to an ambidextrous situation.
\begin{definition}[duality]
A duality in a linearly distributive chirality~$(\Acategory,\Bcategory)$
is defined as a monoidal equivalence
$$
\xymatrix @-1.8pc {
\Acategory
&\ar@/^1.2pc/[rrrrrrrr]^{\leftcomplementary{(-)}}
\ar@{}[rrrrrrrr]|-{\begin{tiny}
\begin{array}{c}
monoidal
\\
equivalence
\end{array}
\end{tiny}}
&&&&
&&&&
\ar@/^1.2pc/[llllllll]^{\rightcomplementary{(-)}}
&
\Bcategory^{\, op(0,1)}}
$$
together with four families of morphisms
$$
\RIGHTAX{m} \quad : \quad \tensorialtrue \quad \morph{} \quad R(L(m)\tensorialor \leftcomplementary{m})
$$
$$
\RIGHTCUT{m} \quad : \quad L(R(\leftcomplementary{m})\tensorialand m)
\quad \morph{} \quad \tensorialfalse
$$
$$
\LEFTAX{m} \quad : \quad \tensorialtrue \quad \morph{} \quad R(\leftcomplementary{m}\tensorialor L(m))
$$
$$
\LEFTCUT{m} \quad : \quad L(m\tensorialand R(\leftcomplementary{m}))
\quad \morph{} \quad \tensorialfalse
$$
each of them parametrized by the objects~$m$ of the category~$\Acategory$.
%
\end{definition}
These morphisms are moreover required to make the three coherence diagrams below commute.
%
\paragraph{The right coherence diagrams.}
The first coherence diagram adapts the usual triangular axiom of adjunctions:
\begin{center}
\includegraphics[width=29em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-1-right-duality.eps}
\end{center}
The second coherence diagram means that the family of combinators $\AX{-}$ is dinatural:
\begin{center}
\includegraphics[width=21em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-2-right-duality.eps}
\end{center}
The third coherence diagram expresses a monoidality of the family $\AX{-}$:
\begin{center}
\includegraphics[width=33em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-3-right-duality.eps}
\end{center}
\begin{center}
\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-4-right-duality.eps}
\end{center}
The four coherence diagrams hold for all objects~$m,n$ and all morphisms~$f:m\to n$ of the category~$\Acategory$.

\paragraph{The left coherence diagrams.}
We need to give the same coherence diagrams on the left side.
\begin{center}
\includegraphics[width=29em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-1-left-duality.eps}
\end{center}
\begin{center}
\includegraphics[width=21em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-2-left-duality.eps}
\end{center}
\begin{center}
\includegraphics[width=33em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-3-left-duality.eps}
\end{center}
\begin{center}
\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-4-left-duality.eps}

\end{center}
\paragraph{The mixed coherence diagrams.}
We also ask this one, which ensures that the two left and right axioms commute:
%\begin{center}
\begin{equation}\label{equation/axiom-helical-left-right-duality}
\raisebox{-8.5em}{\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/apdc-axiome-5-left-right-duality.eps}}
\end{equation}
%\end{center}

\paragraph{Important remark.} Each of these coherence diagrams should be dualized
and repeated for the combinator $CUT$.
%
This is in sharp contrast with the notion of ambidextrous chirality introduced in \S\ref{section/ambi}.
%
Indeed, there is apparently no way to recover the coherence diagram for the cut combinator
from the corresponding diagrams for the combinator $AX$.

\section{Main theorem}
\subsection{Preliminary result on helicality}
One main benefit of introducing the coherence diagram~(\ref{equation/axiom-helical-left-right-duality})
is that we can establish the following property, which states that the dialogue category is helical.
\begin{proposition}
Suppose given a linearly distributive chirality equipped with a duality.
%
In that case, the following diagram
\begin{center}
\includegraphics[width=130mm]{dessins/algebraic-presentation-of-dialogue/commutation-of-the-left-and-right-axioms-proof-step-4.eps}
\end{center}
commutes.
\end{proposition}
The proof that the left and the right axioms commute is based on the commutative diagram below:
\begin{center}
\includegraphics[width=130mm]{dessins/algebraic-presentation-of-dialogue/commutation-of-the-left-and-right-axioms-proof-step-1.eps}
\end{center}
Note that we only need a special case of Diagram~(\ref{equation/axiom-helical-duality-1})
with $\eta$ in front of $\AX{n}$.
%
This commutative diagram enables to establish in turn that the diagram below commutes:
\begin{center}
\includegraphics[width=145mm]{dessins/algebraic-presentation-of-dialogue/commutation-of-the-left-and-right-axioms-proof-step-2.eps}
\end{center}
In order to conclude, there simply remains to establish that the two morphisms~$\eta$
appearing in the previous diagram are monos.
%
This immediately follows from the fact that
%
\begin{center}
\includegraphics[width=130mm]{dessins/algebraic-presentation-of-dialogue/commutation-of-the-left-and-right-axioms-proof-step-3.eps}
\end{center}
is equal to the identity., this esta that each $\eta$ morphism involved in the previous diagram are monos.
%
We conclude that the expected diagram
\begin{center}
\includegraphics[width=130mm]{dessins/algebraic-presentation-of-dialogue/commutation-of-the-left-and-right-axioms-proof-step-4.eps}
\end{center}
commutes.

\begin{corollary}
Suppose given a linearly distributive chirality with a duality.
%
In that case, the induced dialogue chirality is ambidextrous.
\end{corollary}

%There remains to show that...


\subsection{From ambidextrous to linearly distributive and back}

Given an ambidextrous chirality, one constructs a linearly distributive chirality
equipped with a duality.

\begin{proposition}
The ambidextrous chirality deduced from the linearly distributive chirality
and its duality coincide with the original ambidextrous chirality.
\end{proposition}
%
The property is easy to establish. This essentially reduces to establishing that the morphism
$$
\rightaxiom{m} \quad : \quad \leftadjoint(a) \quad \morph{} \leftadjoint(a\tensorialand m)\tensorialor \leftcomplementary{m}
$$
in the original helical chirality~$(\Acategory,\Bcategory)$ coincides with the morphism 
$$
\xymatrix{
\leftadjoint(a) \ar[rr]^-{\RIGHTAX{m}} && \ar[rr]^-{\leftcontau} && \ar[rr]^-{\varepsilon} && 
 \leftadjoint(a\tensorialand m)\tensorialor\leftcomplementary{m}}
$$
recovered from the associated discursive pair.
%
This is established by the simple diagram chase below
\begin{equation}\label{equation/chirality-to-discursive-diagram-chase}
\raisebox{-7em}{\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/chiralite-to-discursive-to-chirality.eps}}
\end{equation}
%
One then needs to check that the morphisms $\leftaxiom{m}$, $\rightcut{m}$ and $\leftcut{m}$ 
coincide with their reconstruction in the discursive pair.
%
Each of the three facts is established by one of the three possible
symmetric variants of the diagram~(\ref{equation/chirality-to-discursive-diagram-chase}).

\subsection{From linearly distributive to ambidextrous and back}
Suppose given a linearly distributive chirality equipped with a duality.
%
We have seen how to construct an ambidextrous chirality from it.
%
The question we would like to address here is whether
the associated linearly distributive chirality coincides with the original one.
%
The first step is to check that the morphism
$$
\RIGHTAX{m} \quad : \quad \tensorialtrue \quad \morph{} \quad \rightadjoint(\leftadjoint(m)\tensorialor\leftcomplementary{m})
$$
of the original duality coincides with the morphism
$$
\includegraphics[width=30em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-morphism.eps}
$$
%$$
%\xymatrix{
%\tensorialtrue
%\ar[rr]^-{\eta}
%&&
%\ar[rr]^-{\RIGHTAX{m}}
%&&
%\ar[rr]^-{\leftcontau{}}
%&&
%\ar[rr]^-{\varepsilon}
%&&
%\rightadjoint(\leftadjoint(m)\tensorialor\leftcomplementary{m})}
%$$
which corresponds to the morphism reconstructed from the chirality.
%
This is essentially immediate.
%
One needs to do the same for the three other components
$\LEFTAX{m}$, $\RIGHTCUT{m}$ and $\LEFTCUT{m}$
of the original duality. 
%
This is done in just the same way, by applying the appropriate
symmetry to the case just treated.

Now, the main difficulty lies in the second part of the proof,
which consists in establishing that the distributivity law
$$
\rightcontau \quad : \quad \rightadjoint(b\tensorialor\leftadjoint (a))\tensorialand m
\quad \morph{} \quad 
\rightadjoint(b\tensorialor\leftadjoint (a\tensorialand m))
$$
of the original discursive pair coincides with the morphism
reconstructed from the associated chirality.
%
This amounts to establishing that the diagram below
$$
\includegraphics[width=29em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-second-morphism.eps}
$$
commutes.
%
This is true, but not so easy to establish, although it boils down 
to producing the appropriate diagram chase.
%
We start by establishing that 
$$
\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-third-diagram.pdf}
$$
commutes as follows:
$$
\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-proof-of-third-diagram.eps}
$$
We then observe that the diagram below
$$
\includegraphics[width=31em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-proof-of-fourth-diagram.eps}
$$
commutes.
%, as an instance of ...
%
Then, we get the final diagram chase:
\newpage
\begin{figure}[!th]
\begin{center}
\includegraphics[width=20em]{dessins/algebraic-presentation-of-dialogue/discursive-to-chirality-to-discursive-second-diagram.pdf}
\caption{Commutative diagram}
\end{center}
\end{figure}


\subsection{Main theorem}
\begin{proposition}
There is a one-to-one relationship between the following notions:
\begin{itemize}
\item an ambidextrous dialogue chirality,
\item a linearly distributive chirality with a duality.
\end{itemize}
\end{proposition}


\begin{thebibliography}{}
%\begin{scriptsize}
\begin{small}

\bibitem{blute-et-al}
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{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-2}
Paul-Andr\'e Melli\`es.
Dialogue categories and chiralities.
Submitted. Manuscript available on the author's webpage.

\bibitem{mellies:tensorial-logic-4}
Paul-Andr\'e Melli\`es.
A micrological study of negation.
Submitted. Manuscript available on the author's webpage.

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

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

\newpage

\tableofcontents

\end{document}
