[Bonchi et al(2022)]
authorpersonFilippo Bonchi, personFabio
Gadducci, personAleks Kissinger, personPawel
Sobocinski, and personFabio Zanasi.
String Diagram Rewrite Theory I: Rewriting with
Frobenius Structure.
journalJ. ACM volume69,
number2 (year2022), pages14:1–14:58.

[Bonchi et al(2019a)]
authorpersonFilippo Bonchi, personJoshua
Holland, personRobin Piedeleu, personPaweł
Sobociński, and personFabio Zanasi.
Diagrammatic Algebra: From Linear to Concurrent
journalProceedings of the ACM on Programming
Languages volume3, numberPOPL (dateJan.
year2019), pages25:1–25:28.

[Bonchi et al(2019b)]
authorpersonFilippo Bonchi, personRobin
Piedeleu, personPawel Sobociński, and
personFabio Zanasi. year2019b.
Graphical Affine Algebra. In
booktitle2019 34th Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS). pages1–12.

[Bonchi et al(2018)]
authorpersonFilippo Bonchi, personJens
Seeber, and personPawel Sobocinski.
Graphical Conjunctive Queries. In
booktitle27th EACSL Annual Conference on Computer Science
Logic (CSL 2018) (seriesLeibniz International Proceedings
in Informatics (LIPIcs), Vol. volume119),
editorpersonDan Ghica and personAchim
Jung (Eds.). publisherSchloss Dagstuhl–Leibniz-Zentrum fuer
Informatik, addressDagstuhl, Germany,

[Bonchi et al(2015)]
authorpersonFilippo Bonchi, personPawel
Sobocinski, and personFabio Zanasi.
Full Abstraction for Signal Flow Graphs.
In booktitleProceedings of the 42nd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages
(seriesPOPL '15). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Brunet and Pous(2015)]
authorpersonPaul Brunet and personDamien
Pous. year2015.
Petri Automata for Kleene Allegories. In
booktitle2015 30th Annual ACM/IEEE Symposium on
Logic in Computer Science. pages68–79.

[Bruni et al(2006)]
authorpersonRoberto Bruni, personIvan
Lanese, and personUgo Montanari.
A Basic Algebra of Stateless Connectors.
journalTheoretical Computer Science
volume366, number1 (dateNov.
year2006), pages98–120.

[Carboni and Walters(1987)]
authorpersonA. Carboni and personR. F. C.
Walters. year1987.
Cartesian Bicategories I.
journalJournal of Pure and Applied Algebra
volume49, number1 (dateNov.
year1987), pages11–32.

[Chandra and Merlin(1977)]
authorpersonAshok K. Chandra and
personPhilip M. Merlin. year1977.
Optimal Implementation of Conjunctive Queries in
Relational Data Bases. In booktitleProceedings of the Ninth
Annual ACM Symposium on Theory of Computing
(seriesSTOC '77). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Coecke and Duncan(2008)]
authorpersonBob Coecke and personRoss
Duncan. year2008.
Interacting Quantum Observables. In
booktitleAutomata, Languages and Programming
(seriesLecture Notes in Computer Science),
editorpersonLuca Aceto, personIvan
Damgård, personLeslie Ann Goldberg,
personMagnús M. Halldórsson, personAnna
Ingólfsdóttir, and personIgor Walukiewicz (Eds.).
publisherSpringer, addressBerlin, Heidelberg,

[Coecke and Duncan(2011)]
authorpersonBob Coecke and personRoss
Duncan. year2011.
Interacting Quantum Observables: Categorical
Algebra and Diagrammatics.
journalNew Journal of Physics
volume13, number4 (dateApril
year2011), pages043016.

[Coecke and Kissinger(2017)]
authorpersonBob Coecke and personAleks
Kissinger. year2017.
booktitlePicturing Quantum Processes: A First Course
in Quantum Theory and Diagrammatic Reasoning.
publisherCambridge University Press.

[Coecke et al(2018)]
authorpersonBob Coecke, personJohn Selby,
and personSean Tull. year2018.
Two Roads to Classicality.
volume266 (dateFeb. year2018),

[Comfort et al(2020)]
authorpersonCole Comfort, personAntonin
Delpeuch, and personJules Hedges.
titleSheet Diagrams for Bimonoidal Categories.

[arxiv]2010.13361 [math]

authorpersonRoss Duncan.
Generalised Proof-Nets for Compact
Categories with Biproducts.
In booktitleSemantics of Quantum Computation,
editorpersonSimon Gay and personIan
Mackie (Eds.). publisherCambridge University Press.

authorpersonLeonardo Bigolli Pisani vulgo Fibonacci.
booktitleLiber Abbaci / edidit Enrico Giusti
coadiuvante Paolo D'Alessandro (editionOlschki ed.).
seriesBiblioteca di «Nuncius»,
Vol. volume79.
addressFirenze, Italy.

[Fong et al(2016)]
authorpersonBrendan Fong, personPaweł
Sobociński, and personPaolo Rapisarda.
A Categorical Approach to Open and Interconnected
Dynamical Systems. In booktitleProceedings of the 31st
Annual ACM/IEEE Symposium on Logic in Computer Science
(seriesLICS '16). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Fong and Spivak(2020)]
authorpersonBrendan Fong and personDavid
Spivak. year2020.
String Diagrams for Regular Logic (Extended
Abstract). In booktitleApplied Category Theory 2019
(seriesElectronic Proceedings in Theoretical Computer
Science, Vol. volume323),
editorpersonJohn Baez and personBob
Coecke (Eds.). publisherOpen Publishing Association,

[Freyd and Scedrov(1990)]
authorpersonPeter Freyd and personAndre
Scedrov. year1990.
booktitleCategories, Allegories.
seriesNorth-Holland Mathematical Library,
Vol. volume39.
publisherElsevier B.V.

authorpersonTobias Fritz.
titleA Presentation of the Category of Stochastic

[Ghica and Jung(2016)]
authorpersonDan R. Ghica and personAchim
Jung. year2016.
Categorical semantics of digital circuits. In
booktitle2016 Formal Methods in Computer-Aided Design
(FMCAD). pages41–48.

authorpersonJohn Harding.
Orthomodularity in dagger biproduct categories.
journalPreprint (year2008).

[Hasegawa et al(2008)]
authorpersonMasahito Hasegawa, personMartin
Hofmann, and personGordon Plotkin.
Finite Dimensional Vector Spaces Are Complete
for Traced Symmetric Monoidal Categories.
In booktitlePillars of Computer Science:
Essays Dedicated to Boris (Boaz) Trakhtenbrot on the
Occasion of His 85th Birthday,
editorpersonArnon Avron, personNachum
Dershowitz, and personAlexander Rabinovich (Eds.).
publisherSpringer, addressBerlin, Heidelberg,

authorpersonCharles A. R. Hoare.
An Axiomatic Basis for Computer Programming.
journalCommun. ACM volume12,
number10 (dateOct. year1969),

[Hoare et al(2011)]
authorpersonTony Hoare, personBernhard
Möller, personGeorg Struth, and personIan
Wehrman. year2011.
Concurrent Kleene Algebra and Its
journalThe Journal of Logic and Algebraic
Programming volume80, number6 (dateAug.
year2011), pages266–296.

[Hodkinson and Mikulás(2000)]
authorpersonIan Hodkinson and
personSzabolcs Mikulás. year2000.
Axiomatizability of Reducts of Algebras of
journalAlgebra Universalis volume43,
number2 (dateAug. year2000),

[James and Sabry(2012)]
authorpersonRoshan P. James and personAmr
Sabry. year2012.
Information Effects.
journalACM SIGPLAN Notices volume47,
number1 (dateJan. year2012),

[Johnson and Yau(2022)]
authorpersonNiles Johnson and personDonald
Yau. year2022.
titleBimonoidal Categories, $ E_n $-Monoidal Categories,
and Algebraic $ K $-Theory.  (year2022).

[Joyal and Street(1991)]
authorpersonAndré Joyal and personRoss
Street. year1991.
The Geometry of Tensor Calculus, I.
journalAdvances in Mathematics
volume88, number1 (dateJuly
year1991), pages55–112.

authorpersonDavid Kaiser.
booktitleDrawing Theories Apart: The
Dispersion of Feynman Diagrams in Postwar Physics.
publisherUniversity of Chicago Press.

[Kappé et al(2018)]
authorpersonTobias Kappé, personPaul
Brunet, personAlexandra Silva, and personFabio
Zanasi. year2018.
Concurrent Kleene Algebra: Free Model and
Completeness. In booktitleProgramming Languages and
Systems (seriesLecture Notes in Computer
Science), editorpersonAmal Ahmed (Ed.).
publisherSpringer International Publishing,
addressCham, pages856–882.

authorpersonStephen Lack.
Composing PROPs.
journalTheory and Application of Categories
volume13, number9 (year2004),

authorpersonYves Lafont.
Towards an Algebraic Theory of Boolean
journalJournal of Pure and Applied Algebra
volume184, number2 (dateNov.
year2003), pages257–310.

authorpersonMiguel L. Laplaza.
Coherence for Distributivity. In
booktitleCoherence in Categories
(seriesLecture Notes in Mathematics),
editorpersonG. M. Kelly,
personM. Laplaza, personG. Lewis, and
personSaunders Mac Lane (Eds.). publisherSpringer,
addressBerlin, Heidelberg, pages29–65.

[Mac Lane(1965)]
authorpersonSaunders Mac Lane.
Categorical Algebra.
journalBull. Amer. Math. Soc.
volume71, number1 (year1965),
0002-9904, 1936-881X

[Mac Lane(1978)]
authorpersonS. Mac Lane.
booktitleCategories for the Working
Mathematician (editionsecond ed.). seriesGraduate
Texts in Mathematics, Vol. volume5.
publisherSpringer-Verlag, addressNew

authorpersonPaul-André Melliès.
Functorial Boxes in String Diagrams. In
booktitleComputer Science Logic
(seriesLecture Notes in Computer Science),
editorpersonZoltán Ésik (Ed.).
publisherSpringer, addressBerlin, Heidelberg,

authorpersonDonald Monk.
On representable relation algebras.
journalMichigan Mathematical Journal
volume11, number3 (year1964),
pages207 – 210.

[Muroya et al(2018)]
authorpersonKoko Muroya, personSteven W. T.
Cheung, and personDan R. Ghica.
The Geometry of Computation-Graph Abstraction. In
booktitleProceedings of the 33rd Annual ACM/IEEE Symposium
on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018,
editorpersonAnuj Dawar and personErich
Grädel (Eds.). publisherACM, pages749–758.

authorpersonRoger Penrose.
Applications of Negative Dimensional Tensors.
In booktitleCombinatorial Mathematics and Its
Applications, editorpersonD. J. A. Welsh
(Ed.). publisherAcademic Press.

[Piedeleu and Zanasi(2021)]
authorpersonRobin Piedeleu and personFabio
Zanasi. year2021.
A String Diagrammatic Axiomatisation of
Finite-State Automata. In booktitleFoundations of
Software Science and Computation Structures
(seriesLecture Notes in Computer Science),
editorpersonStefan Kiefer and
personChristine Tasson (Eds.). publisherSpringer
International Publishing, addressCham,

authorpersonDamien Pous.
On the Positive Calculus of Relations with
Transitive Closure. In booktitle35th Symposium on
Theoretical Aspects of Computer Science, STACS 2018, February 28 to March
3, 2018, Caen, France (seriesLIPIcs,
Vol. volume96), editorpersonRolf
Niedermeier and personBrigitte Vallée (Eds.).
publisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik,

authorpersonValentin N Redko.
On defining relations for the algebra of regular
journalUkrainskii Matematicheskii Zhurnal
volume16 (year1964), pages120–126.

[Sagiv and Yannakakis(1980)]
authorpersonYehoshua Sagiv and
personMihalis Yannakakis. year1980.
Equivalences Among Relational Expressions with
the Union and Difference Operators.
journalJ. ACM volume27,
number4 (dateOct. year1980),

authorpersonPeter Selinger.
booktitleA Note on Bainbridge's Power Set
typeTechnical Report. institutionBRICS,
Basic Research in Computer Science, addressAarhus, Denmark.

authorpersonPeter Selinger.
A survey of graphical languages for monoidal
In booktitleNew structures for physics.
publisherSpringer, pages289–355.

authorpersonPeter Selinger.
Finite Dimensional Hilbert Spaces Are Complete
for Dagger Compact Closed Categories.
journalLogical Methods in Computer Science
volumeVolume 8, Issue 3 (dateAug.

authorpersonSam Staton.
Algebraic Effects, Linearity, and Quantum
Programming Languages.
journalACM SIGPLAN Notices volume50,
number1 (dateJan. year2015),

[Stollenwerk and Hadfield(2022)]
authorpersonTobias Stollenwerk and
personStuart Hadfield. year2022.
titleDiagrammatic Analysis for Parameterized Quantum
[arxiv]2204.01307 [quant-ph]

authorpersonAlfred Tarski.
On the Calculus of Relations.
journalThe Journal of Symbolic Logic
volume6, number3 (dateSept.
year1941), pages73–89.
0022-4812, 1943-5886

[Toumi et al(2021)]
authorpersonAlexis Toumi, personRichie
Yeung, and personGiovanni de Felice.
Diagrammatic Differentiation for Quantum Machine
Learning. In booktitleProceedings 18th International
Conference on Quantum Physics and Logic, QPL 2021, Gdansk, Poland, and
online, 7-11 June 2021 (seriesEPTCS,
Vol. volume343), editorpersonChris
Heunen and personMiriam Backens (Eds.).

authorpersonFabio Zanasi.
titleInteracting Hopf Algebras- the Theory
of Linear Systems.
thesistypePh. D. Dissertation. schoolEcole
normale supérieure de Lyon - ENS LYON.

[Zhao and Gao(2021)]
authorpersonChen Zhao and personXiao-Shan
Gao. year2021.
Analyzing the Barren Plateau Phenomenon in Training
Quantum Neural Networks with the ZX-calculus.
journalQuantum  volume5
(dateJune year2021), pages466.

§ COHERENCE AXIOMS

In this Appendix we collect together various Figures, listing the coherence axioms required by the definition of the algebraic structures we consider in the article.

\begin{equation} \label{ax:monoidaltriangle}
\begin{tikzcd}[column sep=tiny]
(X \perG \unoG) \perG Y \arrow[rr, "{\alpha_{X, \unoG, Y}}"] \arrow[rd, "\rho_X \perG id_Y"'] &             & X \perG (1 \perG Y) \arrow[ld, "id_X \perG \lambda_Y"] \\
& X \perG Y &
\end{tikzcd}  \tag{M1}
\end{equation}

\begin{equation}\label{ax:monoidalpentagone}
\begin{tikzcd}[column sep=tiny]
& (X \perG Y) \perG (Z \perG W) \arrow[rd, "{\alpha_{X, Y, Z \perG W}}"] &                                                                                \\
((X \perG Y) \perG Z) \perG W \arrow[ru, "{\alpha_{X \perG Y, Z, W}}"] \arrow[d, "{\alpha_{X,Y,Z} \perG id_W}"'] &                                                                                & X \perG (Y \perG (Z \perG W))                                             \\
(X \perG (Y \perG Z)) \perG W \arrow[rr, "{\alpha_{X, Y \perG Z, W}}"']                                            &                                                                                & X \perG ((Y \perG Z) \perG W) \arrow[u, "{id_X \perG \alpha_{Y,Z,W}}"']
\end{tikzcd}  \tag{M2}
\end{equation}

Coherence axioms of monoidal categories

\begin{equation}\label{eq:symmax1}
\begin{tikzcd}[row sep=normal]
X \perG Y \arrow[r, "{\sigma_{X,Y}}"] \arrow[rd, Rightarrow, no head, shift right] & Y \perG X \arrow[d, "{\sigma_{Y,X}}"] \\
& X \perG Y
\end{tikzcd}  \tag{S1}
\end{equation}

\begin{equation}\label{eq:symmax2}
\begin{tikzcd}[row sep=normal]
X \perG \unoG \arrow[r, "{\sigma_{X,\unoG}}"] \arrow[d, "\rho_X"'] & \unoG \perG X \arrow[d, "\lambda_X"] \\
X \arrow[r, Rightarrow, no head]                                & X
\end{tikzcd}  \tag{S2}
\end{equation}

\begin{equation}\label{eq:symmax3}
\begin{tikzcd}
& X \perG (Y \perG Z) \arrow[r, "{id_X \perG \sigma_{Y,Z}}"] & X \perG (Z \perG Y) \arrow[rd, "{\alpha^-_{X, Z, Y}}"]       &                         \\
(X \perG Y) \perG Z \arrow[ru, "{\alpha_{X, Y, Z}}"] \arrow[rd, "{\sigma_{X \perG Y, Z}}"'] &                                                                  &                                                                     & (X \perG Z) \perG Y \\
& Z \perG (X \perG Y) \arrow[r, "{\alpha^-_{Z, X, Y}}"']    & (Z \perG X) \perG Y \arrow[ru, "{\sigma_{Z, X} \perG id_Y}"'] &
\end{tikzcd}  \tag{S3}
\end{equation}

Coherence axioms of symmetric monoidal categories

\begin{equation}\label{eq:coherence diag}\tag{FP1}
\begin{tikzcd}[column sep=4.5em,baseline=(current  bounding  box.center)]
X \perG Y \ar[r,"\diag{X \perG Y}"] \ar[d,"\diag X \perG \diag Y"'] & (X \perG Y) \perG (X \perG Y) \\
(X \perG Y) \perG (Y \perG Y) \ar[d,"\assoc X X {Y \perG Y}"'] \\
X \perG (X \perG (Y \perG Y)) \ar[d,"\id X \perG \Iassoc X Y Y"'] & X \perG (Y \perG (X \perG Y)) \ar[uu,"\Iassoc X Y {X \perG Y}"'] \\
X \perG ((X \perG Y) \perG Y) \ar[r,"\id X \perG (\symm{X}{Y} \perG \id Y)"] & X \perG ((Y \perG X) \perG Y) \ar[u,"\id X \perG \assoc Y X Y"']
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:coherence bang}\tag{FP2}
\begin{tikzcd}[baseline=(current  bounding  box.center)]
X \perG Y \ar[r,"\bang{X \perG Y}"] \ar[d,"\bang X \perG \bang Y"'] & \unoG \\
\unoG \perG \unoG \ar[ur,"\lunit \unoG"']
\end{tikzcd}
\end{equation}

\begin{equation}\tag{FP3}
\begin{tikzcd}
I \ar[r,shift left=2,"\diag I"] \ar[r,shift right=2,"\Ilunit I"'] & I \perG I
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:bang I = id I}\tag{FP4}
\begin{tikzcd}
I \ar[r,shift left=2,"\bang I"] \ar[r,shift right=2,"\id I"'] & I
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:coherence codiag}\tag{FC1}
\begin{tikzcd}[column sep=4.5em,baseline=(current  bounding  box.center)]
(X \perG Y) \perG (X \perG Y) \ar[dd,"\assoc X Y {X \perG Y}"'] \ar[r,"\codiag{X \perG Y}"] & X \perG Y \\
& (X \perG X) \perG (Y \perG Y) \ar[u,"\codiag X \perG \codiag Y"']\\
X \perG (Y \perG (X \perG Y)) \ar[d,"\id X \perG \Iassoc Y X Y"'] & X \perG (X \perG (Y \perG Y)) \ar[u,"\Iassoc X X {Y \perG Y}"']  \\
X \perG ((Y \perG X) \perG Y) \ar[r,"\id X \perG ( \symm{Y}{X} \perG \id Y)"] & X \perG (( X \perG Y) \perG Y) \ar[u,"\id X \perG \assoc X Y Y"']
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:coherence cobang}\tag{FC2}
\begin{tikzcd}[baseline=(current  bounding  box.center)]
\unoG \ar[r,"\cobang{X \perG Y}"] \ar[d,"\Ilunit \unoG"']  & X \perG Y \\
\unoG \perG \unoG \ar[ur,"\cobang X \perG \cobang Y"']
\end{tikzcd}
\end{equation}

\begin{equation}\tag{FC3}
\begin{tikzcd}
I \perG I \ar[r,shift left=2,"\codiag I"] \ar[r,shift right=2,"\lunit I"'] &  I
\end{tikzcd}
\end{equation}

\begin{equation}\label{eq:cobang I = id I}\tag{FC4}
\begin{tikzcd}
I \ar[r,shift left=2,"\cobang I"] \ar[r,shift right=2,"\id I"'] & I
\end{tikzcd}
\end{equation}

Coherence axioms for (co)commutative (co)monoids

\begin{equation}
\label{eq:rigax1}\tag{R1}
\adjustbox{scale=0.9}{
\begin{tikzcd}[row sep=normal]
{(X\piu Y)Z} & {XZ \piu YZ} \\
{Z(X \piu Y)} & {ZX \piu ZY}
\arrow["{\dr{X}{Y}{Z}}", from=1-1, to=1-2]
\arrow["{\symmt{X \piu Y}{Z}}"', from=1-1, to=2-1]
\arrow["{\dl{Z}{X}{Y}}"', from=2-1, to=2-2]
\arrow["{\symmt{X}{Z} \piu \symmt{Y}{Z}}", from=1-2, to=2-2]
\end{tikzcd}
\end{equation}

\begin{equation}
\label{eq:rigax2}\tag{R2}
\adjustbox{scale=0.9}{\begin{tikzcd}
{(X \piu Y)Z} & {XZ \piu YZ} \\
{(Y \piu X)Z} & {YZ \piu XZ}
\arrow["{\dr{X}{Y}{Z}}", from=1-1, to=1-2]
\arrow["{\symmp{X}{Y}\per \id Z}"', from=1-1, to=2-1]
\arrow["{\dr{Y}{X}{Z}}"', from=2-1, to=2-2]
\arrow["{\symmp{XZ}{YZ}}", from=1-2, to=2-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax3}\tag{R3}
\adjustbox{scale=0.9}{\begin{tikzcd}[column sep=52pt]
{((X \piu Y)\piu Z)W} & {(X \piu Y)W \piu ZW} & {(XW \piu YW) \piu ZW} \\
{(X \piu (Y \piu Z))W} & {XW \piu (Y \piu Z)W} & {XW \piu (YW \piu ZW)}
\arrow["{\dr{X \piu Y}{Z}{W}}", from=1-1, to=1-2]
\arrow["{\assocp{X}{Y}{Z} \per id_W}"', from=1-1, to=2-1]
\arrow["{\dr{X}{Y \piu Z}{W}}"', from=2-1, to=2-2]
\arrow["{\dr{X}{Y}{W} \per id_{ZW}}", from=1-2, to=1-3]
\arrow["{id_{XW} \per \dr{Y}{Z}{W}}"', from=2-2, to=2-3]
\arrow["{\assocp{XW}{YW}{ZW}}", from=1-3, to=2-3]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax4}\tag{R4}
\adjustbox{scale=0.9}{\begin{tikzcd}[column sep=56pt]
{((X \piu Y)Z)W} & {(XZ \piu YZ)W} & {(XZ)W \piu (YZ)W} \\
{(X \piu Y)(ZW)} && {X(ZW) \piu Y(ZW)}
\arrow["{\assoct{X\piu Y}{Z}{W}}"', from=1-1, to=2-1]
\arrow["{\dr{X}{Y}{Z} \per \id W}", from=1-1, to=1-2]
\arrow["{\dr{XZ}{YZ}{W}}", from=1-2, to=1-3]
\arrow["{\assoct{X}{Z}{W} \piu \assoct{Y}{Z}{W}}", from=1-3, to=2-3]
\arrow["{\dr{X}{Y}{ZW}}"', from=2-1, to=2-3]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax5}\tag{R5}
\adjustbox{scale=0.9}{\begin{tikzcd}[column sep=normal]
{(X \piu Y)(Z \piu W)} & {X(Z \piu W) \piu Y(Z \piu W)} & {} \\
{(X \piu Y)Z \piu (X \piu Y)W} & {(XZ \piu XW) \piu (YZ \piu YW)} \\
{(XZ \piu YZ) \piu (XW \piu YW)} & {XZ \piu (XW \piu (YZ \piu YW))} \\
{XZ \piu (YZ \piu (XW \piu YW))} & {XZ \piu ((XW \piu YZ) \piu YW)} \\
{XZ \piu ((YZ \piu XW) \piu YW)} & {XZ \piu ((YZ \piu XW) \piu YW)}
\arrow["{\dr{X}{Y}{Z \piu W}}", from=1-1, to=1-2]
\arrow[Rightarrow, no head, from=5-1, to=5-2]
\arrow["{\dl{X \piu Y}{Z}{W}}"', from=1-1, to=2-1]
\arrow["{\dr{X}{Y}{Z} \piu \dr{X}{Y}{W}}"', from=2-1, to=3-1]
\arrow["{\assocp{XZ}{YZ}{XW \piu YW}}"', from=3-1, to=4-1]
\arrow["{id_{XZ} \piu \Iassocp{YZ}{XW}{YW}}"', from=4-1, to=5-1]
\arrow["{\dl{X}{Z}{W} \piu \dl{Y}{Z}{W}}", from=1-2, to=2-2]
\arrow["{\assocp{XZ}{XW}{YZ \piu YW}}", from=2-2, to=3-2]
\arrow["{id_{XZ} \piu \Iassocp{XW}{YZ}{YW}}", from=3-2, to=4-2]
\arrow["{id_{XZ} \piu (\symmp{XW}{YZ} \piu id_{YW})}", from=4-2, to=5-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax6}\tag{R6}
\adjustbox{scale=0.9}{\begin{tikzcd}
{\zero \per \zero} & \zero
\arrow["{\annl \zero}", shift left=2, from=1-1, to=1-2]
\arrow["{\annr \zero}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax7}\tag{R7}
\adjustbox{scale=0.9}{\begin{tikzcd}
{(X \piu Y)\zero} & {X\zero \piu Y\zero} \\
\zero & {\zero \piu \zero}
\arrow["{\lunitp{\zero}}", from=2-2, to=2-1]
\arrow["{\annr{X \piu Y}}"', from=1-1, to=2-1]
\arrow["{\annr X \piu \annr Y}", from=1-2, to=2-2]
\arrow["{\dr{X}{Y}{\zero}}", from=1-1, to=1-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax8}\tag{R8}
\adjustbox{scale=0.9}{\begin{tikzcd}
{\zero \per \uno} & \zero
\arrow["{\annl \uno}", shift left=2, from=1-1, to=1-2]
\arrow["{\runitt \zero}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax9}\tag{R9}
\adjustbox{scale=0.9}{\begin{tikzcd}[column sep=15pt]
{X \per \zero} && {\zero \per X} \\
& \zero
\arrow["{\annl X}", from=1-3, to=2-2]
\arrow["{\symmt{X}{\zero}}", from=1-1, to=1-3]
\arrow["{\annr X}"', from=1-1, to=2-2]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax10}\tag{R10}
\adjustbox{scale=0.9}{\begin{tikzcd}
{(XY)0} && {X(Y\zero)} \\
\zero && X\zero
\arrow["{\assoct{X}{Y}{\zero}}", from=1-1, to=1-3]
\arrow["{id_X \per \annr Y}", from=1-3, to=2-3]
\arrow["{\annr{XY}}"', from=1-1, to=2-1]
\arrow["{\annr X}", from=2-3, to=2-1]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax11}\tag{R11}
\adjustbox{scale=0.9}{\begin{tikzcd}
{(\zero \piu X)Y} && {\zero Y \piu XY} \\
XY && {\zero \piu XY}
\arrow["{\dr{\zero}{X}{Y}}", from=1-1, to=1-3]
\arrow["{\annl Y \piu id_{XY}}", from=1-3, to=2-3]
\arrow["{\lunitp{X} \per \id Y}"', from=1-1, to=2-1]
\arrow["{\lunitp{XY}}", from=2-3, to=2-1]
\end{tikzcd}}
\end{equation}

\begin{equation}
\label{eq:rigax12}\tag{R12}
\adjustbox{scale=0.9}{\begin{tikzcd}[column sep=tiny]
{(X \piu Y)\uno} && {X\uno \piu Y\uno } \\
& {X \piu Y}
\arrow["{\dr{X}{Y}{\uno}}", from=1-1, to=1-3]
\arrow["{\runitt X \piu \runitt Y}", from=1-3, to=2-2]
\arrow["{\runitt{X \piu Y}}"', from=1-1, to=2-2]
\end{tikzcd}}
\end{equation}

Coherence Axioms of symmetric rig categories

\begin{equation}
\label{eq:dl1}
\begin{tikzcd}[row sep=normal]
{X(Y\piu Z)} & {XY \piu XZ} \\
{X(Z\piu Y)} & {XZ \piu XY}
\arrow["{\dl{X}{Y}{Z}}", from=1-1, to=1-2]
\arrow["{id_X \per \symmp{Y}{Z}}"', from=1-1, to=2-1]
\arrow["{\dl{X}{Z}{Y}}"', from=2-1, to=2-2]
\arrow["{\symmp{XY}{XZ}}", from=1-2, to=2-2]
\end{tikzcd}     \end{equation}

\begin{equation}
\label{eq:dl2}
\begin{tikzcd}[column sep=52pt]
X[(Y \piu Z) \piu W] \ar[r,"\dl{X}{Y \piu Z}{W}"] \ar[d,"\id{X} \per \assocp Y Z W"'] & X(Y \piu Z) \piu XW \ar[r,"\dl{X}{Y}{Z} \piu \id{XW}"] & (XY \piu XZ) \piu XW \ar[d,"\assocp {XY}{XZ}{XW}"] \\
X[Y\piu(Z \piu W)] \ar[r,"\dl{X}{Y}{Z \piu W}"] & XY \piu X(Z \piu W) \ar[r,"\id{XY} \piu \dl{X}{Z}{W}"] & XY \piu (XZ \piu XW)
\end{tikzcd}     \end{equation}

\begin{equation}
\label{eq:dl3}
\begin{tikzcd}[column sep=48pt]
{(XY)(Z \piu W)} && {(XY)Z \piu (XY)W} \\
{X(Y(Z \piu W))} & {X(YZ \piu YW)} & {X(YZ) \piu X(YW)}
\arrow["{\assoct{X}{Y}{Z \piu W}}"', from=1-1, to=2-1]
\arrow["{id_X \per \dl{Y}{Z}{W}}"', from=2-1, to=2-2]
\arrow["{\dl{X}{YZ}{YW}}"', from=2-2, to=2-3]
\arrow["{\assoct{X}{Y}{Z} \piu \assoct{X}{Y}{W}}", from=1-3, to=2-3]
\arrow["{\dl{XY}{Z}{W}}", from=1-1, to=1-3]
\end{tikzcd}     \end{equation}

\begin{equation}
\label{eq:dl4}
\begin{tikzcd}
{\zero(X \piu Y)} & {\zero X \piu \zero Y} \\
\zero & {\zero \piu \zero}
\arrow["{\lunitp{\zero}}", from=2-2, to=2-1]
\arrow["{\annl{X \piu Y}}"', from=1-1, to=2-1]
\arrow["{\annl X \piu \annl Y}", from=1-2, to=2-2]
\arrow["{\dl{\zero}{X}{Y}}", from=1-1, to=1-2]
\end{tikzcd}     \end{equation}

\begin{equation}
\label{eq:dl5}
\begin{tikzcd}
{X(\zero \piu Y)} && {X\zero \piu XY} \\
XY && {\zero \piu XY}
\arrow["{\dl{X}{\zero}{Y}}", from=1-1, to=1-3]
\arrow["{\annr X \piu id_{XY}}", from=1-3, to=2-3]
\arrow["{id_X \per \lunitp{Y}}"', from=1-1, to=2-1]
\arrow["{\lunitp{XY}}", from=2-3, to=2-1]
\end{tikzcd}     \end{equation}

\begin{equation}
\label{eq:dl7}
\begin{tikzcd}
{X(Y\piu \zero)} && {XY \piu X\zero} \\
XY && {XY \piu \zero}
\arrow["{\dl{X}{Y}{\zero}}", from=1-1, to=1-3]
\arrow["{ id_{XY} \piu \annr X}", from=1-3, to=2-3]
\arrow["{id_X \per \runitp{Y}}"', from=1-1, to=2-1]
\arrow["{\runitp{XY}}", from=2-3, to=2-1]
\end{tikzcd}         \end{equation}

\begin{equation}
\label{eq:dl8}
\begin{tikzcd}
{(X \piu \zero)Y} && {XY \piu \zero Y} \\
XY && {XY \piu \zero}
\arrow["{\dr{X}{\zero}{Y}}", from=1-1, to=1-3]
\arrow["{\id{XY} \piu \annl{Y}}", from=1-3, to=2-3]
\arrow["{\runitp{X} \per \id Y}"', from=1-1, to=2-1]
\arrow["{\runitp{XY}}", from=2-3, to=2-1]
\end{tikzcd}         \end{equation}

\begin{equation}
\label{eq:dl6}
\begin{tikzcd}[column sep=tiny]
{\uno(X \piu Y)} && {\uno X \piu \uno Y } \\
& {X \piu Y}
\arrow["{\dl{\uno}{X}{Y}}", from=1-1, to=1-3]
\arrow["{\lunitp X \piu \lunitp Y}", from=1-3, to=2-2]
\arrow["{\lunitp{X \piu Y}}"', from=1-1, to=2-2]
\end{tikzcd}     \end{equation}

Derived laws of symmetric rig categories

§ ADDITIONAL FIGURES

In this Appendix we provide some additional figures representing useful/interesting axioms and derivations.

\[
\tikzfig{topos/deriv1/step1} \axeq{\substack{\refeq{ax:diagun} \\ \refeq{ax:codiagun}}} \tikzfig{topos/deriv1/step2} \axeq{\refeq{ax:bangnat}} \tikzfig{topos/deriv1/step3} \axsubeq{\refeq{ax:relBangCobang}} \tikzfig{topos/deriv1/step4}
\]

\[
\tikzfig{topos/deriv1/step4} \axsubeq{\substack{\refeq{ax:dischargeradj2} \\ \refeq{ax:dischargernat}}} \tikzfig{topos/deriv2/step3} \axeq{\substack{\refeq{ax:copierun} \\ \refeq{ax:cocopierun}}} \tikzfig{topos/deriv2/step6} \axeq{\refeq{ax:diagnat}} \tikzfig{topos/deriv2/step7} \axsubeq{\refeq{ax:relDiagCodiag}} \tikzfig{topos/deriv1/step1}
\]

Graphical proof for $R \cup (R \cap S) \equiv_{\CR} R$

2*zx/idemp_left $\axeq{\text{res}}$ zx/idemp_right    zx/inner_product $\axeq{\text{id}}$ zx/onb1_right with $i,j \in \{0, 1\}$ and $i = j$

zx/inner_product $\axeq{\emptyset}$ zx/onb2_right with $i,j \in \{0, 1\}$ and $i\neq j$

The axioms above are a graphical rendering of the necessary and sufficient conditions for $\ket{0}$ and $\ket{1}$
to form an orthonormal basis (see <cit.>). In particular, axiom $(\text{id})$ asserts that the basis vectors have norm $1$, while $(\emptyset)$ says that they are orthogonal to each other.

\[ \Ctotrel{\uno} = \Ccoreg{\leq}{\uno} \sqcup \Creg{\geq}{\uno} \qquad \qquad \tikzfig{tapes/totrel} = \tikzfig{tapes/leq_geq} \]

The axiom of GPLA <cit.> on the left expresses the totality of an ordering relation $\leq$. Within tape diagrams the same axiom can be rendered completely graphically as shown on the right.

\begin{equation}\label{eq:bangcobang}
\TPolycounitunit{P}{Q}
\stackrel{\eqref{ax:cobangnat}}{=}
\TPolyCounit{P} \; \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (35) at (-2, -0.5) {};
\node [style=none] (36) at (-2, 0.5) {};
\node [style=dots] (90) at (1.5, 0.025) {$\vdots$};
\node [style=none] (91) at (2, -0.5) {};
\node [style=none] (92) at (2, 0.5) {};
\node [style=label] (94) at (-1.5, 1) {$P$};
\node [style=label] (95) at (1.5, 1) {$Q$};
\node [style=none] (96) at (-0.75, -1) {};
\node [style=none] (97) at (0.75, -1) {};
\node [style=none] (98) at (0.75, 1) {};
\node [style=none] (99) at (-0.75, 1) {};
\node [style=none] (104) at (0, 0) {$\t$};
\node [style=dots] (105) at (-1.5, 0.025) {$\vdots$};
\node [style=none] (106) at (-0.75, -0.5) {};
\node [style=none] (107) at (0.75, -0.5) {};
\node [style=none] (108) at (0.75, 0.5) {};
\node [style=none] (109) at (-0.75, 0.5) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [style=tape] (97.center)
to (96.center)
to (106.center)
to (35.center)
to [bend left=90, looseness=1.75] (36.center)
to (109.center)
to (99.center)
to (98.center)
to (108.center)
to (92.center)
to (91.center)
to (107.center)
to cycle;
\end{pgfonlayer}
\end{tikzpicture}
\stackrel{\eqref{ax:relBangCobang}}{\leq}
\Tbox{t}{P}{Q}
\end{equation}

\begin{equation*}
\Tbox{t}{P}{Q}
\stackrel{\left( \substack{\refeq{ax:diagun} \\ \refeq{ax:codiagun}} \right)}{=}
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (8) at (-0.95, -2) {};
\node [style=none] (9) at (-0.75, 2) {};
\node [style=none] (10) at (-0.75, 1) {};
\node [style=none] (11) at (-1.75, 0) {};
\node [style=none] (12) at (-0.95, -1) {};
\node [style=none] (13) at (-2.75, -0.5) {};
\node [style=none] (14) at (-2.75, 0.5) {};
\node [style=none] (24) at (-4, 0) {};
\node [style=none] (35) at (-4, -0.5) {};
\node [style=none] (36) at (-4, 0.5) {};
\node [style=none] (83) at (0.95, -2) {};
\node [style=none] (84) at (0.75, 2) {};
\node [style=none] (85) at (0.75, 1) {};
\node [style=none] (86) at (1.75, 0) {};
\node [style=none] (87) at (0.95, -1) {};
\node [style=none] (88) at (2.75, -0.5) {};
\node [style=none] (89) at (2.75, 0.5) {};
\node [style=none] (90) at (4, 0) {};
\node [style=none] (91) at (4, -0.5) {};
\node [style=none] (92) at (4, 0.5) {};
\node [style=label] (94) at (-3.25, 1) {$P$};
\node [style=label] (95) at (3.25, 1) {$Q$};
\node [style=none] (96) at (-0.75, 0.5) {};
\node [style=none] (97) at (0.75, 0.5) {};
\node [style=none] (98) at (0.75, 2.5) {};
\node [style=none] (99) at (-0.75, 2.5) {};
\node [style=none] (104) at (0, 1.5) {$\t$};
\node [style=dots] (106) at (3.25, 0.025) {$\vdots$};
\node [style=dots] (107) at (-3.25, 0.025) {$\vdots$};
\node [style=dots] (108) at (0.95, -1.475) {$\vdots$};
\node [style=dots] (109) at (-0.95, -1.475) {$\vdots$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [style=tape] (11.center)
to [bend left=45] (10.center)
to (96.center)
to (97.center)
to (85.center)
to [bend left=45] (86.center)
to [bend left=45] (87.center)
to [bend right=90, looseness=2.00] (83.center)
to [bend right] (88.center)
to (91.center)
to (92.center)
to (89.center)
to [bend right] (84.center)
to (98.center)
to (99.center)
to (9.center)
to [bend right] (14.center)
to (36.center)
to (35.center)
to (13.center)
to [bend right] (8.center)
to [bend right=90, looseness=1.75] (12.center)
to [bend left=45] cycle;
\end{pgfonlayer}
\end{tikzpicture}
\stackrel{\eqref{eq:bangcobang}}{\leq}
\Tconv{\t}{\t}{P}{Q}
\stackrel{\eqref{ax:diagnat}}{=}
\Ttconv{\t}{P}{Q}
\stackrel{\eqref{ax:relDiagCodiag}}{\leq}
\Tbox{\t}{P}{Q}
\end{equation*}

Graphical derivation proving that with the axioms in Figure <ref> $+$ becomes idempotent with $\zerotape$ as bottom element

cbString/symm_inv_left     $\axeq{\sigma^{\per}\text{-inv}}$     cbString/symm_inv_right     cbString/symm_nat_left     $\axeq{\sigma^{\per}\text{-nat}}$     cbString/symm_nat_right

cbString/monoid_assoc_left     $\axeq{\copier{}\text{-as}}$     cbString/monoid_assoc_right     cbString/comonoid_assoc_left     $\axeq{\cocopier{}\text{-as}}$     cbString/comonoid_assoc_right

cbString/monoid_unit_left     $\axeq{\copier{}\text{-un}}$     cbString/monoid_unit_right     cbString/comonoid_unit_left     $\axeq{\cocopier{}\text{-un}}$     cbString/comonoid_unit_right

cbString/monoid_comm_left     $\axeq{\copier{}\text{-co}}$     cbString/monoid_comm_right     cbString/comonoid_comm_left     $\axeq{\cocopier{}\text{-co}}$     cbString/comonoid_comm_right

cbString/spec_frob_left     $\axeq{S}$     cbString/monoid_unit_right     cbString/frob_left     $\axeq{F}$     cbString/frob_center

cbString/copier_nat_left     $\axsubeq{\copier{}\text{-nat}}$     cbString/copier_nat_right     cbString/discharger_nat_left     $\axsubeq{\discharger{}\text{-nat}}$     cbString/discharger_nat_right

cbString/adjoint1_bangs_left     $\axsubeq{\codischarger{}\discharger{}}$     cbString/empty     cbString/monoid_unit_right     $\axsubeq{\discharger{}\codischarger{}}$     cbString/adjoint2_bangs_right

cbString/frob_center     $\axsubeq{\cocopier{}\copier{}}$     cbString/adjoint1_diags_right     cbString/monoid_unit_right     $\axsubeq{\copier{}\cocopier{}}$     cbString/spec_frob_left

Axioms of $\Cat{CB}_\Sigma$

§ APPENDIX TO SECTION <REF>

In this Appendix we show how Definition <ref> is equivalent to the more standard definition of a category with finite biproducts.

Traditionally a category $\Cat C$ with a zero object $\zero$ is said to have finite biproducts if for every pair of objects $X_1$ and $X_2$ there exists a third object $X_1 \piu X_2$ and morphisms $\proj i \colon  X_1 \piu X_2 \to X_i$, $\inj i \colon X_i \to X_1 \piu X_2$ such that $(X_1 \piu X_2, \proj 1, \proj 2)$ is a product, $(X_1 \piu X_2, \inj 1, \inj 2)$ is a coproduct and

\[\inj i ; \proj j = \delta_{i,j}\]

where $\delta_{i,j} = \id{X_i}$ if $i = j$, otherwise $\delta_{i,j} = \zero_{X_i,X_j}$ (i.e. $\bang{X_i}; \cobang{X_j}$). This is consistent with Definition <ref>, as we show now.

For any two objects $X_1$, $X_2$ of a  fb-category $\Cat C$, $X_1 \perG X_2$ is the categorical product $X_1 \times X_2$: the projections $\pi_1\colon X_1 \perG X_2 \to X_1$ and $\pi_2\colon X_1 \perG X_2 \to X_2$ are

\[\begin{tikzcd}[column sep=3em]
X_1 \perG X_2 \ar[r,"\id{X_1} \perG \, \bang{X_2}"] &  X_1 \perG \unoG \ar[r,"\runit{X_1}"]  & X_1
\end{tikzcd}
\quad \text{and} \quad
\begin{tikzcd}[column sep=3em]
X_1 \perG X_2 \ar[r," \bang{X_1} \perG \id{X_2} "] &  \unoG \perG X_2 \ar[r,"\lunit{X_2}"]  & X_2.
\end{tikzcd}
\]

The unit $\unoG$ is the terminal object and $\bang X$ the unique morphism of type $X \to \unoG$.
For $f_1\colon Y\to X_1$, $f_2 \colon Y \to X_2$, their pairing $\pairing{f_1,f_2}\colon Y \to X_1 \perG X_2$ is given by
\[\begin{tikzcd}
Y  \ar[r,"\diag{Y}"] & Y \perG Y \ar[r,"f_1 \perG f_2"] &  X_1 \perG X_2.
\end{tikzcd}\]

$X_1 \perG X_2$ is also a categorical coproduct, with injections $\inj i \colon X_i \to X_1 \perG X_2$ and copairing $\copairing{f_1,f_2} \colon X_1 \perG X_2 \to Y$, for $f_1 \colon X_1 \to Y$ and $f_2 \colon X_2 \to Y$, in the dual way. Also dually $\unoG$ is the initial object and $\cobang X$ the unique morphism of type $\unoG \to X$.

Hence  $\unoG$ is a zero object and $\bang X ; \cobang Y \colon X \to Y$ is a zero morphism. Also the third requirement $\inj i ; \proj j = \delta_{i,j}$ holds. Indeed,

\[
\begin{tikzcd}[column sep=3em]
X_1 \ar[r,"\Irunit {X_1}"] \ar[ddrr,bend right,"\id{X_1}"'] \ar[rr,start anchor=north east,bend left,"\inj 1"] & X_1 \piu \zero \ar[r,"{\id{X_1} \piu \cobang{X_2} }"] \ar[dr,"\id{X_1} \piu \cobang{X_2};\bang{X_2}"description] \ar[dr,bend right=45,"\id{X_1} \piu \id\zero"'] & X_1 \piu X_2 \ar[d,"\id{X_1} \piu \, \bang{X_2}"] \ar[dd,"\proj 1",rounded corners,to path={[pos=0.75] -|
([xshift=12em]\tikztotarget.east)	\tikztonodes --  (\tikztotarget)  }]
\\
& & X_1 \piu \zero \ar[d,"\runit{X_1}"] \\
& & X_1
\end{tikzcd}
\qquad
\begin{tikzcd}
X_2 \ar[r,"\Ilunit {X_2}"] \ar[ddrr,bend right,"\id{X_2}"'] \ar[rr,start anchor=north east,bend left,"\inj 2"] & \zero \piu X_2 \ar[r,"{ \cobang{X_1} } \piu \id{X_2}"] \ar[dr,"\cobang{X_1};\bang{X_1} \piu \id{X_2}"description] \ar[dr,bend right=45,"\id\zero \piu \id{X_2}"'] & X_1 \piu X_2 \ar[d," \bang{X_1} \piu \id{X_2}"] \ar[dd,"\proj 2",rounded corners,to path={[pos=0.75] -|
([xshift=12em]\tikztotarget.east)	\tikztonodes --  (\tikztotarget)  }] \\
& & \zero \piu X_2 \ar[d,"\lunit{X_2}"] \\
& & X_2
\end{tikzcd}
\]

\[
\begin{tikzcd}
X_1 \ar[r,"\Irunit {X_1}"] \ar[d,"\bang{X_1}"'] \ar[rr,start anchor=north east,bend left,"\inj 1"] & X_1 \piu \zero \ar[r,"{\id{X_1} \piu \cobang{X_2} }"] \ar[d,"\bang{X_1} \piu \id\zero"]  & X_1 \piu X_2 \ar[d," \bang{X_1} \piu \id{X_2}"] \ar[dd,"\proj 2",rounded corners,to path={[pos=0.75] -|
([xshift=12em]\tikztotarget.east)	\tikztonodes --  (\tikztotarget)  }] \\
\zero \ar[r,"\Irunit\zero"] \ar[dr,"\id{\zero}"'] & \zero \piu \zero \ar[r,"\id\zero \piu \cobang{X_2}"] \ar[d,"\lunit\zero"] & \zero \piu X_2 \ar[d,"\lunit{X_2}"] \\
& \zero \ar[r,"\cobang{X_2}"] & X_2
\end{tikzcd}
\qquad
\begin{tikzcd}
X_2 \ar[r,"\Ilunit {X_2}"] \ar[d,"\bang{X_2}"']  \ar[rr,start anchor=north east,bend left,"\inj 2"] & \zero \piu X_2 \ar[r,"\cobang{X_1} \piu \id{X_2}"] \ar[d,"\id\zero \piu \bang{X_2}"] & X_1 \piu X_2 \ar[d,"\id{X_1} \piu \bang{X_2}"] \ar[dd,"\proj 1",rounded corners,to path={[pos=0.75] -|
([xshift=12em]\tikztotarget.east)	\tikztonodes --  (\tikztotarget)  }] \\
\zero \ar[r,"\Ilunit\zero"] \ar[dr,"\id{\zero}"'] & \zero \piu \zero \ar[r,"\cobang{X_1} \piu \id\zero"] \ar[d,"\runit\zero"] & X_1 \piu \zero \ar[d,"\runit{X_1}"] \\
& \zero \ar[r,"\cobang{X_1}"] & X_1
\end{tikzcd}
\]

commute, using naturality of $\lunit{}$, $\runit{}$ and the fact that $\lunit\zero = \runit\zero$.

§ APPENDIX TO SECTION <REF>

In this Appendix we state and prove some additional facts for fb-rig categories (Proposition <ref>) and for sesquistrict rig categories (Lemma <ref>), which combined together yield Lemma <ref> for sesquistrict fb rig categories. We also introduce the notion of monomial and polynomial for arbitrary sesquistrict rig categories (Definition <ref>). Finally, we give the proofs of the results claimed in Section <ref>, namely Theorem <ref>, Lemma <ref> and Theorem <ref>.

In any fb-rig category the following diagrams commute:

\[
\begin{tikzcd}
X \per (Y \piu Y) \ar[dr,"{\dl X Y Y}"] \\
X \per Y \ar[u,"\id X \per \diag Y"] \ar[r,"\diag{X \per Y}"] \ar[d,"\diag X \per \id Y"'] & (X \per Y) \piu (X \per Y) \\
(X \piu X) \per Y \ar[ur,"{\dr X X Y}"']
\end{tikzcd}
\qquad
\begin{tikzcd}[column sep=4em]
X \per \zero \ar[dr,"\annr X"] \\
X \per Y \ar[u,"\id X \per \bang Y"] \ar[r,"\bang{X \per Y}"] \ar[d,"\bang X \per \id Y"'] & \zero \\
\zero \per Y \ar[ur,"\annl Y"']
\end{tikzcd}
\]

Dually, also the following diagrams commute:

\[
\begin{tikzcd}[column sep=4em]
X \per (Y \piu Y) \ar[dr,"\id X \per \codiag Y"] \\
(X \per Y) \piu (X \per Y) \ar[u,"{\Idl X Y Y}"] \ar[r,"\codiag{X \per Y}"] \ar[d,"{\Idr X Y Y}"'] & X \per Y \\
(X \piu X) \per Y \ar[ur,"\codiag X \per \id Y"']
\end{tikzcd}
\qquad
\begin{tikzcd}
X \per \zero \ar[dr,"\id X \per \cobang Y"] \\
\zero \ar[u,"\Iannr X"] \ar[r,"\cobang{X \per Y}"] \ar[d,"\Iannl Y"'] & X \per Y \\
\zero \per Y \ar[ur,"\cobang X \per \id Y"']
\end{tikzcd}
\]

The diagrams involving $\zero$ are trivially commuting due to the fact that it is a zero object.

We show that $\diag{X \per Y} = (\diag X \per \id Y) ; \dr X X Y$. To do that, we prove that the morphism $(\diag X \per \id Y) ; \dr X X Y$ satisfies the same universal property of $\diag{X \per Y} = \pairing{\id{X \per Y}, \id{X \per Y}}$; in other words we show that

* $(\diag X \per \id Y) ; \dr X X Y ; \proj 1 = \id{X \per Y}$,

* $(\diag X \per \id Y) ; \dr X X Y ; \proj 2 = \id{X \per Y}$

where $\proj 1, \proj 2 \colon (X \per Y) \piu (X \per Y) \to X \per Y$. Recall that $\proj 1 = (\id{X \per Y} \piu \bang{X \per Y}) ; \runitp{X \per Y}$ and that $\proj 2 = (\bang{X \per Y} \piu \id{X \per Y}) ; \lunitp{X \per Y}$. We have that the following diagram commutes:

\[
\begin{tikzcd}[column sep={3.5em,},bend angle=10,row sep=3em]
& (X \piu X) \per Y \ar[r,"{\dr X X Y}"] \ar[d,"(\id X \piu \bang X) \per \id Y"{description,name=f}] & (X \per Y) \piu (X \per Y)  \ar[r,"\id{X \per Y} \piu \bang{X \per Y}"] \ar[d,"(\id X \per \id Y) \piu (\bang X \per \id Y)"{description,name=g}] & (X \per Y) \piu \zero \ar[dr,"\runitp{X \per Y}"]\\
X \per Y \ar[ur,"\diag X \per \id Y"]
\arrow[rrrr,"\id{X \per Y}"',rounded corners,to path={ -- ([yshift=-5cm]\tikztostart.south) -- ([yshift=-5cm]\tikztotarget.south) \tikztonodes -| ([yshift=-2cm]\tikztotarget.south) -- (\tikztotarget)}]
& (X \piu \zero) \per Y \ar[r,"{\dr X \zero Y}"] \ar[rrr,bend right,"\runitp X \per \id Y"'] & (X \per Y) \piu (\zero \per X) \ar[ur,swap,"\id{X \per Y} \piu \annl X"name=h] \ar[rr,draw=none,"\ast_3"description] & & X \per Y \\[-1em]
& & \ast_4
\arrow[from=f,to=g,draw=none,"\ast_1"description]
\arrow[from=1-3,to=h,draw=none,"\ast_2"description]
\end{tikzcd}
\]

because of the naturality of $\delta^r$ ($\ast_1$), terminality of $\zero$ ($\ast_2$), the derived law (<ref>) ($\ast_3$) and the fact that $\diag X ; \proj 1 = \id X$ ($\ast_4$). This proves the first equality. As per the second, for similar reasons the following diagram commutes:

\[
\begin{tikzcd}[column sep={3.5em,},bend angle=10,row sep=3em]
& (X \piu X) \per Y \ar[r,"{\dr X X Y}"] \ar[d,"(\bang X \piu \id X) \per \id Y"{description,name=f}] & (X \per Y) \piu (X \per Y)  \ar[r,"\bang{X \per Y} \piu \id{X \per Y}"] \ar[d,"(\bang X \per \id Y) \piu (\id X \per \id Y)"{description,name=g}] & \zero \piu (X \per Y)  \ar[dr,"\lunitp{X \per Y}"]\\
X \per Y \ar[ur,"\diag X \per \id Y"]
\arrow[rrrr,"\id{X \per Y}"',rounded corners,to path={ -- ([yshift=-5cm]\tikztostart.south) -- ([yshift=-5cm]\tikztotarget.south) \tikztonodes -| ([yshift=-2cm]\tikztotarget.south) -- (\tikztotarget)}]
& (\zero \piu X) \per Y \ar[r,"{\dr \zero X Y}"] \ar[rrr,bend right,"\lunitp X \per \id Y"'] & (\zero \per Y) \piu (X \per Y) \ar[ur,swap,"\annl Y \piu \id{X \per Y}"name=h] \ar[rr,draw=none,"\ast_5"description] & & X \per Y \\
\end{tikzcd}
\]

where now $\ast_5$ commutes because of Axiom (<ref>).

The fact that $\codiag{X \per Y} = \Idr X X Y ; (\codiag X \per \id Y)$ can be proved in a similar way using the derived laws (<ref>) and (<ref>).

§.§ Additional facts for sesquistrict rig categories

Let $H \colon \Cat M \to \Cat D$ be a sesquistrict rig category. A monomial in $\Cat D$ is an object of the form $\Per[j=1][m]{H(A_j)}$ where $A_j \in \Cat M$. A polynomial in $\Cat D$ is an object of the form $\Piu[i=1][n] U_i$ where $U_i$ is a monomial for all $i=1\dots n$.

Let $H \colon \Cat M \to \Cat D$ be a sesquistrict rig category. For all monomials $U,V$ and polynomials $Y,Z$, the following hold:

* $\dl{U}{Y}{Z}=\id{UY \piu UZ}$.

* If  $Y=\Piu[i]{U_i}$, then $\symmt{Y}{V} = \Piu[i]{\symmt{U_i}{V}}$.

We prove the first item by induction on $U$.

Case $U = \uno$: $\dl{1}{Y}{Z} \axeq{\ref{eq:dl6}}\id{Y\piu Z}$.

Case $U = H(A)U'$:

\begin{align*}
\dl{H(A)U'}{Y}{Z} &= \tag{\ref{eq:dl3}} (\id{H(A)} \per \dl{U'}{Y}{Z}) ; \dl{H(A)}{U'Y}{U'Z} \\
&= \tag{Ind. hp., sesquistrictness} (\id{H(A)} \per \id{U'Y\piu U'Z}) ; \id{H(A)U'Y \piu H(A)U'Z } \\
&= \id{H(A)U'Y \piu H(A)U'Z }
\end{align*}

We prove the second point by induction on $Y$.

Case $Y = \zero$: it follows from axiom (<ref>).

Case $Y = U \piu Y'$: Let $Y' = \Piu[i']{U'_{i'}}$

\begin{align*}
\symmt{U \piu Y'}{V} &= \tag{\ref{eq:rigax1}} (\symmt{U}{V} \piu \symmt{Y'}{V}) ; \Idl{V}{U}{Y'} \\
&= \tag{Lemma \ref{lm:sesqui:symmt}.1} \symmt{U}{V} \piu \symmt{Y'}{V} \\
&= \tag{Ind. hp.} \symmt{U}{V} \piu \Piu[i']{\symmt{U'_{i'}}{V}}
\end{align*}

The following useful result is an immediate consequence of Proposition <ref> and Lemma <ref>.

Let $H \colon \Cat M \to \Cat D$ be a sesquistrict fb rig category, $U$ a monomial and $Y$ a polynomial. Then:

* $\id{U} \per \diag{Y} = \diag{UY} = \diag{U} \per \id{Y}$.

* $\id{U} \per \bang{Y} = \bang{UY} = \bang{U} \per \id{Y}$.

* $\id{U} \per \codiag{Y} = \codiag{UY} = \codiag{U} \per \id{Y}$.

* $\id{U} \per \cobang{Y} = \cobang{UY} = \cobang{U} \per \id{Y}$.

§.§ Proofs of Section <ref>

We recall from <cit.> some facts regarding the strictification $\sCatT C$ of $\Cat C$.

Let $P=\Piu[i=1][r]{U_i}$ and $Q=\Piu[j=1][s]{V_j}$ be objects of $\sCatT C$ (the $U_i$'s and $V_j$'s are words of objects of $\Cat C$). Then $P \per Q$ is given as in (<ref>) and it is immediate to see that $A \per (P \piu Q) = (A \per P) \piu (A \per Q)$ when $A \in Ob(\Cat C)$. We need to show that $\id{A \per (P \piu Q)} = \dl{A}{P}{Q}$ in $\sCatT C$.

In $\sCatT C$, the left distributor $\dl S P Q \colon S \per (P \piu Q) \to (S \per P) \piu (S \per Q)$ is defined as

\[
\begin{tikzcd}
S \per (P \piu Q) \ar[r,"\dl S P Q"] \ar[d,"\symmt{S}{P \piu Q}"'] & (S \per P) \piu (S \per Q) \\
(P \piu Q) \per S \ar[r,"\id{}"] & (P \per S) \piu (Q \per S) \ar[u,"{\symmt{P}{S} \piu \symmt{Q}{S}}"']
\end{tikzcd} \qquad \text{(in $\sCatT C$)}
\]

where the symmetry $\symmt{R}{T} \colon R \per T \to T \per R$ in $\sCatT C$ is defined as the following composite in $\Cat C$:

\[
\begin{tikzcd}
\pi(R \per T) \ar[r,"{\symmt{R}{T}}"] \ar[d,"{\cong_{Lap}}^{-1}"'] & \pi(T \per R) \\
\pi(R) \per \pi(T) \ar[r,"{\symmt{\pi(R)}{\pi(T)}}"] & \pi(T) \per \pi(R) \ar[u,"\cong_{Lap}"']
\end{tikzcd}
\]

The arrow $\cong_{Lap}$ is the isomorphism built up using the structure of rig category whose existence and uniqueness is guaranteed by the coherence theorem for rig categories <cit.>.

In order to prove that $\id{A \per (P \piu Q)} = \dl{A}{P}{Q}$ in $\sCatT C$, we will use the coherence theorem for rig categories as formulated in <cit.>. Suppose that $U_i=B^i_1\dots B^i_{n_i}$ and $V_j = C^j_1\dots C^j_{m_j}$. Now, we have that $\pi(A \per (P \piu Q))$ is the right bracketing of the following object of $\Cat C$:

\[
\Piu[i=1][r]{\Per[k=1][n_i]{(A \per B^i_k)}} \piu \Piu[j=1][m]{\Per[k=1][m_j]{(A \per C^j_k)}}
\]

This object, as a term of the free $\{\piu,\per\}$-algebra generated by the set

\[
X = \{A,B^1_1,\dots,B^1_{n_1},\dots,B^r_1,\dots,B^r_{n_r}, C^1_1,\dots,C^1_{m_1},\dots,C^s_1,\dots,C^s_{n_s},\zero^X,\uno^X\},
\]
is regular in the sense of <cit.>. Indeed, for every $i$ the factors $A, B^i_1,\dots,B^i_{n_i}$ are all distinct elements of $X$, and similarly for every $j$ the factors $A, C^j_1,\dots,C^j_{m_j}$ are all distinct elements of $X$; moreover, all the $r + s$ addends $\Per[k=1][n_i]{(A \per B^i_k)}$ and $\Per[k=1][m_j]{(A \per C^j_k)}$ are all pairwise distinct elements of the free $\{\piu,\per\}$-algebra on $X$. Hence, by the coherence theorem for rig categories, as stated in Theorem 3.9.1 of <cit.>, there exists a unique isomorphism, built up using instances of the natural isomorphisms given by the structure of rig category and involving only the objects in $X$, from $\pi(A \per (P \piu Q))$ to itself. Since $\id{A \per (P \piu Q)}$ and $\dl{A}{P}{Q}$ are two such structural isomorphisms, they must coincide.

Simply postcompose $F$ with the two functors $\sCatT D \to \Cat D \to \sCatT D$ that make the equivalence $\Cat D \simeq \sCatT D$.

Let $\sign$ be a rig signature and let $\gen$ be a generator in $\sign$, say
\[\gen \colon \Piu[i=1][n_\gen]{U_i} \to \Piu[j=1][m_\gen]{V_j}\]

where $U_i$, $V_j$ are monomials for $i=1 \dots n_\gen$ and $j=1 \dots m_\gen$. For each $(i,j)$, we define a new generator

\[
\gen_{j,i} \colon U_i \to V_j
\]

having as arity the monomial $U_i$ and as coarity the monomial $V_j$. These $\gen_{j,i}$'s are now formal symbols that we use to define a signature $\sign_M$, obtained from $\sign$ by replacing each $\gen \in \sign$ with all the $\gen_{j,i}$'s:

\[
\sign_M \defeq \{ \gen_{j,i} \mid \gen\in \sign,\, j = 1\dots m_\gen,\, i=1\dots n_\gen \}\text{.}
\]

Observe that $\sign_M$ is a monoidal signature since it only contains symbols having as arity and coarity some monomials.

For example, assume that $\sign$ consists of a single generator $\gen \colon AB \piu C \to A \piu B \piu C$ depicted as follows:

\[\tikzfig{tapes/examples/rigGen}\]

Then $\sign_M$ is the signature consisting of the following six generators:

\[ \monGenDue{\gen_{1,1}}{A}{B}{A} \quad \monGenDue{\gen_{2,1}}{A}{B}{B} \quad  \monGenDue{\gen_{3,1}}{A}{B}{C}\]

\[ \monGen{\gen_{1,2}}{C}{A} \quad \monGen{\gen_{2,2}}{C}{B} \quad \monGen{\gen_{3,2}}{C}{C}\]

Now, call $\fssbRig$ and $\fssbRigM$ the free sesquistrict fb rig categories generated, respectively, by $\sign$ and $\sign_M$. We show that there is an isomorphism of rig categories

\[\begin{tikzcd} \fssbRig \ar[r,bend left,"F"above]  &\fssbRigM \ar[l,bend left,"G"below]
\end{tikzcd}\]

The functor $F$ is the unique strict fb-rig functor mapping every $\gen \in \sign$ with arity $\Piu[i][n]{U_i} $ and coarity $\Piu[j][m]{V_j}$ into

\[\begin{tikzcd}[ampersand replacement=\&,column sep=3em]
\PiuL[i=1][n]{U_i} \ar[r,"{\PiuL[i=1][n]{\diagg{U_i} m}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{U_i}} \ar[r,"{\PiuL[i=1][n]{\PiuL[j=1][m]{\gen_{ji}}}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{V_j}} \ar[r,"\codiagg{\Piu[j=1][m]{V_j}}{n}"] \& \PiuL[j=1][m]{V_j}
\end{tikzcd}
\]

Similarly, the functor $G$ is the unique strict fb-rig functor mapping every $\gen_{ji} \in \sign_M$ into

\[
\begin{tikzcd}[ampersand replacement=\&,column sep=3em]
{U_i} \ar[r,"\inj{i}"] \& \PiuL[i=1][n]{U_i} \ar[r,"s"] \& \PiuL[j=1][m]{V_j} \ar[r,"\proj{j}"] \& {V_j}
\end{tikzcd}
\]

To prove that $GF=Id_{\fssbRig}$, it is enough to check that $GF(\gen)=\gen$. Since $G$ preserves the finite biproduct rig structure, it holds that $GF(\gen)$ is

\[\begin{tikzcd}[ampersand replacement=\&,column sep=4em]
\PiuL[i=1][n]{U_i} \ar[r,"{\PiuL[i=1][n]{\diagg{U_i} m}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{U_i}} \ar[r,"{\PiuL[i=1][n]{\PiuL[j=1][m]{G(\gen_{ji})}}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{V_j}} \ar[r,"\codiagg{\Piu[j=1][m]{V_j}}{n}"] \& \PiuL[j=1][m]{V_j}
\end{tikzcd}
\]

which, by Proposition <ref>, is exactly $\gen$.

To prove that  $FG(\gen_{ji})=\gen_{ji}$, just observe that $FG(\gen_{ji})$ is the upper leg of the following diagram:

\[
\begin{tikzcd}[row sep={3em}]& & \PPiuL h n k m {U_h} \ar[r,"{\PPiuL h n k m {s_{kh}}}"] & \PPiuL h n k m {V_k} \ar[dr,"\codiagg{\Piu[k]{V_k}} n"]\\
& \PiuL[h=1][n]{U_h} \ar[ur,"{\PiuL[h=1][n]{\diagg{U_h} m}}"]  & \PiuL[k=1][m]{U_i} \ar[u,"\inj i"description] \ar[r,"{\PiuL[k=1][m]{s_{ki}}}"] \ar[d,"\proj j"description] & \PiuL[k=1][m]{V_k} \ar[r,"\id{}"] \ar[u,"\inj i"description] \ar[d,"\proj j"description] & \PiuL[k=1][m]{V_k} \ar[dr,"\proj j"]\\
U_i \ar[ur,"\inj i"] \ar[urr,"\diagg{U_i} m "description] \ar[rr,"\id{}"] & & U_i  \ar[r,"s_{ji}"] & V_j \ar[rr,"\id{}"] & & V_j
\end{tikzcd}
\]

which commutes because of the naturality of the injections and the projections for the biproduct $\piu$, as well as the universal property of $\codiagg{\Piu[k]{V_k}} n$ as the copairing of n copies of $\id{\Piu[k]{V_k}}$ (in the top-right triangle).

§ APPENDIX TO SECTION <REF>

In this Appendix we study, in detail, the properties of $\per_{\CatTape}$. It is divided in four subsections. In Section <ref> we state and prove several properties of the distributors and the symmetries (Lemma <ref> and <ref>). In Section <ref> we present some additional lemmas for monomial whiskerings (Lemma <ref> and <ref>), which are needed to prove, in Section <ref>, the 17 equations stated in Table <ref>: the algebra of whiskerings. Finally, in Section <ref> we prove the remaining results that were claimed in Section <ref>, namely Theorems <ref>, <ref>, <ref> and Corollary <ref>.

§.§ Properties of distributors and symmetries in $\CatTape$

The following lemma provides a sanity check for our inductive definitions.

For all $P,P',Q,R$, monomials $U,V$ the followings hold:

* $\dl{U}{Q}{R} = \id{U(Q\piu R)}$

* $\dl{P \piu P'}{Q}{R} = (\dl{P}{Q}{R} \piu \dl{P'}{Q}{R});(\id{PQ} \piu \symmp{PR}{P'Q} \piu \id{P'R})$

* $\dl{P}{\zero}{R} = \id{PR}$

* $\dl{P}{Q}{\zero} = \id{PQ}$

* $\symmt{P}{Q} ; \symmt{Q}{P} = \id{P  Q}$

* $\symmt{P}{Q \piu R} = \dl{P}{Q}{R} ; (\symmt{P}{Q} \piu \symmt{P}{R})$

* $\symmt{P}{\uno} = \id{P}$

* $\symmt{P}{V} = \Piu[i]{\tapesymm{U_i}{V}}$ for $P = \Piu[i]{U_i}$. In particular $\symmt{U}{V}=\tape{\symm{U}{V}}$.

It holds by definition of $\delta^l$.

We prove that $\dl{P \piu P'}{Q}{R} = (\dl{P}{Q}{R} \piu \dl{P'}{Q}{R});(\id{PQ} \piu \symmp{PR}{P'Q} \piu \id{P'R})$ by induction on $P$.

Case $P = \zero$: it holds by definition of $\delta^l$.

Case $P = U \piu P''$:

\begin{align*}
\dl{U \piu P'' \piu P'}{Q}{R} &= \dl{U \piu (P'' \piu P')}{Q}{R} \\
&=\tag{Def. $\delta^l$} (\id{U(Q \piu R)} \piu \dl{P'' \piu P'}{Q}{R});(\id{UQ} \piu \symmp{UR}{P''Q \piu P'Q} \piu \id{P''R \piu P'R})\\
&=\tag{Rem.~\ref{rem:per tape is right distributive}} \tikzfig{lemmaDlG/step1} \\
&=\tag{Ind. hp.} \tikzfig{lemmaDlG/step2}\\
&=\tag{Funct. $\piu$} \tikzfig{lemmaDlG/step4}\\
(((\id{U(Q\piu R)} \piu \dl{P''}{Q}{R});(\id{UQ} \piu \symmp{UR}{P''Q} \piu \id{P''R})) \piu \dl{P'}{Q}{R}); \\ (\id{UQ \piu P''Q} \piu \symmp{UR \piu P''R}{P'Q} \piu \id{P'R})
\end{multlined} \\
&=\tag{Def. $\delta^l$}(\dl{U \piu P''}{Q}{R} \piu \dl{P'}{Q}{R});(\id{UQ \piu P''Q} \piu \symmp{UR \piu P''R}{P'Q} \piu \id{P'R})
\end{align*}

We prove that $\dl{P}{\zero}{R} = \id{PR}$ by induction on $P$.

Case $P = \zero$: it holds by definition of $\delta^l$.

Case $P = U \piu P'$:

\begin{align*}
\dl{U \piu P'}{\zero}{R} &=\tag{Def. $\delta^l$} (\id{U(\zero \piu R)} \piu \dl{P'}{\zero}{R});(\id{U\zero} \piu \symmp{UR}{P'\zero} \piu \id{P'R}) \\
&=\tag{Ind. hp.} (\id{UR} \piu \id{P'R});(\id{\zero} \piu \symmp{UR}{\zero} \piu \id{P'R}) \\
&=\tag{\ref{eq:symmax2}} (\id{UR} \piu \id{P'R});(\id{UR} \piu \id{P'R}) \\
&=\tag{Funct. $\piu$} \id{UR \piu P'R} \\
&=\tag{Rem.~\ref{rem:per tape is right distributive}} \id{(U \piu P')R} \\
\end{align*}

Analogous to the proof of Lemma <ref>.<ref> above.

We want to prove that $\symmt{P}{Q} ; \symmt{Q}{P} = \id{P  Q}$.
First we prove the following three equations:

\begin{align*}
\symmt{\zero}{Q} &= \id{\zero} \tag{$\ast_1$} \\
\symmt{U \piu P'}{V} &= (\symmt{U}{V} \piu \symmt{P'}{V}) ; \Idl{V}{U}{P'} \tag{$\ast_{2.1}$} \\
\symmt{U \piu P'}{Q} &= (\Piu[j]{\tapesymm{U}{V_j}} \piu \symmt{P'}{Q}) ; \Idl{Q}{U}{P'} \text{ with $Q = \Piu[j]{V_j}$} \tag{$\ast_2$}
\end{align*}

For $(\ast_1)$ we proceed by induction on $Q$:

Case $Q = \zero$: it holds by definition of $\symmt$.

Case $Q = V \piu Q'$:

\begin{align*}
\symmt{\zero}{V \piu Q'} &=\tag{Def. $\symmt$} \dl{\zero}{V}{Q'} ; (\Piu[i=1][0]{\tapesymm{U_i}{V}} \piu \symmt{\zero}{Q'}) \\
&=\tag{Def. $\delta^l$, ind. hp.} \id\zero
\end{align*}

For $(\ast_{2.1})$, suppose that $P' = \Piu[i']{U_{i'}'}$ and observe that the following holds:

\begin{align*}
\symmt{U \piu P'}{V} &=\tag{Def. $\symmt$} \dl{U \piu P'}{V}{\zero} ; (\tapesymm{U}{V} \piu \Piu[i']{\tapesymm{U'_{i'}}{V}} \piu \symmt{U}{\zero}) \\
&=\tag{Def. $\symmt$} \dl{U \piu P'}{V}{\zero} ; (\symmt{U}{V} \piu \symmt{P'}{V}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl zero}} (\symmt{U}{V} \piu \symmt{P'}{V}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}} (\symmt{U}{V} \piu \symmt{P'}{V}) ; \Idl{V}{U}{P'}
\end{align*}

For $(\ast_2)$ we proceed by induction on $Q:$

Case $Q = \zero$:

\begin{align*}
\symmt{U \piu P'}{\zero} &=\tag{Def. $\symmt$} \id\zero \\
&=\tag{Def. $\delta^l$} (\Piu[i=1][0]{\tapesymm{U_i}{V}} \piu \symmt{\zero}{Q'}) ; \dl{\zero}{V}{Q'}\\
\end{align*}

Case $Q = V \piu Q'$:

\begin{align*}
\symmt{U \piu P'}{V \piu Q'} &=\tag{Def. $\symmt$} \dl{U \piu P'}{V}{Q'} ; (\tapesymm{U}{V} \piu \Piu[i']{\tapesymm{U'_{i'}}{V}} \piu \symmt{U \piu P'}{Q'}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V}} \dl{U \piu P'}{V}{Q'} ; (\symmt{U \piu P'}{V} \piu \symmt{U \piu P'}{Q'}) \\
&=\tag{$\ast_{2.1}$, ind. hp.} \dl{U \piu P'}{V}{Q'} ; (((\symmt{U}{V} \piu \symmt{P'}{V}) ; \Idl{V}{U}{P'}) \piu ((\symmt{U}{Q'} \piu \symmt{P'}{Q'}) ; \Idl{Q'}{U}{P'})) \\
&=\tag{Def.\ $\delta^l$}\begin{multlined}[t]
(\dl{U}{V}{Q'} \piu \dl{P'}{V}{Q'}) ; (\id{UV} \piu \symmp{UQ'}{P'V} \piu \id{P'Q'}) ; \\
(((\symmt{U}{V} \piu \symmt{P'}{V}) ; \Idl{V}{U}{P'}) \piu ((\symmt{U}{Q'} \piu \symmt{P'}{Q'}) ; \Idl{Q}{U}{P'}))
\end{multlined} \\
&=\tag{Funct.\ $\piu$}\begin{multlined}[t]
(\dl{U}{V}{Q'} \piu \dl{P'}{V}{Q'}) ; (\id{UV} \piu \symmp{UQ'}{P'V} \piu \id{P'Q'}) ; \\
(\symmt{U}{V} \piu \symmt{P'}{V} \piu \symmt{U}{Q'} \piu \symmt{P'}{Q'}) ; (\Idl{V}{U}{P'} \piu \Idl{Q'}{U}{P'})
\end{multlined} \\
(\dl{U}{V}{Q'} \piu \dl{P'}{V}{Q'}) ; (\symmt{U}{V} \piu \symmt{U}{Q'} \piu \symmt{P'}{V} \piu \symmt{P'}{Q'}) ; \\
(\id{VU} \piu \symmp{Q'U}{VP'} \piu \id{Q'P}) ; (\Idl{V}{U}{P'} \piu \Idl{Q'}{U}{P'})
\end{multlined} \\
&=\tag{Def.\ $\delta^l$} (\dl{U}{V}{Q'} \piu \dl{P'}{V}{Q'}) ; (\symmt{U}{V} \piu \symmt{U}{Q'} \piu \symmt{P'}{V} \piu \symmt{P'}{Q'}) ; \Idl{V \piu Q'}{U}{P'} \\
&=\tag{Funct. $\piu$} (\dl{U}{V}{Q'} ; (\symmt{U}{V} \piu \symmt{U}{Q'})) \piu (\dl{P'}{V}{Q'} ; (\symmt{P'}{V} \piu \symmt{P'}{Q'})) ; \Idl{V \piu Q'}{U}{P'} \\
&=\tag{Def.\ $\symmt$, Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V} } (\symmt{U}{V \piu Q'} \piu \symmt{P'}{V \piu Q'}) ; \Idl{V \piu Q'}{U}{P'}
\end{align*}

The rest of the proof is by induction on $Q$:

Case $Q = \zero$
\begin{align*}
\symmt{P}{\zero} ; \symmt{\zero}{P} &=\tag{Def. $\symmt$} \id\zero ; \symmt{\zero}{P} \\
&=\tag{$\ast_1$} \id\zero ; \id\zero \\
&= \id\zero \\
\end{align*}

Case $Q = V \piu Q'$
\begin{align*}
\symmt{P}{V \piu Q'} ; \symmt{V \piu Q'}{P} &=\tag{Def. $\symmt$, $\ast_2$} \dl{P}{V}{Q'} ; (\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q'}) ; (\Piu[i]{\tapesymm{V}{U_i}} \piu \symmt{Q'}{P}) ; \Idl{P}{V}{Q'} \\
&=\tag{Funct. $\piu$} \dl{P}{V}{Q'} ; ((\Piu[i]{\tapesymm{U_i}{V}} ; \Piu[i]{\tapesymm{V}{U_i}}) \piu (\symmt{P}{Q'} ; \symmt{Q'}{P})) ; \Idl{P}{V}{Q'} \\
&=\tag{\ref{eq:symmax1}, ind. hp.} \dl{P}{V}{Q'} ; (\id{PV} \piu \id{PQ'}) ; \Idl{P}{V}{Q'} \\
&=\tag{Iso} \id{P(V \piu Q')}
\end{align*}

It holds by definition of $\symmt$.

The following holds for all monomials $V$ and polynomials $P,Q,R$:

\[ \dl{P}{V \piu Q}{R} ; (\dl{P}{V}{Q} \piu \id{PR}) = \dl{P}{V}{Q \piu R} ; (\id{PV} \piu \dl{P}{Q}{R}) \]

By induction on $P$.

Case $P = \zero$: it holds since both sides of the equation are $\id\zero$ by definition of $\delta^l$.

Case $P = U \piu P'$: For the inductive case we will mix the classical syntax with tape diagrams to ease the reading.

\begin{align*}
&\dl{U \piu P'}{V \piu Q}{R} ; (\dl{U \piu P'}{V}{Q} \piu \id{UR \piu P'R}) \\
&=\tag{Def. $\delta^l$} \begin{multlined}[t]
(\id{U((V \piu Q) \piu R)} \piu \dl{P'}{V \piu Q}{R}) ; (\id{UV \piu UQ} \piu \symmp{UR}{P'(V \piu Q)} \piu \id{P'R}) ; \\
(\dl{U \piu P'}{V}{Q} \piu \id{UR \piu P'R})
\end{multlined}\\
&=\tag{Def. $\delta^l$} \begin{multlined}[t]
(\id{U((V \piu Q) \piu R)} \piu \dl{P'}{V \piu Q}{R}) ; (\id{UV \piu UQ} \piu \symmp{UR}{P'(V \piu Q)} \piu \id{P'R}) ; \\
(((\id{U(V \piu Q)} \piu \dl{P'}{V}{Q});(\id{UV} \piu \symmp{UQ}{P'V} \piu \id{P'Q})) \piu \id{UR \piu P'R})
\end{multlined}\\
&= \tikzfig{lemmaDl/step1} \\
&=\tag{\ref{ax:symmpnat}} \tikzfig{lemmaDl/step2} \\
&=\tag{Ind. hp.} \tikzfig{lemmaDl/step3} \\
&= \tag{Funct. $\piu$}  \tikzfig{lemmaDl/step5} \\
&= \begin{multlined}[t]
(\id{U(V\piu (Q \piu R))} \piu \dl{P'}{V}{Q \piu R}) ; (\id{UV} \piu \symmp{U(Q \piu R)}{P'V} \piu \id{P'(Q \piu R)}) ; \\
(\id{UV \piu P'V} \piu ((\id{U(Q \piu R)} \piu \dl{P'}{Q}{R});(\id{UQ} \piu \symmp{UR}{P'Q} \piu \id{P'R})))
\end{multlined}\\
&=\tag{Def. $\delta^l$} \dl{U \piu P'}{V}{Q \piu R} ; (\id{UV \piu P'V} \piu \dl{U \piu P'}{Q}{R}) \\
\end{align*}

We want to prove that $\symmt{P}{Q \piu R} = \dl{P}{Q}{R} ; (\symmt{P}{Q} \piu \symmt{P}{R})$ by induction on $Q$.

Case $Q=\zero$: By Lemma <ref>.<ref>, $\dl {P}{\zero}{R}=\id R$ and by definition of $\symmt$, $\symmt{P}{\zero}=\id{\zero}$. The right-hand side reduces therefore to $\symmp{P}{R}$, as desired.

Case $Q=V \piu Q'$:

\begin{align*}
\symmt{P}{V \piu Q' \piu R} &=\tag{Def. $\symmt$} \dl{P}{V}{Q' \piu R} ; (\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q' \piu R}) \\
&=\tag{Ind. hp.} \dl{P}{V}{Q' \piu R} ; (\Piu[i]{\tapesymm{U_i}{V}} \piu (\dl{P}{Q'}{R};(\symmt{P}{Q'} \piu \symmt{P}{R}))) \\
&=\tag{Funct. $\piu$} \dl{P}{V}{Q' \piu R} ; (\id{PV} \piu \dl{P}{Q'}{R}) ; (\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q'} \piu \symmt{P}{R}) \\
&=\tag{Lemma~\ref{lm:tape:dl aux}} \dl{P}{V \piu Q'}{R} ; (\dl{P}{V}{Q'} \piu \id{PR}) ; (\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q'} \piu \symmt{P}{R}) \\
&=\tag{Funct. $\piu$} \dl{P}{V \piu Q'}{R} ; ((\dl{P}{V}{Q'};(\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q'})) \piu \symmt{P}{R}) \\
&=\tag{Def. $\symmt$} \dl{P}{V \piu Q'}{R} ; (\symmt{P}{V \piu Q'} \piu \symmt{P}{R})
\end{align*}

We want to prove that $\symmt{P}{\uno} = \id{P}$ by induction on $P$.

Case $P = \zero$: it holds by definition of $\symmt$.

Case $P = U \piu P'$:

\begin{align*}
\symmt{U \piu P'}{\uno} &=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmtInv}} \Isymmt{\uno}{U \piu P'} \\
&=\tag{Def. $\symmt$} (\tapesymm{U}{\uno} \piu \symmt{P'}{\uno}) ; \Idl{\uno}{U}{P'} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}} (\tapesymm{U}{\uno} \piu \symmt{P'}{\uno}) ; \id{UP'} \\
&=\tag{\ref{eq:symmax2}, ind. hp.} \id{U} \piu \id{P'} \\
&= \id{U \piu P'}
\end{align*}

§.§ Additional lemmas for monomial whiskerings

Let $\t \colon \Piu[i]{U_i} \to \Piu[j]{V_j}$ be a tape diagram, then the following holds

\[ \RW{W} \t = \Piu[i]{\tapesymm{U_i}{W}} ; \LW{W} \t ; \Piu[j]{\tapesymm{W}{V_j}} \]

By induction on $\t$.

Case $\t = \id\zero$: Notice that $\PiuL[i=1][0]{\tapesymm{U_i}{W}} = \PiuL[j=1][0]{\tapesymm{W}{V_j}} = \id\zero$ and thus $\RW W {\id\zero} = \id\zero = \LW W {\id\zero}$.

Case $\t = \tape{c}$: Suppose $c \colon U \to V$, then

\begin{align*}
\RW W {\tape{c}} &=\tag{Def. $R$} \tape{c \per \id W} \\
&=\tag{\ref{eq:symmax1}} \tape{c \per \id W} ; \tapesymm{V}{W} ; \tapesymm{W}{V} \\
&=\tag{Nat. $\tape{\sigma}$} \tapesymm{U}{W} ; \tape{\id W \per c} ; \tapesymm{W}{V} \\
&=\tag{Def. $L$} \tapesymm{U}{W} ; \LW W {\tape{c}} ; \tapesymm{W}{V}
\end{align*}

Case $\t = \symmp{U}{V}$:

\begin{align*}
\RW W {\symmp{U}{V}} &=\tag{Def. $R$} \symmp{UW}{VW} \\
&=\tag{\ref{eq:symmax1}} \symmp{UW}{VW} ; ((\tapesymm{V}{W} ; \tapesymm{W}{V}) \piu (\tapesymm{U}{W} ; \tapesymm{W}{U})) \\
&=\tag{\ref{ax:symmpnat}} (\tapesymm{U}{W} \piu \tapesymm{V}{W}) ; \symmp{WU}{WV} ; (\tapesymm{W}{V} \piu \tapesymm{W}{U}) \\
&=\tag{Def. $L$} (\tapesymm{U}{W} \piu \tapesymm{V}{W}) ; \LW W {\symmp{U}{V}} ; (\tapesymm{W}{V} \piu \tapesymm{W}{U})
\end{align*}

Case $\t = \diag U$: (similarly for $\codiag{U}$)

\begin{align*}
\RW W {\diag U} &=\tag{Def. $R$} \diag{UW} \\
&=\tag{\ref{eq:symmax1}} \diag{UW} ; ((\tapesymm{U}{W} ; \tapesymm{W}{U})  \piu (\tapesymm{U}{W} ; \tapesymm{W}{U}))\\
&=\tag{\ref{ax:diagnat}} \tapesymm{U}{W} ; \diag{WU} ; (\tapesymm{W}{U} \piu \tapesymm{W}{U}) \\
&=\tag{Def. $L$} \tapesymm{U}{W} ; \LW W {\diag{U}} ; (\tapesymm{W}{U} \piu \tapesymm{W}{U})
\end{align*}

Case $\t = \bang U$: (similarly for $\cobang{U}$)

\begin{align*}
\RW W {\bang U} &=\tag{Def. $R$} \bang{UW} \\
&=\tag{\ref{eq:symmax1}} \tapesymm{U}{W} ; \tapesymm{W}{U} ; \bang{UW} \\
&=\tag{\ref{ax:bangnat}} \tapesymm{U}{W} ; \bang{WU} \\
&=\tag{Def. $L$} \tapesymm{U}{W} ; \LW W {\bang{U}}
\end{align*}

Case $\t = \t_1 ; \t_2$: Suppose $\t_1 \colon \Piu[i]{U_i} \to \Piu[l]{Z_l}, \t_2 \colon \Piu[l]{Z_l} \to \Piu[j]{V_j}$, then

\begin{align*}
\RW W {\t_1 ; \t_2} &=\tag{Def. $R$} \RW W {\t_1} ; \RW W {\t_2} \\
&=\tag{Ind. hp.} \Piu[i]{\tapesymm{U_i}{W}} ; \LW{W} {\t_1} ; \Piu[l]{\tapesymm{W}{Z_l}} ; \Piu[l]{\tapesymm{Z_l}{W}} ; \LW{W} {\t_2} ; \Piu[j]{\tapesymm{W}{V_j}} \\
&=\tag{\ref{eq:symmax1}} \Piu[i]{\tapesymm{U_i}{W}} ; \LW{W} {\t_1} ; \LW{W} {\t_2} ; \Piu[j]{\tapesymm{W}{V_j}} \\
&=\tag{Def. $L$} \Piu[i]{\tapesymm{U_i}{W}} ; \LW{W} {\t_1 ; \t_2} ; \Piu[j]{\tapesymm{W}{V_j}}
\end{align*}

Case $\t = \t_1 \piu \t_2$: Suppose $\t_1 \colon \Piu[i]{U_i} \to \Piu[j]{V_j}, \t_2 \colon \Piu[i']{U'_{i'}} \to \Piu[j']{V'_{j'}}$, then

\begin{align*}
\RW W {\t_1 \piu \t_2} &=\tag{Def. $R$} \RW W {\t_1} \piu \RW W {\t_2} \\
&=\tag{Ind. hp.} (\Piu[i]{\tapesymm{U_i}{W}} ; \LW{W} {\t_1} ; \Piu[j]{\tapesymm{W}{V_j}}) \piu (\Piu[i']{\tapesymm{U'_{i'}}{W}} ; \LW{W} {\t_2} ; \Piu[j']{\tapesymm{W}{V'_{j'}}}) \\
&=\tag{Funct. $\piu$} (\Piu[i]{\tapesymm{U_i}{W}} \piu \Piu[i']{\tapesymm{U'_{i'}}{W}}) ; (\LW{W} {\t_1} \piu \LW{W}{\t_2} ; (\Piu[j]{\tapesymm{W}{V_{j}}} \piu \Piu[j']{\tapesymm{W}{V'_{j'}}}) \\
&=\tag{Def. $L$} (\Piu[i]{\tapesymm{U_i}{W}} \piu \Piu[i']{\tapesymm{U'_{i'}}{W}}) ; (\LW{W} {\t_1 \piu \t_2}) ; (\Piu[j]{\tapesymm{W}{V_{j}}} \piu \Piu[j']{\tapesymm{W}{V'_{j'}}})
\end{align*}

For all $\tape{c} \colon U \to V, \t \colon P \to Q$, $\LW{U}{\t} ; \RW{Q}{\tape{c}} = \RW{P}{\tape{c}} ; \LW{V}{\t}$.

We fix $P=\Piu[k]{W_k} $ and $Q= \Piu[l]{Z_l}$. By definition of $\RW{P}{-}$ and $\delta^l$, it is immediate that  $\RW{Q}{\tape{c}}= \Piu[l]{\tape{c \per \id{Z_l}}}$ and $ \RW{P}{\tape{c}} = \Piu[k]{\tape{c \per \id{W_k}}}$.

We proceed by induction on $\t$.

Case $\t = \id{\zero}$: $\LW U {\id{\zero}} ; \Piu[l=1][0]{\tape{c \per \id{Z_l}}} = \id{\zero} = (\Piu[k=1][0]{\tape{c \per \id{W_k}}}) ; \LW V {\id{\zero}}$

Case $\t = \tape{d}$: Suppose $d \colon W \to Z$, then

\begin{align*}
\LW U {\tape{d}} ; \tape{c \per \id Z} &=\tag{Def. $L$} \tape{\id U \per d} ; \tape{c \per \id Z} \\
&=\tag{Funct. $\tape{\per}$} \tape{c \per d} \\
&=\tag{Funct. $\tape{\per}$} \tape{c \per \id W} ; \tape{\id V \per d} \\
&=\tag{Def. $L$} \tape{c \per \id W} ; \LW V {\tape{d}}
\end{align*}

Case $\t = \symmp{W}{Z}$:

\begin{align*}
\LW U {\symmp{W}{Z}} ; (\tape{c \per \id Z} \piu \tape{c \per \id W}) &=\tag{Def. $L$} \symmp{UW}{UZ} ; (\tape{c \per \id Z} \piu \tape{c \per \id W}) \\
&=\tag{\ref{ax:symmpnat}} (\tape{c \per \id W} \piu \tape{c \per \id Z}) ; \symmp{VW}{VZ} \\
&=\tag{Def. $L$} (\tape{c \per \id W} \piu \tape{c \per \id Z}) ; \LW V {\symmp{W}{Z}}
\end{align*}

Case $\t = \diag{W}$: (similarly for $\codiag{W}$)

\begin{align*}
\LW U {\diag{W}} ; (\tape{c \per \id W} \piu \tape{c \per \id W}) &=\tag{Def. $L$} \diag{UW} ; (\tape{c \per \id W} \piu \tape{c \per \id W}) \\
&=\tag{\ref{ax:diagnat}} \tape{c \per \id W} ; \diag{VW} \\
&=\tag{Def. $L$} \tape{c \per \id W} ; \LW V {\diag{W}}
\end{align*}

Case $\t = \bang{W}$: (similarly for $\cobang{W}$)

\begin{align*}
\LW U {\bang{W}} ; \Piu[l=1][0]{\tape{c \per \id{Z_l}}} &=\tag{Def. $L$} \bang{UW} \\ &=\tag{\ref{ax:bangnat}} \tape{c \per \id W} ; \bang{VW} \\
&=\tag{Def. $L$} \tape{c \per \id W} ; \LW V {\bang{W}}
\end{align*}

Case $\t = \t_1 ; \t_2$: Suppose $\t_1 \colon \Piu[k]{W_k} \to \Piu[j]{V_j}, \t_2 \colon \Piu[j]{V_j} \to \Piu[l]{Z_l}$, then

\begin{align*}
\LW U {\t_1 ; \t_2} ; \Piu[l]{\tape{c \per \id{Z_l}}} &=\tag{Def. $L$} \LW U {\t_1} ; \LW U {\t_2} ; \Piu[l]{\tape{c \per \id{Z_l}}} \\
&=\tag{Ind. hp.} \LW U {\t_1} ; \Piu[j]{\tape{c \per \id{V_j}}} ; \LW V {\t_2}\\
&=\tag{Ind. hp.} \Piu[k]{\tape{c \per \id{W_k}}} ; \LW V {\t_1} ; \LW V {\t_2}\\
&=\tag{Def. $L$} \Piu[k]{\tape{c \per \id{W_k}}} ; \LW V {\t_1 ; \t_2}
\end{align*}

Case $\t = \t_1 \piu \t_2$: Suppose $\t_1 \colon \Piu[k]{W_k} \to \Piu[l]{Z_l}, \t_2 \colon \Piu[k']{W'_{k'}} \to \Piu[l']{Z'_{l'}}$, then

\begin{align*}
&\LW U {\t_1 \piu \t_2} ; (\Piu[l]{\tape{c \per \id{Z_l}}} \piu \Piu[l']{\tape{c \per \id{Z'_{l'}}}}) \\
&=\tag{Def. $L$} (\LW U {\t_1} \piu \LW U {\t_2}) ; (\Piu[l]{\tape{c \per \id{Z_l}}} \piu \Piu[l']{\tape{c \per \id{Z'_{l'}}}}) \\
&=\tag{Funct. $\piu$} (\LW U {\t_1} ; \Piu[l]{\tape{c \per \id{Z_l}}}) \piu (\LW U {\t_2} ; \Piu[l']{\tape{c \per \id{Z'_{l'}}}}) \\
&=\tag{Ind. hp.} (\Piu[k]{\tape{c \per \id{W_k}}} ; \LW V {\t_1}) \piu (\Piu[k']{\tape{c \per \id{W'_{k'}}}} ; \LW V {\t_2}) \\
&=\tag{Funct. $\piu$} (\Piu[k]{\tape{c \per \id{W_k}}} \piu \Piu[k']{\tape{c \per \id{W'_{k'}}}}) ; (\LW V {\t_1} \piu \LW V {\t_2}) \\
&=\tag{Def. $L$} (\Piu[k]{\tape{c \per \id{W_k}}} \piu \Piu[k']{\tape{c \per \id{W'_{k'}}}}) ; \LW V {\t_1 \piu \t_2}
\end{align*}

§.§ Proof of Lemma <ref>: the algebra of whiskerings

The properties of the left whiskering are all trivial, thus we show only the proofs for their right counterpart.

Let $P = \Piu[i]{U_i}, Q = \Piu[j]{V_j}, S = \Piu[k]{W_k}, T = \Piu[l]{Z_l}$.

Equation (<ref>): $\RW S {\id{P}} = \id{PS}$. We prove it by induction on $S$.

Case $S=\zero$: it holds by Definition <ref>.

Case $S=W \piu S'$:

\begin{align*}
\RW {W \piu S'} {\id{Q}} &=\tag{Def. $R$} \dl{Q}{W}{S'} ; (\RW{W}{\id Q} \piu \RW{S'}{\id Q}) ; \Idl{Q}{W}{S'} \\
&=\tag{Def. $R$, ind. hp.} \dl{Q}{W}{S'} ; (\id {QW} \piu \id {QS'}) ; \Idl{Q}{W}{S'} \\
&=\tag{Iso} \id{Q(W \piu S')}
\end{align*}

Equation (<ref>): $\RW{S}{\t_1 ; \t_2} = \RW{S}{\t_1} ; \RW{S}{\t_2}$. Let $\t_1 \colon P \to Q, \t_2 \colon Q \to T$, we prove it by induction on $S$.

Case $S=\zero$: it holds by Definition <ref>.

Case $S=W \piu S'$:

\begin{align*}
&\RW{W \piu S'}{\t_1 ; \t_2} \\
&=\tag{Def. $R$} \dl{P}{W}{S'} ; (\RW{W}{\t_1 ; \t_2} \piu \RW{S'}{\t_1;\t_2}) ; \Idl{T}{W}{S'} \\
&=\tag{Def. $R$, ind. hp.} \dl{P}{W}{S'} ; ((\RW{W}{\t_1} ; \RW{W}{\t_2}) \piu (\RW{S'}{\t_1} ; \RW{S'}{\t_2})) ; \Idl{T}{W}{S'} \\
&=\tag{Funct. $\piu$} \dl{P}{W}{S'} ; ((\RW{W}{\t_1} \piu \RW{S'}{\t_1});(\RW{W}{\t_2} \piu \RW{S'}{\t_2})) ; \Idl{T}{W}{S'} \\
&=\tag{Iso} \dl{P}{W}{S'} ; ((\RW{W}{\t_1} \piu \RW{S'}{\t_1}) ; \Idl{Q}{W}{S'} ; \dl{Q}{W}{S'} ; (\RW{W}{\t_2} \piu \RW{S'}{\t_2})) ; \Idl{T}{W}{S'} \\
&=\tag{Def. $R$} \RW{W \piu S'}{\t_1} ; \RW{W \piu S'}{\t_2}
\end{align*}

Equation (<ref>): $\RW{\uno}{\t} = \t$. We prove it by induction on $\t$. All the base cases are trivial and the inductive cases follow by inductive hypothesis and functoriality of $R$ and $\piu$.

Equation (<ref>): $\RW{\zero}{\t} = \id{\zero}$. It holds by Definition <ref>.

Equation (<ref>): $\RW{S \piu T}{\t} = \dl{P}{S}{T} ; ( \RW{S}{\t} \piu \RW{T}{\t} ) ; \Idl{Q}{S}{T}$. Let $\t \colon P \to Q$, we prove it by induction on $S$.

Case $S=\zero$: it holds by Definition <ref>.

Case $S=W \piu S'$:

\begin{align*}
&\RW {W \piu S' \piu T} {\t} \\
&=\tag{Def. $R$} \dl{P}{W}{S' \piu T} ; (\RW{W}{\t} \piu \RW{S' \piu T}{\t}) ; \Idl{Q}{W}{S' \piu T} \\
&=\tag{Ind. hp.} \dl{P}{W}{S' \piu T} ; (\RW{W}{\t} \piu (\dl{P}{S'}{T} ; (\RW{S'}{\t} \piu \RW{T}{\t}) ; \Idl{Q}{S'}{T})) ; \Idl{Q}{W}{S' \piu T} \\
&=\tag{Funct. $\piu$} \dl{P}{W}{S' \piu T} ; (\id{PW} \piu \dl{P}{S'}{T}) ; (\RW{W}{\t} \piu ((\RW{S'}{\t} \piu \RW{T}{\t}) ; \Idl{Q}{S'}{T})) ; \Idl{Q}{W}{S' \piu T} \\
&=\tag{Lemma~\ref{lm:tape:dl aux}} \dl{P}{W \piu S'}{T} ; (\dl{P}{W}{S'} \piu \id{PT}) ; (\RW{W}{\t} \piu ((\RW{S'}{\t} \piu \RW{T}{\t}) ; \Idl{Q}{S'}{T})) ; \Idl{Q}{W}{S' \piu T} \\
&=\tag{Funct. $\piu$} \dl{P}{W \piu S'}{T} ; (\dl{P}{W}{S'} \piu \id{PT}) ; (\RW{W}{\t} \piu \RW{S'}{\t} \piu \RW{T}{\t}) ; (\id{QW} \piu \Idl{Q}{S'}{T}) ; \Idl{Q}{W}{S' \piu T} \\
&=\tag{Lemma~\ref{lm:tape:dl aux}} \dl{P}{W \piu S'}{T} ; (\dl{P}{W}{S'} \piu \id{PT}) ; (\RW{W}{\t} \piu \RW{S'}{\t} \piu \RW{T}{\t}) ; (\Idl{Q}{W}{S'} \piu \id{QT}) ; \Idl{Q}{W \piu S'}{T} \\
&=\tag{Funct. $\piu$} \dl{P}{W \piu S'}{T} ; ((\dl{P}{W}{S'} ; (\RW{W}{\t} \piu \RW{S'}{\t}) ; \Idl{Q}{W}{S'}) \piu \RW{T}{\t})  ; \Idl{Q}{W \piu S'}{T} \\
&=\tag{Def. $R$} \dl{P}{W \piu S'}{T} ; (\RW{W \piu S'}{\t} \piu \RW{T}{\t})  ; \Idl{Q}{W \piu S'}{T}
\end{align*}

Equation (<ref>): $\RW{S}{\t_1 \piu \t_2} = \RW{S}{\t_1} \piu \RW{S}{\t_2}$. Let $\t_1 \colon P \to Q, \t_2 \colon P' \to Q'$, we prove it by induction on $S$.

Case $S = \zero$: it holds by Definition <ref>.

Case $S = W \piu S'$:

\begin{align*}
&\RW {W \piu S'} {\t_1 \piu \t_2} \\
&=\tag{\ref{eq:whisk:sum}} \dl{P \piu P'}{W}{S'} ; (\RW W {\t_1 \piu \t_2} \piu \RW {S'} {\t_1 \piu \t_2}) ; \Idl{Q \piu Q'}{W}{S'} \\
&=\tag{Def. $R$, ind. hp.} \dl{P \piu P'}{W}{S'} ; (\RW W {\t_1} \piu \RW W {\t_2} \piu \RW {S'} {\t_1} \piu \RW {S'} {\t_2}) ; \Idl{Q \piu Q'}{W}{S'} \\
(\dl{P}{W}{S'} \piu \dl{P'}{W}{S'}) ; (\id{PW} \piu \symmp{PS'}{P'W} \piu \id{P'S'}) ; \\
(\RW W {\t_1} \piu \RW W {\t_2} \piu \RW {S'} {\t_1} \piu \RW {S'} {\t_2}) ; \\
(\id{QW} \piu \symmp{Q'W}{QS'} \piu \id{Q'S'}) ; (\Idl{Q}{W}{S'} \piu \Idl{Q'}{W}{S'})
\end{multlined} \\
&=\tag{\ref{ax:symmpnat}} (\dl{P}{W}{S'} \piu \dl{P'}{W}{S'}) ; (\RW W {\t_1} \piu \RW {S'} {\t_1} \piu \RW {W} {\t_2} \piu \RW {S'} {\t_2}) ; (\Idl{Q}{W}{S'} \piu \Idl{Q'}{W}{S'}) \\
&=\tag{Funct. $\piu$} (\dl{P}{W}{S'} ; (\RW W {\t_1} \piu \RW {S'} {\t_1}) ; \Idl{Q}{W}{S'})  \piu (\dl{P'}{W}{S'} ; (\RW {W} {\t_2} \piu \RW {S'} {\t_2}) ; \Idl{Q'}{W}{S'}) \\
&=\tag{$\ref{eq:whisk:sum}$} \RW {W \piu S'} {\t_1} \piu  \RW {W \piu S'} {\t_2}
\end{align*}

Equation (<ref>): $\RW S {\diag{U}} = \diag{US}$. We prove it by induction on $S$.

Case $S = \zero$: it holds by Definition <ref> and definition of $\diag{}$.

Case $S = W \piu S'$:

\begin{align*}
&\RW {W \piu S'} {\diag{U}} \\
&=\tag{\ref{eq:whisk:sum}} \dl{U}{W}{S'} ; (\RW W {\diag{U}} \piu \RW {S'} {\diag{U}}) ; \Idl{U\piu U}{W}{S'} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}, def. $\delta^l$} (\RW W {\diag{U}} \piu \RW {S'} {\diag{U}}) ; (\id{UW} \piu \symmp{UW}{US'} \piu \id{US'}) ; (\id{U(W\piu S')} \piu \Idl{U}{W}{S'}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}} (\RW W {\diag{U}} \piu \RW {S'} {\diag{U}}) ; (\id{UW} \piu \symmp{UW}{US'} \piu \id{US'}) \\
&=\tag{Def. $R$, ind. hp.} (\diag{UW} \piu \diag{US'}) ; (\id{UW} \piu \symmp{UW}{US'} \piu \id{US'}) \\
&=\tag{Def. $\diag{}$} \diag{UW \piu US'} \\
&=\tag{Rem.~\ref{rem:per tape is right distributive}} \diag{U(W \piu S')}
\end{align*}

The case for $\codiag{U}$ is completely analogous.

Equation (<ref>): $\RW S {\bang{U}} = \bang{US}$. We prove it by induction on $S$.

Case $S = \zero$: it holds by Definition <ref> and definition of $\bang{}$.

Case $S = W \piu S'$:
\begin{align*}
\RW {W \piu S'} {\bang{U}} &=\tag{\ref{eq:whisk:sum}} \dl{U}{W}{S'} ; (\RW W {\bang{U}} \piu \RW {S'} {\bang{U}}) ; \Idl{\zero}{W}{S'} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}, def. $\delta^l$} \RW W {\bang{U}} \piu \RW {S'} {\bang{U}} \\
&=\tag{Def. $R$, ind. hp.} \bang{UW} \piu \bang{US'} \\
&=\tag{Def. $\bang{}$} \bang{UW \piu US'} \\
&=\tag{Rem.~\ref{rem:per tape is right distributive}} \bang{U(W \piu S')}
\end{align*}
The case for $\cobang{U}$ is completely analogous.

Equation (<ref>): $\RW S {\symmp{P}{Q}} = \symmp{PS}{QS}$. We prove it by induction on $P$.

Case $P = \zero$:
\begin{align*}
\RW{S}{\symmp{\zero}{Q}} &=\tag{\ref{eq:symmax2}} \RW{S}{\id{Q}} \\
&=\tag{\ref{eq:whisk:id}} \id{QS} \\
&=\tag{\ref{eq:symmax2}} \symmp{\zero}{QS}
\end{align*}

Case $P = U \piu P'$:
\begin{align*}
\RW{S}{\symmp{U \piu P'}{Q}} &=\tag{\ref{eq:symmax3}} \RW{S}{(\id{U} \piu \symmp{P'}{Q}) ; (\symmp{U}{Q} \piu \id{P'})} \\
&=\tag{\ref{eq:whisk:funct}, \ref{eq:whisk:funct piu} } (\RW{S}{\id{U}} \piu \RW{S}{\symmp{P'}{Q}}) ; (\RW{S}{\symmp{U}{Q}} \piu \RW{S}{\id{P'}}) \\
&=\tag{\ref{eq:whisk:id}, ind. hp} (\id{US} \piu \symmp{P'S}{QS}) ; (\symmp{US}{QS} \piu \id{P'S}) \\
&=\tag{\ref{eq:symmax3}} \symmp{US \piu P'S}{QS} \\
&=\tag{Rem.~\ref{rem:per tape is right distributive}} \symmp{(U \piu P')S}{QS}
\end{align*}

Equation (<ref>): $\RW S {\dl{P}{Q}{R}} = \dl{P}{QS}{RS}$. We prove it by induction on $P$.

Case $P = \zero$: it follows from Definition <ref> and definition of $\delta^l$.

Case $P = U \piu P'$:

\begin{align*}
&\RW{S}{\dl{U\piu P'}{Q}{R}} \\
&=\tag{Def. $\delta^l$} \RW{S}{(\id{U(Q\piu R)} \piu \dl{P'}{Q}{R}) ; (\id{UQ} \piu \symmp{UR}{P'Q} \piu \id{P'R})}\\
&=\tag{\ref{eq:whisk:funct}, \ref{eq:whisk:funct piu}} (\RW{S}{\id{U(Q\piu R)}} \piu \RW{S}{\dl{P'}{Q}{R}}) ; (\RW{S}{\id{UQ}} \piu \RW{S}{\symmp{UR}{P'Q}} \piu \RW{S}{\id{P'R}}) \\
&=\tag{Ind. hp.} (\RW{S}{\id{U(Q\piu R)}} \piu \dl{P'}{QS}{RS}) ; (\RW{S}{\id{UQ}} \piu \RW{S}{\symmp{UR}{P'Q}} \piu \RW{S}{\id{P'R}})\\
&=\tag{\ref{eq:whisk:id}, \ref{eq:whisk:symmp}} (\id{U(Q\piu R)S} \piu \dl{P'}{QS}{RS}) ; (\id{UQS} \piu \symmp{URS}{P'QS} \piu \id{P'RS})\\
&=\tag{Def. $\delta^l$} \dl{U \piu P'}{QS}{RS}
\end{align*}

Equation (<ref>): $\symmt{PQ}{S} = \LW{P}{ \symmt{Q}{S}} ; \RW{Q}{\symmt{P}{S}}$. First we prove the following equations:

\begin{align*}
\LW{U}{\tapesymm{V}{W}};\RW{V}{\tapesymm{U}{W}} &= \tape{\sigma_{UV,W}} \tag{$\ast_1$} \\
\LW{U}{\Piu[j]{\tapesymm{V_j}{W}}} ; \RW{Q}{\tapesymm{U}{W}} &= \Piu[j]{\tapesymm{UV_j}{W}} \text{\qquad where $Q = \Piu[j]{V_j}$} \tag{$\ast_2$} \\
\LW{P}{\symmt{Q}{W}} ; \RW{Q}{\symmt{P}{W}} &= \symmt{PQ}{W} \tag{$\ast_3$}
\end{align*}

For $(\ast_1)$ observe that the following holds:

\begin{align*}
\LW{U}{\tapesymm{V}{W}};\RW{V}{\tapesymm{U}{W}} &=\tag{Def. $L, R$} \tape{\id U \per \sigma_{V,W}};\tape{\sigma_{U,W} \per \id{V}} \\
&=\tag{\ref{eq:symmax3}} \tape{\sigma_{UV,W}}
\end{align*}

For $(\ast_2)$ we proceed by induction on $Q$:

\begin{equation}
\LW{U}{\Piu[j]{\tapesymm{V_j}{W}}} ; \RW{Q}{\tapesymm{U}{W}} = \Piu[j]{\tapesymm{UV_j}{W}} \text{\qquad where $Q = \Piu[j]{V_j}$}
\end{equation}

Case $Q = \zero$: it follows from Definitions <ref> and <ref> and from the fact that $\PiuL[j=1][0]{\tapesymm{V_j}{W}} = \id\zero$.

Case $Q = V \piu Q'$: Let $Q' = \Piu[j']{V'_{j'}}$, then
\begin{align*}
&\LW{U}{\tapesymm{V}{W} \piu \Piu[j']{\tapesymm{V'_{j'}}{W}}};\RW{V \piu Q'}{\tapesymm{U}{W}} \\
&=\tag{Def. $L$, \ref{eq:whisk:sum}} (\LW{U}{\tapesymm{V}{W}} \piu \LW{U}{\Piu[j']{\tapesymm{V'_{j'}}{W}}}) ; \dl{UW}{V}{Q'} ; (\RW{V}{\tapesymm{U}{W}} \piu \RW{Q'}{\tapesymm{U}{W}}) ; \Idl{WU}{V}{Q'} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:dl U}} (\LW{U}{\tapesymm{V}{W}} \piu \LW{U}{\Piu[j']{\tapesymm{V'_{j'}}{W}}}) ; (\RW{V}{\tapesymm{U}{W}} \piu \RW{Q'}{\tapesymm{U}{W}}) \\
&=\tag{Funct. $\piu$} (\LW{U}{\tapesymm{V}{W}};\RW{V}{\tapesymm{U}{W}}) \piu (\LW{U}{\Piu[j']{\tapesymm{V'_{j'}}{W}}} ; \RW{Q'}{\tapesymm{U}{W}}) \\
&=\tag{$\ast_1$, ind. hp.} \tape{\sigma_{UV,W}} \piu \Piu[j']{\tapesymm{UV'_{j'}}{W}} \\
\end{align*}

For $(\ast_3)$ observe that the following holds:

\begin{align*}
&\LW{P}{\symmt{Q}{W}} ; \RW{Q}{\symmt{P}{W}} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V}} \LW{P}{\Piu[j]{\tapesymm{V_j}{W}}} ; \RW{Q}{\Piu[i]{\tapesymm{U_i}{W}}} \\
&=\tag{Def. $L$,\ref{eq:whisk:funct piu}} \Piu[i]{\LW{U_i}{\Piu[j]{\tapesymm{V_j}{W}}}} ; \Piu[i]{\RW{Q}{\tapesymm{U_i}{W}}} \\
&=\tag{Funct. $\piu$} \PiuPar[i]{\LW{U_i}{\Piu[j]{\tapesymm{V_j}{W}}} ; \RW{Q}{\tapesymm{U_i}{W}}} \\
&=\tag{$\ast_2$} \Piu[i]{\Piu[j]{\tapesymm{U_iV_j}{W}}} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V}} \symmt{PQ}{W} \\
\end{align*}

Now we are ready to prove Equation (<ref>) by induction on $S$:

Case $S=\zero$: it follows from Definitions <ref>, <ref> and definition of $\symmt$.

Case $S=W \piu S'$:

\begin{align*}
&\LW{P}{\symmt{Q}{W \piu S'}} ; \RW{Q}{\symmt{P}{W \piu S'}} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt dl}} \LW{P}{\dl{Q}{W}{S'} ; (\symmt{Q}{W} \piu \symmt{Q}{S'})} ; \RW{Q}{\dl{P}{W}{S'} ; (\symmt{P}{W} \piu \symmt{P}{S'})} \\
&=\tag{\ref{eq:whisk:funct}, \ref{eq:whisk:funct piu}} \begin{multlined}[t]
\LW{P}{\dl{Q}{W}{S'}} ; \dl{P}{QW}{QS'} ; (\LW{P}{\symmt{Q}{W}} \piu \LW{P}{\symmt{Q}{S'}}) ; \Idl{P}{WQ}{S'Q} ; \\
\RW{Q}{\dl{P}{W}{S'}} ; (\RW{Q}{\symmt{P}{W}} \piu \RW{Q}{\symmt{P}{S'}})
\end{multlined} \\
&=\tag{\ref{eq:whisk:Ldl}, \ref{eq:whisk:dl}} \begin{multlined}[t]
\dl{PQ}{W}{S'} ; \Idl{P}{QW}{QS'} ; \dl{P}{QW}{QS'} ; (\LW{P}{\symmt{Q}{W}} \piu \LW{P}{\symmt{Q}{S'}}) ; \Idl{P}{WQ}{S'Q} ; \\
\dl{P}{WQ}{S'Q} ; (\RW{Q}{\symmt{P}{W}} \piu \RW{Q}{\symmt{P}{S'}})
\end{multlined} \\
&=\tag{Iso} \dl{PQ}{W}{S'} ; (\LW{P}{\symmt{Q}{W}} \piu \LW{P}{\symmt{Q}{S'}}) ; (\RW{Q}{\symmt{P}{W}} \piu \RW{Q}{\symmt{P}{S'}}) \\
&=\tag{Funct. $\piu$} \dl{PQ}{W}{S'} ; ((\LW{P}{\symmt{Q}{W}};\RW{Q}{\symmt{P}{W}}) \piu (\LW{P}{\symmt{Q}{S'}};\RW{Q}{\symmt{P}{S'}})) \\
&=\tag{$\ast_3$, ind. hp.} \dl{PQ}{W}{S'} ; (\symmt{PQ}{W} \piu \symmt{PQ}{S'}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt dl}} \symmt{PQ}{W \piu S'}
\end{align*}

Equation (<ref>): $\RW{S}{\t} ; \symmt{Q}{S} = \symmt{P}{S} ; \LW{S}{\t}$. First observe that when $S$ is a monomial $W$, the following holds:

\begin{equation}\tag{$\ast$}
\RW{W}{\t} ; \symmt{Q}{W} = \symmt{P}{W} ; \LW{W}{\t}
\end{equation}

\begin{align*}
\RW{W}{\t} ; \symmt{Q}{W} &=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V}} \RW{W}{\t} ; \Piu[j]{\tapesymm{V_J}{W}} \\
&=\tag{Lemma~\ref{lm:whisk}} \Piu[i]{\tapesymm{U_i}{W}} ; \LW{W}{\t} \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt V}} \symmt{P}{W} ; \LW{W}{\t}
\end{align*}

Then we proceed by induction on $S$.

Case $S=\zero$ it follows from Definitions <ref> and definition of $\symmt$.

Case $S=W \piu S'$:

\begin{align*}
&\RW{W \piu S'}{\t} ; \symmt{Q}{W \piu S'} \\
&=\tag{\ref{eq:whisk:sum}, Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt dl}} \dl{P}{W}{S'} ; (\RW{W}{\t} \piu \RW{S'}{\t}) ; \Idl{Q}{W}{S'} ; \dl{Q}{W}{S'} ; (\symmt{Q}{W} \piu \symmt{Q}{S'}) \\
&=\tag{Iso} \dl{P}{W}{S'} ; (\RW{W}{\t} \piu \RW{S'}{\t}) ; (\symmt{Q}{W} \piu \symmt{Q}{S'}) \\
&=\tag{Funct. $\piu$} \dl{P}{W}{S'} ; ((\RW{W}{\t};\symmt{Q}{W}) \piu (\RW{S'}{\t};\symmt{Q}{S'})) \\
&=\tag{$\ast$, ind. hp.} \dl{P}{W}{S'} ; ((\symmt{P}{W};\LW{W}{\t}) \piu (\symmt{P}{S'};\LW{S'}{\t})) \\
&=\tag{Funct. $\piu$} \dl{P}{W}{S'} ; (\symmt{P}{W} \piu \symmt{P}{S'}) ; (\LW{W}{\t} \piu \LW{S'}{\t}) \\
&=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmt dl}, \ref{eq:whisk:sum}} \symmt{P}{W \piu S'} ; \LW{W \piu S'}{\t}
\end{align*}

Equations (<ref>): $\LW{ST}{\t} = \LW{S}{\LW{T}{\t}}$, (<ref>): $\LW{S}{\RW{T}{\t}} = \RW{T}{\LW{S}{\t}}$, (<ref>):$\RW{TS}{\t} = \RW{S}{\RW{T}{\t}}$. First we prove the particular cases in which $S$ and $T$ are monomials:

\begin{align*}
\LW{W}{\LW{Z}{\t}} &= \LW{WZ}{\t} &\tag{$\ast_1$}\\
\LW{W}{\RW{Z}{\t}} &= \RW{Z}{\LW{W}{\t}} &\tag{$\ast_2$}\\
\RW{W}{\RW{Z}{\t}} &= \RW{ZW}{\t} &\tag{$\ast_3$}
\end{align*}

All the three equations are proved by induction on $\t$ as follows:
the base cases $\t = \id\zero, \symmp{U}{V}, \diag{U}, \bang{U}, \codiag{U}, \cobang{U}$ are trivial by definition of $L$ and $R$. For $\t = \tape{c}$ we apply the definition of $L$ and $R$ and the fact that $\per$ is associative inside a tape.
The inductive cases follow from functoriality of $L$ and $R$ and the inductive hypothesis.

For the general cases, we start with (<ref>):
\begin{align*}
\LW{S}{\LW{T}{\t}} &=\tag{Def. $L$} \Piu[k]{\Piu[l]{\LW{W_k}{\LW{Z_l}{\t}}}}\\
&=\tag{$\ast_1$} \Piu[k]{\Piu[l]{\LW{W_kZ_l}{\t}}}\\
&=\tag{Def. $L$} \LW{ST}{\t}
\end{align*}

Regarding Equation (<ref>), first observe that the following holds:

\begin{equation*}\tag{$\ast$}
\RW{W}{\LW{T}{\t}} = \LW{T}{\RW{W}{\t}}
\end{equation*}

\begin{align*}
\RW{W}{\LW{T}{\t}} &=\tag{Def. $L$} \RW{W}{\Piu[l]{\LW{Z_l}{\t}}} \\
&=\tag{Def. $R$} \Piu[l]{\RW{W}{\LW{Z_l}{\t}}} \\
&=\tag{$\ast_2$} \Piu[l]{\LW{Z_l}{\RW{W}{\t}}} \\
&=\tag{Def. $L$} \LW{T}{\RW{W}{\t}}
\end{align*}

Then we proceed by induction on $S$:

Case $S = \zero$: if follows from Definition <ref> and (<ref>).

Case $S = W \piu S'$:
\begin{align*}
&\RW{W \piu S'}{\LW{T}{\t}} \\
&=\tag{Def. $R$} \dl{TP}{W}{S'} ; (\RW{W}{\LW{T}{\t}} \piu \RW{S'}{\LW{T}{\t}}) ; \Idl{TQ}{W}{S'} \\
&=\tag{$\ast$, ind. hp.} \dl{TP}{W}{S'} ; (\LW{T}{\RW{W}{\t}} \piu \LW{T}{\RW{S'}{\t}}) ; \Idl{TQ}{W}{S'} \\
&=\tag{\ref{eq:whisk:funct piu}} \dl{TP}{W}{S'} ; \Idl{T}{PW}{PS'} ; \LW{T}{\RW{W}{\t} \piu \RW{S'}{\t}} ; \dl{T}{QW}{QS'} ; \Idl{TQ}{W}{S'} \\
&=\tag{\ref{eq:whisk:Ldl}} \LW{T}{\dl{P}{W}{S'}} ; \LW{T}{\RW{W}{\t} \piu \RW{S'}{\t}} ; \LW{T}{\Idl{Q}{W}{S'}} \\
&=\tag{\ref{eq:whisk:funct}} \LW{T}{\dl{P}{W}{S'} ; (\RW{W}{\t} \piu \RW{S'}{\t}) ; \Idl{Q}{W}{S'}} \\
&=\tag{\ref{eq:whisk:sum}} \LW{T}{\RW{W \piu S'}{\t}}
\end{align*}

Equation (<ref>) is proved by means of the other two:

\begin{align*}
\RW{TS}{\t} & =\tag{\ref{eq:LRnatsym}} \symmt{P}{TS} ; \LW{TS}{\t} ; \symmt{TS}{Q}\\
& =\tag{\ref{eq:tape:LL}} \symmt{P}{TS} ; \LW{T}{\LW{S}{\t}} ; \symmt{TS}{Q}\\
& =\tag{\ref{eq:symmper}} \RW{S}{\symmt{P}{T}} ; \LW{T}{\symmt{P}{S}} ; \LW{T}{\LW{S}{\t}} ; \LW{T}{\symmt{S}{Q}}  ;   \RW{S}{\symmt{T}{Q}}  \\
& =\tag{\ref{eq:whisk:funct}} \RW{S}{\symmt{P}{T}} ; \LW{T}{\symmt{P}{S} ; \LW{S}{\t} ; \symmt{S}{Q}}  ;   \RW{S}{\symmt{T}{Q}}  \\
& =\tag{\ref{eq:LRnatsym}} \RW{S}{\symmt{P}{T}} ; \LW{T}{\RW{S}{\t} }  ;   \RW{S}{\symmt{T}{Q}}  \\
& =\tag{\ref{eq:tape:LR}} \RW{S}{\symmt{P}{T}} ; \RW{S}{\LW{T}{\t} }  ;   \RW{S}{\symmt{T}{Q}}  \\
& =\tag{\ref{eq:whisk:funct}} \RW{S}{\symmt{P}{T} ; \LW{T}{\t} ;\symmt{T}{Q}}  \\
& =\tag{\ref{eq:LRnatsym}} \RW{S}{\RW{T}{\t} }  \\
\end{align*}

Equation (<ref>): $\LW{P}{\t_2} ; \RW{S}{\t_1} = \RW{R}{\t_1} ; \LW{Q}{\t_2}$. Let $\t_1 \colon P \to Q, \t_2 \colon R \to S$, then we show by induction on $\t_1$ that

\[\LW{P}{\t_2} ; \RW{S}{\t_1} = \RW{R}{\t_1} ; \LW{Q}{\t_2}\]

Case $\t_1 = \id{\zero}$: by (<ref>), $ \RW{S}{\id{\zero}} = \id{\zero} = \RW{R}{\id{\zero}}$. By definition, $\LW{\zero}{\t_2}=\id{\zero}$.

Case $\t_1 = \tape{c}$: it holds by Lemma <ref>.

Case $\t_1 = \symmp{U}{V}, \diag{U}, \bang{U}$: these cases all follow the same pattern, thus we show only the one for $\diag{U}$:

\begin{align*}
\LW{U}{\t_2} ; \RW{S}{\diag{U}}&=\tag{\ref{eq:whisk:diag}} \LW{U}{\t_2} ; \diag{US} \\
&=\tag{\ref{ax:diagnat}} \diag{UR} ; (\LW{U}{\t_2} \piu \LW{U}{\t_2}) \\
&=\tag{\ref{eq:whisk:diag}} \RW{R}{\diag{U}} ; (\LW{U}{\t_2} \piu \LW{U}{\t_2}) \\
&=\tag{Def. $L$}\RW{R}{\diag{U}} ; (\LW{U\piu U}{\t_2} )     \end{align*}

Case $\t_1 = \t_1' ; \t_1''$: Suppose $\t_1' \colon P \to P', \t_1'' \colon P' \to Q, \t_2 \colon R \to S$

\begin{align*}
\LW{P}{\t_2} ; \RW{S}{\t_1'; \t_1''} & =\tag{\ref{eq:whisk:funct}} \LW{P}{\t_2} ; \RW{S}{\t_1'} ; \RW{S}{ \t_1''}\\
& =\tag{Ind. hp.} \RW{R}{\t_1'} ; \LW{P'}{\t_2} ; \RW{S}{ \t_1''}\\
& =\tag{Ind. hp.} \RW{R}{\t_1'} ; \RW{R}{\t_1''} ; \LW{Q}{\t_2}  \\
& =\tag{\ref{eq:whisk:funct}} \RW{R}{\t_1' ; \t_1''} ; \LW{Q}{\t_2}  \\
\end{align*}

Case $\t_1 = \t_1' \piu \t_1''$: Suppose $\t_1' \colon P_1 \to Q_1, \t_1'' \colon P' \to Q', \t_2 \colon R \to S$

\begin{align*}
\LW{P_1 \piu P'}{\t_2} ; \RW{S}{\t_1' \piu \t_1''}  &=\tag{\ref{eq:whisk:sum}, \ref{eq:whisk:funct piu}} (\LW{P_1}{\t_2} \piu \LW{P'}{\t_2}) ; (\RW{S}{\t_1'} \piu \RW{S}{\t_1''}) \\
&=\tag{Funct. $\piu$} (\LW{P_1}{\t_2} ; \RW{S}{\t_1'}) \piu ( \LW{P'}{\t_2} ; \RW{S}{\t_1''}) \\
&=\tag{Ind. hp.} (\RW{R}{\t_1'} ; \LW{Q_1}{\t_2}) \piu (\RW{R}{\t_1''} ; \LW{Q'}{\t_2}) \\
&=\tag{Funct. $\piu$} (\RW{R}{\t_1'} \piu \RW{R}{\t_1''}) ; (\LW{Q_1}{\t_2} \piu \LW{Q'}{\t_2}) \\
&=\tag{\ref{eq:whisk:sum}, \ref{eq:whisk:funct piu}}  \RW{R}{\t_1' \piu \t_1''} ; \LW{Q_1 \piu Q'}{\t_2}
\end{align*}

This concludes the proof of Lemma <ref>.

§.§ Other proofs of Section <ref>

Given a strict fb category $\Cat{D}$ and functor $H \colon \Cat{C} \to U_2(\Cat{D})$, one can define the fb-functor $H^{\sharp} \colon  F_2(\Cat{C})  \to \Cat{D}$  inductively on objects of $ F_2(\Cat{C}) $ as

\[H^{\sharp}(\unoG) = \unoG \qquad H^{\sharp}(AW)=H(A)\perG H^{\sharp}(W) \]

and on arrows as

\[H^{\sharp}(\id\unoG) ={\id{\unoG}} \qquad H^{\sharp}(\id{A})= H(\id{A}) \qquad H^{\sharp}(\tape{c})=H(c) \]

\[H^{\sharp}(f; g)=H^{\sharp}(f); H^{\sharp}(g) \qquad  H^{\sharp}(f \perG g)= H^{\sharp}(f) \perG H^{\sharp}(g)  \qquad  H^{\sharp}(\sigma_{A,B})=\sigma_{H(A),H(B)} \]

\[ H^{\sharp}(\bang{A})=\bang{H(A)} \qquad  H^{\sharp}(\diag{A})=\diag{H(A)} \qquad  H^{\sharp}(\cobang{A})=\cobang{H(A)} \qquad H^{\sharp}(\codiag{A})=\codiag{H(A)}\]

Observe that $H^{\sharp}$ is well-defined:

\begin{align*}
H^{\sharp}(\tape{\id{A}}) & =\tag{Def. $H^{\sharp}$}  H(\id{A}) \\
& =\tag{Def. $H^{\sharp}$} H^{\sharp}(\id{A})
\end{align*}

\begin{align*}
H^{\sharp}(\tape{c;d}) & =\tag{Def. $H^{\sharp}$}  H(c;d) \\
& =\tag{Fun. $H$} H(c); H(d)\\
& =\tag{Def. $H^{\sharp}$} H^{\sharp}(\tape{c}); H^{\sharp}(\tape{d}) \\
& =\tag{Fun. $H^{\sharp}$} H^{\sharp}(\tape{c}; \tape{d}) \\
\end{align*}

The axioms in Tables <ref> and <ref> are preserved by $H^{\sharp}$, since they hold in $\Cat{D}$.
By definition, $\tapeFunct{\cdot} \, ; H^{\sharp}= H$. Moreover $ H^{\sharp}$ is the unique strict fb functor satisfying this equation. Thus indeed $F_2 \dashv U_2$.

Observe that for all objects $S$ and arrows $\t \colon P \to Q$, it holds that

\begin{equation}\label{eq:mainwhiskering}
\t \per \id{S} = \RW{S}{\t} \qquad \qquad \id{S} \per \t = \LW{S}{\t}
\end{equation}

as shown below:

\begin{align*}
\t \per \id{S}  &= \LW{P}{\id{S}} ; \RW{S}{\t} \tag{Def. $\per$} \\
&= \RW{S}{\t} \tag{\ref{eq:whisk:id}}
\end{align*}

\begin{align*}
\id{S}  \per \t  &= \LW{S}{\t} ; \RW{Q}{\id{S}} \tag{Def. $\per$}\\
&= \LW{S}{\t} \tag{\ref{eq:whisk:id}}
\end{align*}

Thus $\id{P} \per \id{Q} \stackrel{\eqref{eq:mainwhiskering}}{=}  \LW{P}{\id{Q}} \stackrel{\eqref{eq:whisk:id}}{=}  \id{P \per Q}$. To conclude functoriality of $\per$, the key is the sliding law (<ref>):  for all  $\t_1 \colon P \to Q, \t_2 \colon Q \to S, \t_3 \colon P' \to Q', \t_4 \colon Q' \to S'$,

\begin{align*}
(\t_1 ; \t_2) \per (\t_3 ; \t_4) &=\tag{Def. $\per$}   \LW {P} {\t_3 ; \t_4} ; \RW {S'} {\t_1 ; \t_2} \\
&=\tag{\ref{eq:whisk:funct}} \LW {P} {\t_3} ; \LW {P} {\t_4} ; \RW {S'} {\t_1} ; \RW {S'} {\t_2} \\
&=\tag{\ref{eq:tape:LexchangeR}} \LW {P} {\t_3} ; \RW {Q'} {\t_1} ; \LW {Q} {\t_4}   ; \RW {S'} {\t_2} \\
&=\tag{Def. $\per$} (\t_1 \per \t_3) ; (\t_2 \per \t_4) \\
\end{align*}

By (<ref>) and (<ref>) it immediately follows that

\[\id{\uno} \per \t \; =  \; \t  \;= \; \t \per \id{\uno}\]

For associativity of $\per$, observe that for all  $\t_1 \colon P_1 \to Q_1, \t_2 \colon P_2 \to Q_2, \t_3 \colon P_3 \to Q_3$,

\begin{align*}
((\t_1 \per \t_2) \per \t_3 ) &=\tag{Def. $\per$}   \LW {P_1P_2} {\t_3} ; \RW {Q_3} {\LW{P_1}{\t_2}; \RW{Q_2}{\t_1}} \\
&=\tag{\ref{eq:whisk:funct}} \LW {P_1P_2} {\t_3} ; \RW {Q_3} {\LW{P_1}{\t_2}}; \RW {Q_3} {\RW{Q_2}{\t_1}} \\
&=\tag{\ref{eq:tape:LL},\ref{eq:tape:LR},\ref{eq:tape:RR}} \LW {P_1} {\LW{P_2}{\t_3}} ;  \LW{P_1}{\RW {Q_3}{\t_2}};  \RW{Q_2Q_3}{\t_1}\\
&=\tag{\ref{eq:whisk:funct}} \LW {P_1} {\LW{P_2}{\t_3} ; \RW {Q_3}{\t_2}};  \RW{Q_2Q_3}{\t_1} \\
&=\tag{Def. $\per$}  (\t_1 \per (\t_2 \per \t_3 ))
\end{align*}

So far, we proved that $(\CatTape, \per, \uno)$ is a strict monoidal category. For symmetries, observe that naturality follows immediately by (<ref>) and (<ref>). Inverses is Lemma <ref>.<ref> and the coherence axioms (<ref>) and (<ref>) hold by Lemma <ref>.<ref> and (<ref>).

By construction $(\CatTape, \piu, \zero, \symmp)$ is a symmetric strict monoidal category. We are left to prove a few laws. First,

\[ \id{\zero} \per \t  \; =  \; \id{\zero} = \t \per \id{\zero}\]

hold by (<ref>) and (<ref>). Regarding right distributivity of $\per$ over $\piu$, observe that for all
$\t_1 \colon P_1 \to Q_1, \, \t_2 \colon P_2 \to Q_2, \, \t_3 \colon P_3 \to Q_3$ it holds that:

\begin{align*}
(\t_1 \piu \t_2) \per \t_3 &=\tag{Def. $\per$} \LW{P_1 \piu P_2}{\t_3} ; \RW{Q_3}{\t_1 \piu \t_2} \\
&=\tag{\ref{eq:whisk:sum}, \ref{eq:whisk:funct piu}} (\LW{P_1}{\t_3} \piu \LW{P_2}{\t_3}) ; (\RW{Q_3}{\t_1} \piu \RW{Q_3}{\t_2}) \\
&=\tag{Funct. $\piu$} (\LW{P_1}{\t_3} ; \RW{Q_3}{\t_1}) \piu ( \LW{P_2}{\t_3} ; \RW{Q_3}{\t_2}) \\
&=\tag{Def. $\per$} (\t_1 \per \t_3) \piu (\t_2 \per \t_3)
\end{align*}

(This is tantamount to saying that $\CatTape$ has a natural right distributor whose components $\dr{P}{Q}{R}$ are all identity morphisms).

Next we have to check the axioms of coherence for strict rig categories that amount just to (<ref>), (<ref>), (<ref>) and (<ref>) from Figure <ref>.
Axiom (<ref>) is Lemma <ref>.<ref>.
Axiom (<ref>) follows by (<ref>) and (<ref>).
Axiom (<ref>) is Lemma <ref>.<ref>. Axiom (<ref>) holds by definition of $\symmt$ in Table <ref>. Finally, from Axiom (<ref>) and the naturality of the right distributor and of $\symmt $ we get that also $\delta^l$ is natural.
This proves that $\CatTape$ is a strict rig category. $(\CatTape, \piu, \zero, \symmp)$  is a finite biproduct category by definition.

All that is left to do is to prove that the inclusion functor $\sort \to \CatTape$ makes $\CatTape$ a $\sort$-sesquistrict fb rig category according to Definition <ref>. This means that we have to show that $\dl{A}{Q}{R} = \id{(A \per Q)  \piu (A \per R)}$ in $\CatTape$ for all $A \in \sort$, which is easily inferred from the inductive definition of $\dl{P}{Q}{R}$.

We have a trivial interpretation of $(\sort,\sign)$ in $\sort \to \CatTape$, given by $(\id\sort,\tapeFunct{\cdot})$. Suppose now that $H \colon \Cat M \to \Cat D$ is a sesquistrict fb rig category with an interpretation $\interpretation=(\alpha_\sort \colon \sort \to {Ob}(\Cat M), \alpha_\sign \colon \sign \to {Ar}(\Cat D))$. We aim to find a sesquistrict fb rig functor $(\alpha \colon \sort \to \Cat M, \beta \colon \CatTape \to \Cat D)$ such that $\id\sort ; \alpha = \alpha_{\sort}$ and $\tapeFunct{\cdot} ; \beta = \alpha_{\sign}$.
Since $(\sort,\sign)$ is a monoidal signature, $\interpretation$ is in fact a monoidal interpretation of $(\sort,\sign)$ into the ssm category $(\Cat D,\per,\uno)$, hence by freeness of $\CatString$ there exists a unique ssm functor $\dsem{-}_{\interpretation} \colon \CatString \to \Cat D$ that extends $\interpretation$. Now, because $\CatTape = F_2(\CatString)$ is by definition the free fb category generated by $\CatString$ and $\Cat D$ is also a fb category, we have that there is a unique fb functor $\beta \colon \CatTape \to \Cat D$ that extends $\dsem{-}_{\interpretation}$.
Now we prove that $\beta$ preserves the rest of the rig structure in several steps.
For the rest of this proof, to lighten up the calculations, with little abuse of notation we will treat $\GFunct$ as if it were the identity on objects. The context will make clear whether we will be speaking of $P \in Ob(\CatTape)$ or of $\GFunct(P) \in Ob(\Cat D)$.

*  We show that $\GFunct(\dl{P}{Q}{R})= \dl{P}{Q}{R}$  by induction on $P$.

Case $P=\zero$:
\begin{align*}
\GFunct(\dl{\zero}{Q}{R}) &=\tag{Def. $\delta^l$} \GFunct(\id\zero) \\
&=\tag{Def. $\GFunct$} \id\zero \\
&=\tag{\ref{eq:dl4}} \dl{\zero}{Q}{R}
\end{align*}

Case $P=U \piu P'$:
\begin{align*}
&\GFunct(\dl{U \piu P'}{Q}{R}) \\
&=\tag{Def. $\delta^l$} \GFunct((\id{U(Q\piu R)} \piu \dl{P'}{Q}{R});(\id{UQ} \piu \symmp{UR}{P'Q} \piu \id{P'R})) \\
&=\tag{Funct. $\GFunct$} (\GFunct(\id{U(Q\piu R)}) \piu \GFunct(\dl{P'}{Q}{R})) ; (\GFunct(\id{UQ}) \piu \GFunct(\symmp{UR}{P'Q}) \piu \GFunct(\id{P'R})) \\
&=\tag{Def. $\GFunct$} (\id{U(Q\piu R)} \piu \dl{P'}{Q}{R}) ; (\id{UQ} \piu \symmp{UR}{P'Q} \piu \id{P'R}) \\
&=\tag{Def. $\delta^l$} (\dl{U}{Q}{R} \piu \dl{P'}{Q}{R}) ; (\id{UQ} \piu \symmp{UR}{P'Q} \piu \id{P'R}) \\
&=\tag{\ref{eq:rigax5}} \dl{U \piu P'}{Q}{R}.
\end{align*}

*  Next we prove that $\GFunct(\symmt{P}{Q}) = \symmt{P}{Q}$ by induction on $Q$.

Case $Q=\zero$: it follows from definitions of $\symmt$ and $\GFunct$.

Case $Q=V \piu Q'$:

\begin{align*}
\GFunct(\symmt{P}{V \piu Q'}) &=\tag{Def. $\symmt$} \GFunct(\dl{P}{V}{Q'} ; (\Piu[i]{\tapesymm{U_i}{V}} \piu \symmt{P}{Q'})) \\
&=\tag{Def. $\GFunct$} \GFunct(\dl{P}{V}{Q'}) ; (\Piu[i]{\GFunct(\tapesymm{U_i}{V})} \piu \GFunct(\symmt{P}{Q'})) \\
&=\tag{\ref{lm:tape:Gsymmt.1}} \dl{P}{V}{Q'} ; (\Piu[i]{\GFunct(\tapesymm{U_i}{V})} \piu \GFunct(\symmt{P}{Q'})) \\
&=\tag{Def. $\GFunct$, ind. hp.} \dl{P}{V}{Q'} ; (\Piu[i]{\symmt{U_i}{V}} \piu \symmt{P}{Q'}) \\
&=\tag{Lemma~\ref{lm:sesqui:symmt}} \dl{P}{V}{Q'} ; (\symmt{P}{V} \piu \symmt{P}{Q'}) \\
&=\tag{\ref{eq:rigax1}} \symmt{P}{V \piu Q'}
\end{align*}

*  Now we show that if $\t \colon P \to Q$ be a tape diagram, then $\GFunct(\RW{W}{\t}) = \GFunct(\t) \per \id{W}$. We reason by induction on $\t$.

Case $\t=\id{\zero}$: $\GFunct(\RW{W}{\id{\zero}}) = \GFunct(\id{\zero}) = \id\zero = \id\zero \per \id{W} = \GFunct(\id{\zero}) \per \id{W}$

Case $\tape{c}$: $\GFunct(\RW{W}{\tape{c}}) = \GFunct(\tape{c \per \id{W}}) = c \per \id{W} = \GFunct(\tape{c}) \per \id{W}$

Case $\symmp{U}{V}$: $\GFunct(\RW{W}{\symmp{U}{V}}) = \GFunct(\symmp{UW}{VW}) = \symmp{UW}{VW} \stackrel{\eqref{eq:rigax2}}{=} \symmp{U}{V} \per \id{W} = \GFunct(\symmp{U}{V}) \per \id{W}$

Case $\diag{U}$: $\GFunct(\RW{W}{\diag{U}}) = \GFunct(\diag{UW}) = \diag{UW} \; \stackrel{Prop.\ref{prop:fbrig}}{=} \; \diag{U} \per \id{W} = \GFunct(\diag{U}) \per \id{W}$  and analogously for $\bang U, \codiag U, \cobang U$.

Case $\t = \t_1 ; \t_2$: $\GFunct(\RW{W}{(\t_1 ; \t_2)}) = \GFunct(\RW{W}{\t_1}) ; \GFunct(\RW{W}{\t_2}) = (\GFunct(\t_1) \per \id{W}) ; (\GFunct(\t_2) \per \id{W}) = (\GFunct(\t_1) ; \GFunct(\t_2)) \per \id{W} = \GFunct(\t_1 ; \t_2) \per \id{W}$

Case $\t = \t_1 \piu \t_2$: $\GFunct(\RW{W}{(\t_1 \piu \t_2)}) = \GFunct(\RW{W}{\t_1}) \piu \GFunct(\RW{W}{\t_2}) = (\GFunct(\t_1) \per \id{W}) \piu (\GFunct(\t_2) \per \id{W}) = (\GFunct(\t_1) \piu \GFunct(\t_2)) \per \id{W} = \GFunct(\t_1 \piu \t_2) \per \id{W}$.

*  Next we show that if $\t \colon P \to Q$ be a tape diagram, then

* $\GFunct(\RW{S}{\t}) = \GFunct(\t) \per \id{S}$

* $\GFunct(\LW{S}{\t}) = \id{S} \per \GFunct(\t)$

We prove the first point by induction on $S$:

Case $S = \zero$: $\GFunct(\RW{\zero}{\t}) = \GFunct(\id\zero) = \id\zero = \GFunct(\t) \per \id\zero$.

Case $S = W \piu S'$:

\begin{align*}
\GFunct(\RW{W\piu S'}{\t}) &=\tag{\ref{eq:whisk:sum}} \GFunct(\dl{P}{W}{S'} ; (\RW{W}{\t} \piu \RW{S'}{\t}) ; \dl{Q}{W}{S'}) \\
&=\tag{Def. $\GFunct$} \GFunct(\dl{P}{W}{S'}) ; (\GFunct(\RW{W}{\t}) \piu \GFunct(\RW{S'}{\t})) ; \GFunct(\dl{Q}{W}{S'}) \\
&=\tag{\ref{lm:tape:Gsymmt.1}} \dl{P}{W}{S'} ; (\GFunct(\RW{W}{\t}) \piu \GFunct(\RW{S'}{\t})) ; \dl{Q}{W}{S'} \\
&=\tag{\ref{lm:tape:GperW1}, ind. hp.} \dl{P}{W}{S'} ; ((\GFunct(\t) \per \id W) \piu (\GFunct(\t) \per \id {S'})) ; \dl{Q}{W}{S'} \\
&=\tag{Nat. $\delta^l$} \GFunct(\t) \per (\id W \piu \id {S'}) \\
&=\tag{Funct. $\piu$} \GFunct(\t) \per \id{W \piu S'}
\end{align*}

For the second point, we use the first point and naturality of $\per$-symmetries.

\begin{align*}
\GFunct(\LW{S}{\t}) &=\tag{Lemma~\ref{lemma:tapesymdis}.\ref{lm:tape:symmtInv}} \GFunct(\symmt{S}{P} ; \symmt{P}{S} ; \LW{S}{\t}) \\
&=\tag{\ref{eq:LRnatsym}} \GFunct(\symmt{S}{P} ; \RW{S}{\t} ; \symmt{Q}{S}) \\
&=\tag{Funct. $\GFunct$} \GFunct(\symmt{S}{P}) ; \GFunct(\RW{S}{\t}) ; \GFunct(\symmt{Q}{S}) \\
&=\tag{\ref{lm:tape:Gsymmt.2}} \symmt{S}{P} ; \GFunct(\RW{S}{\t}) ; \symmt{Q}{S} \\
&=\tag{\ref{lm:tape:Gper1}.a} \symmt{S}{P} ; (\GFunct(\t) \per \id{S}) ; \symmt{Q}{S} \\
&=\tag{Nat. $\symmt$} \id{S} \per \GFunct(\t)
\end{align*}

* Finally, we prove that if $\t_1 \colon P \to Q, \t_2 \colon R \to S$ are tape diagrams, then $\GFunct(\t_1 \per \t_2 ) =  \GFunct(\t_1) \per \GFunct(\t_2)$:

\begin{align*}
\GFunct(\t_1 \per \t_2 ) &=\tag{Def. $\per$} \GFunct(\LW{P}{\t_2};\RW{S}{\t_1}) \\
&=\tag{Funct. $\GFunct$} \GFunct(\LW{P}{\t_2});\GFunct(\RW{S}{\t_1}) \\
&=\tag{\ref{lm:tape:Gper1}} (\id{P} \per \GFunct(\t_2)) ; (\GFunct(\t_1) \per \id{S}) \\
&=\tag{Funct. $\per$} \GFunct(\t_1) \per \GFunct(\t_2)
\end{align*}

This concludes the proof of Theorem <ref>.

Recall our convention following Lemma <ref> that in fact we are considering the codomain of $F$ to be $\sCatT D$, and that we will expect the codomain of $F^\sharp$ also to be $\sCatT D$. Let us call $\interpretation_M$ and $\interpretation_R$ the obvious interpretations of $(\sort,\sign)$ in $\CatString$ and in $\CatTape$, respectively (the first is a monoidal, the second a sesquistrict rig interpretation). Notice that $\interpretation_R = \tapeFunct{\cdot} \circ \interpretation_M$. We have that $F$ induces a sesquistrict rig interpretation $F \circ \interpretation_M$ of $(\sort,\sign)$ in $\sCatT D$, given by

\[
\begin{tikzcd}[row sep=0em]
\sort \ar[r,"\alpha_\sort"] & Ob(\Cat D) \\
A \ar[r,|->] & F(A)
\end{tikzcd}
\qquad
\begin{tikzcd}[row sep=0em]
\sign \ar[r,"\alpha_\sign"] & Ar(\sCatT D) \\
f \ar[r,|->] & F(f)
\end{tikzcd}
\]

(we are assuming that $F(A)$ is a unary word of a unary word as a consequence of Lemma <ref>). This makes $(\alpha_\sort,\alpha_\sign)$ an interpretation because $F$ is strict monoidal. Indeed, if $\ar(f) = U$ with $U=A_1\dots A_n$, then the domain of $\alpha_\sign (f) = F(f)$ in $\sCatT D$ is the formal monomial $F(U)=F(A_1) \per \dots \per F(A_n)$, which is the result of applying the inductive extension of $\iota F$ to $U \in \sort^\star$ ($\iota \colon \Cat D \to \sCatT D$ being the inclusion functor). Since $\CatTape$ is the free sesquistrict  fb rig category generated by $(\sort,\sign)$, there exists a unique strict fb rig functor $F^\sharp \colon \CatTape \to \sCat D$ such that

* the pair $(\alpha_\sort,F^\sharp)$ is a sesquistrict fb rig functor from $(\sort \to \CatTape)$ to $(Ob(\Cat D) \to \sCatT D)$,

* $F^\sharp \circ \interpretation_R = F \circ \interpretation_M$.

The second condition means that $F^\sharp(\tape f) = F(f)$ for all $f \in \sign$. Now we want to prove that $F^\sharp(\tapeFunct c) = F(\tapeFunct c)$ for every circuit $c \in \CatString$.

We note that $F^\sharp \circ \interpretation_R$ is in fact a monoidal interpretation of $(\sort,\sign)$ in the ssm category $(\sCat D,\per,\uno)$, given by

\[
\alpha_\sort ' = \alpha_\sort \qquad
\begin{tikzcd}[row sep=0em]
\sign \ar[r,"\alpha_\sign '"] & Ar(\sCat D) \\
f \ar[r,|->] & F^\sharp(\tape f)
\end{tikzcd}
\]

Now, since $\CatString$ is the free strict symmetric monoidal category generated by $(\sort,\sign)$, there exists a unique strict monoidal functor $G \colon \CatString \to \sCat D$ such that $G \circ \interpretation_M = F^\sharp \circ \interpretation_R$. But both $G=F$ and $G=F^\sharp \circ \tapeFunct{\cdot}$ satisfy the above equation. Hence $F=F^\sharp \circ \tapeFunct{\cdot}$.

Regarding uniqueness: we have shown that every functor $H \colon \CatTape \to \sCat D$ extending the interpretation $F \circ \interpretation_M$ also satisfies $F = H \circ \tapeFunct{\cdot}$. Vice versa, any functor $H$ extending $F$ via $\tapeFunct{\cdot}$ clearly extends the interpretation $F \circ \interpretation_M$. Hence these two sets are in bijective correspondence, and by freeness of $\CatTape$ we know that there is only one $F^\sharp$ extending the interpretation $F \circ \interpretation_M$. Thus we conclude.

We conclude by proving Theorem <ref>. For this, it is convenient to first prove the following two lemmas.

In the main text, we claimed that $\WprecongBA$ is closed under $\per$, i.e. that
if $\t_1 \WprecongBA \t_2$ and  $\s_1 \WprecongBA \s_2$, then  $\t_1\per \s_1 \WprecongBA \t_2 \per \s_2$. This is immediate using the definition of $\per$ and Lemma <ref>, which we prove below.

If $\t_1 \WprecongBA \t_2 $, then $\RW{U}{\t_1}\WprecongBA \RW{U}{\t_2}$ for all monomials $U$.

We proceed by induction on the rule generating $\WprecongBA$.

If $\t_1  \WprecongBA \t_2$ by rule $(\wiskbasicR)$, then $\t_1   \WprecongBA \t_2$, i.e. there exists $(\t_1',\t_2')\in \basicR$ and $V\in S^*$ such that $\t_i=\RW{V}{\t_i'}$. Thus $\RW{U}{\t_i}= \RW{U}{\RW{V}{\t_i'}} \stackrel{\eqref{eq:tape:RR}}{=} \RW{VU}{\t_i'}$.
Since $(\t_1',\t_2')\in \basicR$, by definition of $ \wiskbasicR$, it holds that $\t_1 \wiskbasicR \t_2$ and thus, by rule $(\wiskbasicR)$, it holds that $\RW{U}{\t_1}   \WprecongBA \RW{U}{\t_2}$

If $\t_1   \WprecongBA \t_2$ by rule ($t$), then there exists $\t$ such that $\t_1   \WprecongBA \t$ and $\t   \WprecongBA \t_2$. By induction hypothesis, it holds that $\RW{U}{\t_1}   \WprecongBA \RW{U}{\t}$ and $\RW{U}{\t}   \WprecongBA \RW{U}{\t_2}$. Thus by rule ($t$),
$\RW{U}{\t_1}   \WprecongBA \RW{U}{\t_2}$.

The cases for $;$ and $\piu$ exploit induction in the same way and the laws (<ref>) and (<ref>) expressing the fact that $\RW{U}{-}$ preserves both $;$ and $\piu$.
The case for ($r$) is trivial.

If $\t_1 \WprecongBA \t_2 $, then $\RW{S}{\t_1}\WprecongBA \RW{S}{\t_2}$ and $\LW{S}{\t_1}\WprecongBA \LW{S}{\t_2}$ for all polynomials $S$.

We first show the case for $\RW{S}{-}$. The proof proceed by induction on $S$.

Case $S = \zero$: $\RW{\zero}{\t_1}=\id{\zero} \WprecongBA \id{\zero} = \RW{\zero}{\t_2}$.

Case $S = W \piu S'$:

\begin{align*}
\RW{W \piu S'}{\t_1} &= \dl{P}{W}{S'} ; (\RW{W}{\t_1} \piu \RW{S'}{\t_1}) ; \Idl{Q}{W}{S'}  \tag{Def. $R$} \\
&\WprecongBA  \dl{P}{W}{S'} ; (\RW{W}{\t_2} \piu \RW{S'}{\t_1}) ; \Idl{Q}{W}{S'}  \tag{Lemma \ref{lemmaCont}, Rules ($r$), ($;$), ($\piu$)} \\
&\WprecongBA \dl{P}{W}{S'} ; (\RW{W}{\t_2} \piu \RW{S'}{\t_2}) ; \Idl{Q}{W}{S'} \tag{Ind. Hyp., Rules ($r$), ($;$), ($\piu$)}\\
& = \RW{W \piu S'}{\t_2} \tag{Def. $R$}
\end{align*}

The proof for $\LW{S}{-}$ is trivial using the result for $\RW{S}{-}$ and (<ref>).

§ APPENDIX TO SECTION <REF>

In this Appendix we dive into the details of the calculus of matrices for categories with finite biproducts. In Section <ref> we present the standard calculus in the general setting of an arbitrary fb category. In Section <ref> we prove Theorem <ref>, showing how $F_2(\Cat C)$ and $\Mat{\fCMon{\Cat C}}$ are isomorphic as fb rig categories. In Section <ref> we define in detail the Kronecker product on $\Mat{\fCMon{\CatString}}$ and we show that it coincides with the monoidal product inherited from $F_2(\CatString)=\CatTape$. Finally, Section <ref> is dedicated to the proof of Theorem <ref>.

§.§ Matrix calculus for categories with finite biproducts

It is well known that morphisms in a fb category have a matrix representation such that composition corresponds to the usual matrix multiplication (see, for example, <cit.>). Here we recall how the correspondence is defined and a few useful properties. For the rest of this section we denote the composite of two morphisms $f_1 \colon X \to Y$ and $f_2 \colon Y \to Z$ as $f_2 \circ f_1 \colon X \to Z$.

Let $f \colon \PiuL[k=1][n]{A_k} \to \PiuL[k=1][m]{B_k}$ in $\Cat C$. The matrix associated to $f$ is the $m \times n$ matrix $\matr f$ whose $(j,i)$ entry (row $j$, column $i$), for $j=1,\dots,m$ and $i=1,\dots,n$, is

\[
f_{ji} \defeq \Bigl(
\begin{tikzcd}
A_i \ar[r,"\inj i"] & \PiuL[k=1][n]{A_k} \ar[r,"f"] & \PiuL[k=1][m]{B_k} \ar[r,"\proj j"] & B_j
\end{tikzcd}
\Bigr).
\]

For $f \colon \PiuL[k=1][n]{A_k} \to \PiuL[k=1][m]{B_k}$, we have

\[
\matr f =
\begin{pNiceMatrix}[first-row,first-col]
\rotatebox{90}{$\Lsh$} & A_1 & \dots & A_n \\
B_1&f_{11} &  \dots & f_{1n} \\
\vdots   & \vdots & \ddots & \vdots \\
B_m& f_{m1}  &   \dots      & f_{mn}
\end{pNiceMatrix}
\]

Notice how all morphisms in the $i$-th column have domain $A_i$, hence it makes sense to consider their pairing $\pairing{f_{1i},\dots,f_{mi}} \colon A_i \to \Piu[k]{B_k}$. Ranging over $i=1,\dots,n$, we can now consider their copairing $\copairing{\pairing{f_{11},\dots,f_{m1}},\dots,\pairing{f_{1n},\dots,f_{mn}}}$, which is now a morphism of type $\Piu[k]{A_k} \to \Piu[k]{B_k}$, just like $f$. Also, all morphisms in the $j$-th row have codomain $B_j$, hence we can take their copairing $\copairing{f_{j1},\dots,f_{jn}} \colon \Piu[k]{A_k} \to B_j$ and then, ranging over $j=1,\dots,m$, their collective pairing $\pairing{\copairing{f_{11},\dots,f_{1n}},\dots,\copairing{f_{m1},\dots,f_{mn}}}$, which is also of type $\Piu[k]{A_k} \to \Piu[k]{B_k}$. It turns out these morphisms are all equal to each other.

Let $f \colon \PiuL[k=1][n]{A_k} \to \PiuL[k=1][m]{B_k}$. Then

\begin{align*}
f &= \copairing{\pairing{f_{11},\dots,f_{m1}},\dots,\pairing{f_{1n},\dots,f_{mn}}} \\
&= \pairing{\copairing{f_{11},\dots,f_{1n}},\dots,\copairing{f_{m1},\dots,f_{mn}}}
\end{align*}

For the first equality we need to prove that $\inj i ; f = \pairing{f_{1i},\dots,f_{mi}}$ for all $i \in \{1,\dots,n\}$. This holds for any $i$ because $(\inj i ; f) ; \proj j = f_{ji}$ for all $j \in \{1,\dots,m\}$.

Similarly, for the second equality we need to prove that for all $j \in \{1,\dots,m\}$ we have $f ; \proj j = \copairing{f_{j1},\dots,j_{jn}}$, which is true because for all $i \in \{1,\dots,n\}$ it holds that $\inj i ; (f ; \proj j) = f_{ji}$.

Let $f$ and $g$ have same domain and codomain. Then $\matr f = \matr g$ if and only if $f = g$.

We denote with $\diagg X m \colon X \to \PiuL[j=1][m] X$ the generalised diagonal of $X$, inductively defined in the obvious way:

\begin{equation}\label{eq:generalised diagonal}
\diagg X 0 \defeq \bang X \qquad \diagg X {m+1} \defeq \Bigl(
\begin{tikzcd}[column sep=4em]
X \ar[r,"\diag X"] & X \piu X \ar[r,"\id X \piu \diagg X {m}"] & \PiuL[j=1][m+1] X
\end{tikzcd}
\Bigr)
\end{equation}

Similarly, we denote with $\codiagg X n \colon \PiuL[i=1][n]{X} \to X$ the generalised codiagonal of $X$, inductively defined as:

\begin{equation}\label{eq:generalised codiagonal}
\codiagg X 0 \defeq \cobang X \qquad \codiagg X {n+1} \defeq \Bigl(
\begin{tikzcd}[column sep=4em]
\PiuL[i=1][n+1]{X} \ar[r,"\id X \piu \codiagg X {n}"] & X \piu X \ar[r,"\codiag X"] & X
\end{tikzcd}
\Bigr).
\end{equation}

Let $f \colon \PiuL[k=1][n]{A_k} \to \PiuL[k=1][m]{B_k}$. Then

\begin{align*}
f &= \Bigl(
\begin{tikzcd}[ampersand replacement=\&,column sep=3em]
\PiuL[i=1][n]{A_i} \ar[r,"{\PiuL[i=1][n]{\diagg{A_i} m}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{A_i}} \ar[r,"{\PiuL[i=1][n]{\PiuL[j=1][m]{f_{ji}}}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{B_j}} \ar[r,"\codiagg{\Piu[j=1][m]{B_j}}{n}"] \& \PiuL[j=1][m]{B_j}
\end{tikzcd}
\Bigr) \\
&= \Bigl(
\begin{tikzcd}[ampersand replacement=\&,column sep=3em]
\PiuL[i=1][n]{A_i} \ar[r,"\diagg{\Piu[i=1][n]{A_i}} m"] \& \PPiuL j m i n {A_i} \ar[r,"{\PPiuL j m i n {f_{ji}}}"] \& \PPiuL j m i n {B_j} \ar[r,"{\PiuL[j=1][m]{\codiagg{B_j} n}}"] \& \PiuL[j=1][m]{B_j}
\end{tikzcd}
\Bigr)
\end{align*}

In general, if $u_j \colon X \to Y_j$, with $j=1,\dots,m$, we have

\[
\pairing{u_1,\dots,u_m} = \Bigl(
\begin{tikzcd}[column sep=4em]
X \ar[r,"\diagg X m"] & \PiuL[j=1][m]{X} \ar[r,"{\Piu[j]{u_j}}"] & \PiuL[j=1][m]{U_j}
\end{tikzcd}
\Bigr)
\]

(one can prove it by showing that the above satisfies the same universal property of $\pairing{u_1,\dots,u_m}$). Hence, for any $i \in \{1,\dots,n\}$,

\[
\pairing{f_{1i},\dots,f_{mi}} = \Bigl(
\begin{tikzcd}
A_i \ar[r,"\diagg {A_i} m"] & \PiuL[j=1][m]{A_j} \ar[r,"{\PiuL[j=1][m]{f_{ji}}}"] & \PiuL[j=1][m]{B_j}
\end{tikzcd}
\Bigr)
\]

Analogously, if $v_i \colon W_i \to Z$, with $i=1,\dots,n$,

\[
\copairing{v_1,\dots,v_n} = \Bigl(
\begin{tikzcd}
\PiuL[i=1][n]{W_i} \ar[r,"{\PiuL[i=1][n]{v_i}}"] & \PiuL[i=1][n]{Z} \ar[r,"\codiagg Z n"] & Z
\end{tikzcd}
\Bigr)
\]

Using these facts and Lemma <ref>, we get the two equations of the statement.

Let $A = \PiuL[k=1][n]{A_k}$ and $B=\PiuL[k=1][m]{B_k}$. Then

\[
\matr{\id A}
= \begin{pmatrix}
\delta_{A_i,A_j}
\end{pmatrix}
\begin{pNiceMatrix}[first-row,first-col]
& A_1      			& A_2 			          & A_{n-1} 			   & A_n \\
A_1 	& \id{A_1} 			& \zero_{A_2,A_1} & \Cdots   & \zero_{A_n,A_1}	\\
A_2 	& \zero_{A_1,A_2}	& 	\Ddots	  &  \Ddots  & \Vdots	\\
A_{n-1}  & \vdots 			& \Ddots 		  &  & \zero_{A_n,A_{n-1}} \\
A_n     & \zero_{A_1,A_n}	& \Cdots & \zero_{A_{n-1},A_n}   & \id{A_n}
\CodeAfter
\line{2-0}{3-0}
\line{0-2}{0-3}
%	\line{1-1}{4-4}
\end{pNiceMatrix}
\]

\[
\matr{\zero_{A,B}} = \begin{pmatrix}
\zero_{A_i,B_j}
\end{pmatrix}
\begin{pNiceMatrix}[first-row,first-col]
& A_1 & \dots & A_n\\
B_1&\zero_{A_1,B_1} &  \Cdots & \zero_{A_n,B_1} \\
\vdots   & \vdots & \ddots & \vdots\\
B_m& \zero_{A_1,B_m}  &   \Cdots      & \zero_{A_n,B_m} \\
\end{pNiceMatrix}
\]

For this reason we will sometimes simply write $\zero_{A,B}$ for the matrix $\matr{\zero_{A,B}}$ and $\id{A}$ for the matrix $\matr{\id A}$. The context they appear in will make clear whether we are referring to a matrix or to a morphism of $\Cat C$.

The matrix representation of morphisms in fb categories enjoys several nice properties.

For $f$ and $g$ of the appropriate type, we have:

* $\matr{g \circ f} = \matr g  \matr f$,

* $\matr{f \piu g} = \begin{pmatrix}
\matr f & \zero \\
\zero & \matr g
\end{pmatrix} $

* $\matr{\pairing{f,g}} = \begin{pmatrix}
\matr f \\ \matr g
\end{pmatrix}$

* $\matr{\copairing{f,g}} = \begin{pmatrix}
\matr f & \matr g
\end{pmatrix}$

* $\matr{\inj i \colon A_i \to \PiuL[k=1][n]{A_k}} = \begin{pmatrix}
\delta_{i,1} \\
\vdots \\
\delta_{i,n}
\end{pmatrix}$, $\matr{\proj j \colon \PiuL[k=1][n]{A_k} \to A_j} = \begin{pmatrix}
\delta_{1,j} & \Cdots & \delta_{m,j}
\end{pmatrix}$

* For $A = \PiuL[k=1][n]{A_k}$ and $B=\PiuL[k=1][m]{B_k}$,

\[
\matr{\symm{A}{B}} = \begin{pmatrix}
\matr{\zero_{B,A}} & \matr{\id B} \\
\matr{\id A} & \matr{\zero_{A,B}}
\end{pmatrix}
\]

matrix of size $(m+n) \times (n+m)$.

§.§ Additional details of the Proof of Theorem <ref>

We present here the two functors

\begin{equation}\label{eq:iso between CatTape and biproduct completion}
\begin{tikzcd}[column sep={8em,between origins}]
F_2(\Cat C) \ar[r,bend left,"\FF"name=F]   & \Mat{\fCMon{\Cat C}} \ar[l,bend left,"\GG"name=G]
\arrow[from=F,to=G,draw=none,"\cong"description]
\end{tikzcd}
\end{equation}

of Theorem <ref> explicitly.

$\FF$ was defined in the proof of Theorem <ref>, so let us define $\GG$.
On objects it simply is the identity. On morphisms: let

\[
M = (M_{ji})_{\substack{j=1\dots m \\ i=1 \dots n}} \colon \PiuL[i=1][n]{A_i} \to \PiuL[j=1][m]{B_j} \text{ in } \Mat{\fCMon{\Cat{C}}}.
\]

If $m=0$, then define $\GG(M)=\bang{\Piu[j]{B_j}}$; if $n=0$ define instead $\GG(M) = \cobang{\Piu[i]{A_i}}$. (This is consistent with the case $n=0=m$, because $\bang \zero = \cobang \zero = \id\zero$ by Axioms (<ref>) and (<ref>).)

Suppose now that $n \ne 0 \ne m$.
We have that $M_{ji}$ is a multiset of morphisms of type $A_i \to B_j$ in $\Cat{C}$. $M_{ji}$ determines a morphism in $F_2(\Cat{C})$:

\[
\Gg(M_{ji}) \defeq \sum_{a \in M_{ji}} \tapeFunct{a} \colon A_i \to B_j %\text{ in } F_2(\Cat{C}).
\]

Notice that for $M_{ji}=\emptyset$ we get $\Gg(\emptyset)=\zero_{A_i,B_j}$. Now, $\bigl(\Gg(M_{ji})\bigr)_{j=1\dots m, i=1 \dots n}$ is a matrix of morphisms of $F_2(\Cat{C})$, to which corresponds a unique arrow of the same type of $M$:

\[
\GG(M) \defeq
\Bigl(
\begin{tikzcd}[ampersand replacement=\&,column sep=4em]
\PiuL[i=1][n]{A_i} \ar[r,"{\PiuL[i=1][n]{\diagg{A_i} m}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{A_i}} \ar[r,"{\PiuL[i=1][n]{\PiuL[j=1][m]{\Gg(M_{ji})}}}"] \& \PiuL[i=1][n]{\PiuL[j=1][m]{B_j}} \ar[r,"\codiagg{\Piu[j=1][m]{B_j}}{n}"] \& \PiuL[j=1][m]{B_j}
\end{tikzcd}
\Bigr)
\]

where $\diagg X m \colon X \to \Piu[][m]{X}$ and $\codiagg Y n \colon Y \to \Piu[][n]{Y}$ are defined as:

\begin{equation}
\begin{array}{rclcrcl}
\diagg X 0 &\defeq& \bang X  & \qquad \qquad&\codiagg Y 0 &\defeq& \cobang{Y}  \\
\diagg X {m+1} &\defeq& \diag X ; \diagg X m & \qquad \qquad &\codiagg Y {n+1} &\defeq& \codiagg Y n ; \codiag Y
\end{array}
\end{equation}

Now we start showing that $\FF$ and $\GG$ are mutually inverse. We first observe a few properties of $\FF$: if $U = \PiuL[i=1][n]{A_i}$ then

\[
\FF(\id U) =
\begin{pNiceMatrix}
\multiset{\id{A_1}}  	& \emptyset & \Cdots & \emptyset  \\
\emptyset  &   & \Ddots & \Vdots \\
\Vdots & \Ddots &   & \emptyset  \\
\emptyset  & \Cdots & \emptyset  & \multiset{\id{A_{n}}}
\CodeAfter
\line{1-1}{4-4}
\end{pNiceMatrix}
\]

Since $\FF$ sends symmetries, (co)diagonals and (co)bangs into symmetries, (co)diagonals and (co)bangs of $\Mat{\fCMon{\Cat C}}$, if $U = \PiuL[i=1][n]{A_i}$ and $V=\PiuL[j=1][m]{B_j}$ then:

\[
\FF(\symm{U}{V}) =
\begin{pNiceMatrix}
\emptyset_{m \times n} & \FF(\id V)  \\
\FF(\id U) & \emptyset_{n \times m}  \\
\end{pNiceMatrix}
\]

\[
\FF(\diag U) =
\begin{pNiceMatrix}
\FF(\id U) & \FF(\id U)
\end{pNiceMatrix}
\qquad
\FF(\codiag U) =
\begin{pNiceMatrix}
\FF(\id U) \\
\FF(\id U)
\end{pNiceMatrix}
\]

\[
\FF(\bang U) = \text{empty matrix of size $0 \times n$} \qquad \FF(\cobang U) = \text{empty matrix of size $n \times 0$}
\]

Since $\Cat{C}$ has all finite biproducts, $\Cat{C}[U,V]$ is a commutative monoid where addition is given using diagonals and codiagonals as in (<ref>).
The action of $\FF$ on $f_1 + f_2 \colon U \to V$, with $U = \PiuL[i=1][n]{A_i}$ and $V=\PiuL[j=1][m]{B_j}$, is the usual entry-by-entry addition of matrices:

\begin{align*}
\FF(f_1 + f_2) &= \FF(\codiag V) \circ \FF(f_1 \piu f_2) \circ \FF(\diag U) \\
\begin{pNiceMatrix}
\FF(\id V) & \FF(\id V)
\end{pNiceMatrix}
\begin{pNiceMatrix}
\FF(f_1) & \emptyset_{m \times n} \\
\emptyset_{m \times n} & \FF(f_2)
\end{pNiceMatrix}
\begin{pNiceMatrix}
\FF(\id U) \\
\FF(\id U)
\end{pNiceMatrix} \\
\begin{pNiceMatrix}
\FF(f_1) & \FF(f_2)
\end{pNiceMatrix}
\begin{pNiceMatrix}
\FF(\id U) \\
\FF(\id U)
\end{pNiceMatrix} \\
&= \FF(f_1) + \FF(f_2).
\end{align*}

If $f_1 \colon W \to U$ and $f_2 \colon W \to V$ then

\begin{align*}
\FF(\pairing{f_1,f_2}) &= \FF((f_1 \piu f_2)  \circ \pairing{\id W, \id W}) \\
&= \FF(f_1 \piu f_2) \circ \FF(\diag W) \\
&= \begin{pmatrix}
\FF(f_1) & \emptyset \\
\emptyset & \FF(f_2)
\end{pmatrix}
\begin{pNiceMatrix}
\FF(\id W) \\
\FF(\id W)
\end{pNiceMatrix} \\
&= \begin{pNiceMatrix}
\FF(f_1) \\
\FF(f_2)
\end{pNiceMatrix}
\end{align*}

Analogously, if $f_1 \colon U \to W$ and $f_2 \colon V \to W$ then $\FF(\copairing{f_1,f_2}) = \begin{pNiceMatrix}
\FF(f_1) & \FF(f_2)
\end{pNiceMatrix}$.

$\GG \colon \Mat{\fCMon{\Cat C}} \to F_2(\Cat C)$ is a functor that preserves biproducts.

\[
\begin{tikzcd}
\PiuL[i=1][n]{A_i} \ar[r,"M"] & \PiuL[k=1][m]{V_k} \ar[r,"N"] & \PiuL[j=1][l]{W_j}.
\end{tikzcd}
\]

We aim to compute $\GG(N \circ M)$. We have

\begin{align*}
(N \circ M)_{ji} = (N \cdot M)_{ji} &= \sum_{k=1}^m N_{jk} \circ M_{ki} & \tag{Sum and composition in $\fCMon{\CatString}$} \\
&= \bigcup_{k=1}^m {\multiset{ b \circ_{\Cat C} a \mid a \in M_{ki}, \, b \in N_{jk}} } & \tag{Union of multisets}
\end{align*}

\[
\Gg\bigl( (N\circ M)_{ji}  \bigr) = \sum_{k=1}^m \, \sum_{\substack{a \in M_{ki} \\ b \in N_{jk}}} \tape{b \circ a}
\]

Now, $\GG(N) \circ \GG(M)$ is a morphism in $F_2(\Cat C)$ whose associated matrix, by Proposition <ref>,

\[
\bigl( \Gg(N_{wv})  \bigr)_{\substack{w=1\dots l \\ v=1\dots m}} \cdot \bigl( \Gg(M_{vu})  \bigr)_{\substack{v=1 \dots m \\ u=1 \dots n}}
\]

whose entry $(j,i)$, for $i \in \{1,\dots, n\}$ and $j \in \{1,\dots, m\}$, is the following sum of compositions in $F_2(\Cat C)$:

\begin{align*}
\bigl( \matr{\GG(N) \circ \GG(M)}  \bigr)_{ji} &= \sum_{k=1}^m \Gg(N_{jk}) \circ \Gg(M_{ki}) \\
&= \sum_{k=1}^m \Bigl( \sum_{b \in N_{jk}} \tape b \Bigr) \circ \Bigl( \sum_{a \in M_{ki}} \tape a \Bigr) \\
&= \sum_{k=1}^m \sum_{a \in M_{ki}} \Bigl( \sum_{b \in N_{jk}} \tape b \Bigr) \circ \tape a \tag{$\CMon$-enrichment: $v \circ (f+g)= v \circ f + v \circ g$} \\
&= \sum_{k=1}^m \sum_{a \in M_{ki}} \sum_{b \in N_{jk}} \tape b \circ \tape a \tag{$\CMon$-enrichment: $(f+g) \circ u = f \circ u + g \circ u$} \\
&= \sum_{k=1}^m \sum_{a \in M_{ki}} \sum_{b \in N_{jk}} \tape{b \circ a} \tag{\refeq{ax:tape}} \\
&= \Gg\bigl( (N\circ M)_{ji}  \bigr) \\
&= \matr{\GG(N \circ M)}_{ji}.
\end{align*}

Hence $\GG(N) \circ \GG(M) = \GG(N \circ M)$ by Corollary <ref>.

Regarding preservation of biproducts, if $M \colon \PiuL[k=1][n]{A_k} \to \PiuL[k=1][n']{A_k'}$ and $N \colon \PiuL[k=1][m]{B_k} \to \PiuL[k=1][m']{B_k}$ are any two matrices, we have that

\[
\GG(M \piu N) = \GG \begin{pNiceMatrix}
M & \emptyset \\
\emptyset & N
\end{pNiceMatrix} \qquad \text{(block matrix)}
\]

thus $\GG(M \piu N)$ is the morphism in $\CatTape$ whose associated matrix is

\[
\begin{pNiceMatrix}
\Gg(M_{11}) & \Cdots & \Gg(M_{1n}) & \zero & \Cdots & \zero \\
\vdots & \Ddots & \vdots & \vdots &  & \vdots \\
\Gg(M_{n'1}) & \dots & \Gg(M_{n'n}) & \zero & \dots & \zero \\
\zero & \Cdots & \zero & \Gg(N_{11}) & \Cdots & \Gg(N_{1m}) \\
\vdots &  & \vdots & \vdots & \ddots & \vdots \\
\zero & \Cdots & \zero & \Gg(N_{m'1}) & \Cdots & \Gg(N_{m' m})
\CodeAfter
\line{1-4}{3-6}
\line{4-1}{6-3}
\end{pNiceMatrix}
\]

which is exactly the block matrix $\begin{pNiceMatrix}
\matr{\GG(M)} & \zero \\
\zero & \matr{\GG(N)}
\end{pNiceMatrix}$, which in turn is $\matr{\GG(M) \piu \GG(N)}$ by Proposition <ref> (<ref>). Hence $\GG(M \piu N) = \GG(M) \piu \GG(N)$.

In light of this, in order to check that $\GG$ preserves identities it suffices to make sure that $\GG(\id A) = \id A$ for $A$ object in $\Cat C$ (seen as a unary list). And indeed $\GG(\id A)$ is the morphism whose associated matrix is the $1 \times 1$ matrix
\begin{pNiceMatrix}
\multiset{\id A}
\end{pNiceMatrix}
hence $\GG(\id A) = \id A$.

$\FF$ and $\GG$ are mutually inverse.

It is not difficult to prove by induction on $f$ that $\GG\FF(f) = f$, using Proposition <ref>. We show here that $\FF\GG = \id{}$:
let $M \colon \PiuL[i=1][n]{A_i} \to \PiuL[j=1][m]{B_j}$. First notice that

\[
\GG(M) = \copairing{\pairing{\Gg(M_{11}),\dots,\Gg(M_{n1})}, \dots, \pairing{\Gg(M_{1m}),\dots,\Gg(M_{mn}) }}
\]

by Lemma <ref> and Proposition <ref>.

\begin{align*}
\FF\GG(M) &= \FF \Bigl( \copairing{\pairing{\sum_{f \in M_{11}} \tape f,\dots,\sum_{f \in M_{n1}} \tape f}, \dots, \pairing{\sum_{f \in M_{1m}} \tape f,\dots,\sum_{f \in M_{mn}} \tape f}} \Bigr) & \tag{Definition of $\GG$} \\
\begin{pNiceMatrix}
\FF\bigl( \sum_{f \in M_{11}} \tape f \Bigr) & \dots & \FF\bigl( \sum_{f \in M_{1m}} \tape f \Bigr) \\
\vdots & \ddots & \vdots \\
\FF\bigl( \sum_{f \in M_{n1}} \tape f \Bigr) & \dots & \FF\bigl( \sum_{f \in M_{mn}} \tape f \Bigr)
\end{pNiceMatrix}
& \tag{Remark~\ref{rem: FF of pairing and copairings}} \\
&= M
\end{align*}

because for every $j \in \{1,\dots,m\}$ and $i \in \{1,\dots,n\}$

\begin{align*}
\FF\bigl( \sum_{f \in M_{ji}} \tape f \Bigr) &= \sum_{f \in M_{ji}} \FF(\tape f) & \tag{Remark~\ref{rem:FF(t1+t2)=FF(t1)+FF(t2)}} \\
&= \sum_{f \in M_{ji}}
\begin{pNiceMatrix}
\multiset{f}
\end{pNiceMatrix} \\
&= M_{ji}
\end{align*}

where above $\sum_{f \in M_{ji}}
\begin{pNiceMatrix}
\multiset{f}
\end{pNiceMatrix} $ is an entry-by-entry sum of $1 \times 1$ matrices, which yields the matrix whose only entry is $\sum_{f \in M_{ji}} \multiset f$: a sum of multisets equal to $M_{ji}$ itself.

§.§ Kronecker product. Details of the proof of Theorem <ref>

We will work using $\Cat C = \CatString$ here, but everything that follows can be generalised to an arbitrary SMC. Recall the definition of $\kron$. On objects it is set as follows:

\[
\Bigl(\PiuL[i=1][n]{U_i} \Bigr) \kron \Bigl( \PiuL[j=1][m]{V_j} \Bigr) \defeq \PiuL[i=1][n]{\PiuL[j=1][m]{U_iV_j}}.
\]

If $M \colon \PiuL[i=1][n]{U_i} \to \PiuL[i'=1][n']{U_{i'}'}$ and $N \colon \PiuL[j=1][m]{V_j} \to \PiuL[j'=1][m']{V_{j'}'}$, define $M \kron N$ as the block matrix:

\[
M \kron N =
\begin{pNiceMatrix}[first-row,first-col]
& U_1V_1 & \Cdots & U_1V_m & \Cdots & U_nV_1 & \Cdots & U_nV_m \\
U_1'V_1' 	& \Block[borders={right,bottom}]{3-3}{M_{11} \per N} & & &  & \Block[borders={left,bottom}]{3-3}{M_{1n} \per N}\\
\Vdots & & & & \Hdotsfor{1}	& \\
U_1'V_{m'}' & &  & & & &   \\
\Vdots 	& & \Hdotsfor{1} & &  & & \Hdotsfor{1} & \\
U_{n'}'V_1' 	& \Block[borders={right,top}]{3-3}{M_{n'1} \per N} &  & &  & \Block[borders={left,top}]{3-3}{M_{n'n} \per N}\\
\Vdots & & & & \Hdotsfor{1} & \\
\end{pNiceMatrix}
\]

\[
M_{i'i} \per N =
\begin{pNiceMatrix}
M_{i'i} \per N_{11} & \dots & M_{i'i} \per N_{1m} \\
\vdots & \ddots & \vdots \\
M_{i'i} \per N_{m'1} & \dots & M_{i'i} \per N_{m'n'}
\end{pNiceMatrix}
\]

In other words, $M \kron N$ is a matrix of size $n' m' \times n  m$, whose rows are indexed by $(i',j') \in \{1,\dots,n'\} \times \{1,\dots,m'\}$ and whose columns by $(i,j) \in \{1,\dots,n\} \times \{1,\dots,m\}$; then we have

\[
(M \kron N)_{(i',j'),(i,j)} = M_{i'i} \per N_{j'j} = \multiset{a \per_{\CatString} b \mid a \in M_{i'i},\, b \in N_{j'j}}.
\]

We will show that $\kron$ coincides with the tensor product inherited from $\CatTape$. We begin by proving some preliminary results.

Let $M \colon P \to P'$ and $N \colon Q \to Q'$, with $P=\PiuL[i=1][n]{U_i}$, $P'= \PiuL[i'=1][n']{U_{i'}'}$, $Q=\PiuL[j=1][m]{V_j}$ and $Q'=\PiuL[j'=1][m']{V_{j'}'}$. Then

\begin{align*}
M \kron N &= (\id{P'} \kron N) \circ (M \kron \id{Q}) \\
&= (M \kron \id{Q'}) \circ (\id P \kron N)
\end{align*}

We only show the first equality: the other is analogous. We have:

\[
\id{P'} \kron N =
\begin{pNiceMatrix}
\multiset{\id{U_1'}} \per N 	& \emptyset \per N & \Cdots & \emptyset \per N \\
\emptyset \per N &  & \Ddots & \Vdots \\

\Vdots & \Ddots & \Ddots[shorten=0.2em] & \emptyset \per N \\
\emptyset \per N & \Cdots & \emptyset \per N & \multiset{\id{U_{n'}'}} \per N
\end{pNiceMatrix}
\]

Notice that $\emptyset \per N$ is $\emptyset_{m' \times m}$, the $m' \times m$ matrix whose every entry is the empty multiset. Next,

\[
M \kron \id Q =
\begin{pNiceMatrix}
M_{11} \per \id Q & \dots & M_{1n} \per \id Q \\
\vdots & \ddots & \vdots \\
M_{n'1} \per \id Q & \dots & M_{n'n} \per \id Q
\end{pNiceMatrix}
\]

(in the above $\id{P'}$ and $\id Q$ are identity morphisms in $\Mat{\fCMon{\CatString}}$, hence they are matrices). To save space, we shall drop the multiset brackets in $\multiset{\id{U_{i'}'}}$, since it is a singleton, and simply write $\id{U_{i'}'}$. Therefore $(\id{P'} \kron N) \circ (M \kron \id{Q})$ is equal to:

\[
\scalebox{0.9}{$
\begin{pNiceMatrix}
(\id{U_1'} \per N) \circ (M_{11} \per \id Q) & (\id{U_1'} \per N) \circ (M_{12} \per \id Q) & \dots & (\id{U_1'} \per N) \circ (M_{1n} \per \id Q) \\
(\id{U_2'} \per N) \circ (M_{21} \per \id Q) & (\id{U_2'} \per N) \circ (M_{22} \per \id Q) & \dots & (\id{U_2'} \per N) \circ (M_{2n} \per \id Q) \\
\vdots & \vdots & \ddots & \vdots \\
(\id{U_1{n'}'} \per N) \circ (M_{n'1} \per \id Q) & (\id{U_{n'}'} \per N) \circ (M_{n'2} \per \id Q) & \dots & (\id{U_{n'}'} \per N) \circ (M_{n'n} \per \id Q) \\
\end{pNiceMatrix}$}
\]

In other words, $(\id{P'} \kron N) \circ (M \kron \id{Q})$ is a matrix consisting of $n'n$ blocks (the entries in the matrix above), each of size $m' \times m$, where the block at row $i'$ and column $i$ is

\[
B^{i'i} = \underbrace{(\id{U_{i'}'} \per N)}_{m' \times m} \circ \underbrace{(M_{i'i} \per \id Q)}_{m' \times m}.
\]

The entry $(j',j)$ of the above block is the following sum of composite of multisets:

\begin{align*}
B_{j'j}^{i'i} &=	\sum_{k=1}^m (\id{U_{i'}'} \per N)_{j'k} \circ (M_{i'i} \per \id Q)_{kj} \\
&= \sum_{k=1}^m (\id{U_{i'}'} \per N_{j'k}) \circ (M_{i'i} \per (\id Q)_{kj})
\end{align*}

Now, if $k \ne j$ then $(\id Q)_{kj} = \emptyset$, hence $M_{i'i} \per \emptyset = \emptyset$ and $(\id{U_{i'}'} \per N_{j'k}) \circ \emptyset =\emptyset$. Therefore,

\begin{align*}
B_{j'j}^{i'i} &= (\id{U_{i'}'} \per N_{j'j}) \circ (M_{i'i} \per \id{V_j}) \\
&= \multiset{\id{U_{i'}'} \per_{\CatString} b \mid b \in N_{j'j}} \circ
\multiset{a \per_{\CatString} \id{V_j} \mid a \in M_{i'i}} & \tag{Definition of $\per_{\fCMon{\CatString}}$} \\
&= \multiset{(\id{U_{i'}'} \per_{\CatString} b) \circ (a \per_{\CatString} \id{V_j}) \mid a \in M_{i'i},\, b \in N_{j'j} } & \tag{Definition of $\circ$ in $\fCMon{\CatString}$} \\
&= \multiset{ a \per_{\CatString} b \mid a \in M_{i'i},\, b \in N_{j'j} } & \tag{Functoriality of $\per_{\CatString}$} \\
&= (M \kron N)_{(i',j'),(i,j)}. \tag*{\qedhere}
\end{align*}

$\Mat{\fCMon{\CatString}}$ inherits a tensor functor $\perM$ from $\CatTape$, via the isomorphism (<ref>), defined as

\[
\text{$M \perM N$} \defeq {\FF(\GG(M) \perT \GG(N))}.
\]

This makes $\Mat{\fCMon{\CatString}}$ a strict fb rig category, where $\FF$ and $\GG$ strictly preserve the rig structure. Now we show that $\perM$ actually coincides with the Kronecker product.

Let $P=\PiuL[i=1][n]{U_i}$ and $Q=\PiuL[j=1][m]{V_j}$. Then $\id P \kron \id Q = \id{P \kron Q}$.

We have:

\begin{align*}
\id P \kron \id Q &=
\begin{pNiceMatrix}
(\id P)_{11} \per \id Q & \dots & (\id P)_{1n} \per \id Q \\
\vdots & \ddots & \vdots \\
(\id P)_{n1} \per \id Q & \dots & (\id P)_{nn} \per \id Q
\end{pNiceMatrix}
\\
\begin{pNiceMatrix}
\multiset{\id{U_1}} \per \id Q 	& \emptyset & \Cdots & \emptyset  \\
\emptyset  &  & \Ddots & \Vdots \\
\Vdots & \Ddots &  & \emptyset  \\
\emptyset  & \Cdots & \emptyset  & \multiset{\id{U_{n}}} \per \id Q
\CodeAfter
\line{1-1}{4-4}
\end{pNiceMatrix}
\\
\begin{pNiceMatrix}
\multiset{\id{U_1} \per \id{V_1}}  	& \emptyset & \Cdots & \emptyset  \\
\emptyset  & \multiset{\id{U_1} \per \id{V_m}} & \Ddots & \Vdots \\
\Vdots & \Ddots & \multiset{\id{U_n} \per \id{V_1}}  & \emptyset  \\
\emptyset  & \Cdots & \emptyset  & \multiset{\id{U_{n}} \per \id{V_m}}
\CodeAfter
\line{1-1}{2-2}
\line{2-2}{3-3}
\line{3-3}{4-4}
\end{pNiceMatrix}
\\
&= \id{\Piu[i]{\Piu[j]{U_iV_j}}} \\
&= \id{P \kron Q}. \qedhere
\end{align*}

$\perM = \kron$ in $\Mat{\fCMon{\CatString}}$.

On objects: if $P=\PiuL[i=1][n]{U_i}$ and $Q = \PiuL[j=1][m]{V_j}$ we have $P \perM Q = \FF(P \perT Q) = \FF(\Piu[i]{\Piu[j]{U_iV_j}} = P \kron Q$.