The word problem for double categories

TL;DR

This paper presents a quadratic algorithm to solve the word problem in free double categories by translating it into the well-understood word problem for 2-categories, simplifying reasoning and revealing that double categories are not more expressive than 2-categories.

Contribution

It introduces a translation method from double categories to 2-categories that enables efficient decision procedures for diagram equality.

Findings

Quadratic algorithm for diagram equality in free double categories.

Double categories are not more expressive than 2-categories.

The translation helps reason about double categories using 2-category language.

Abstract

We solve the word problem for free double categories without equations between generators by translating it to the word problem for 2-categories. This yields a quadratic algorithm deciding the equality of diagrams in a free double category. The translation is of interest in its own right since and can for instance be used to reason about double categories with the language of 2-categories, sidestepping the pinwheel problem. It also shows that although double categories are formally more general than 2-categories, they are not actually more expressive, explaining the rarity of applications of this notion.

Equations

$$A$$

$$\sim$$

$$v$$

$$p(t(\text{ \leavevmode\hbox to57.31pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{19.40218pt}{14.22638pt}\pgfsys@curveto{19.40218pt}{17.08492pt}{17.08492pt}{19.40218pt}{14.22638pt}{19.40218pt}\pgfsys@curveto{11.36784pt}{19.40218pt}{9.05058pt}{17.08492pt}{9.05058pt}{14.22638pt}\pgfsys@curveto{9.05058pt}{11.36784pt}{11.36784pt}{9.05058pt}{14.22638pt}{9.05058pt}\pgfsys@curveto{17.08492pt}{9.05058pt}{19.40218pt}{11.36784pt}{19.40218pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{11.81618pt}{13.28194pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mu$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{47.5485pt}{14.22638pt}\pgfsys@curveto{47.5485pt}{16.91568pt}{45.36844pt}{19.09573pt}{42.67914pt}{19.09573pt}\pgfsys@curveto{39.98984pt}{19.09573pt}{37.80978pt}{16.91568pt}{37.80978pt}{14.22638pt}\pgfsys@curveto{37.80978pt}{11.53708pt}{39.98984pt}{9.35703pt}{42.67914pt}{9.35703pt}\pgfsys@curveto{45.36844pt}{9.35703pt}{47.5485pt}{11.53708pt}{47.5485pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{42.67914pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{40.70322pt}{12.50417pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\nu$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{0.0pt}{14.22638pt}\pgfsys@lineto{8.8906pt}{14.22638pt}\pgfsys@moveto{19.56216pt}{14.22638pt}\pgfsys@lineto{37.64981pt}{14.22638pt}\pgfsys@moveto{47.7085pt}{14.22638pt}\pgfsys@lineto{56.90552pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{14.22638pt}{0.0pt}\pgfsys@lineto{14.22638pt}{8.8906pt}\pgfsys@moveto{14.22638pt}{19.56218pt}\pgfsys@lineto{14.22638pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{42.67914pt}{0.0pt}\pgfsys@lineto{42.67914pt}{9.19704pt}\pgfsys@moveto{42.67914pt}{19.25574pt}\pgfsys@lineto{42.67914pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }))=p(\text{ \leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{34.14365pt}\pgfsys@lineto{34.14365pt}{34.14365pt}\pgfsys@lineto{34.14365pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{34.14365pt}{34.14365pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{16.96704pt}{25.60774pt}\pgfsys@curveto{16.96704pt}{28.75557pt}{14.41528pt}{31.30733pt}{11.26746pt}{31.30733pt}\pgfsys@curveto{8.11963pt}{31.30733pt}{5.56787pt}{28.75557pt}{5.56787pt}{25.60774pt}\pgfsys@curveto{5.56787pt}{22.45992pt}{8.11963pt}{19.90816pt}{11.26746pt}{19.90816pt}\pgfsys@curveto{14.41528pt}{19.90816pt}{16.96704pt}{22.45992pt}{16.96704pt}{25.60774pt}\pgfsys@closepath\pgfsys@moveto{11.26746pt}{25.60774pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{0.0}{0.0}{0.5}{6.91386pt}{24.35774pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t(\mu)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{28.51317pt}{8.5359pt}\pgfsys@curveto{28.51317pt}{11.7434pt}{25.91304pt}{14.34352pt}{22.70555pt}{14.34352pt}\pgfsys@curveto{19.49806pt}{14.34352pt}{16.89793pt}{11.7434pt}{16.89793pt}{8.5359pt}\pgfsys@curveto{16.89793pt}{5.32841pt}{19.49806pt}{2.72829pt}{22.70555pt}{2.72829pt}\pgfsys@curveto{25.91304pt}{2.72829pt}{28.51317pt}{5.32841pt}{28.51317pt}{8.5359pt}\pgfsys@closepath\pgfsys@moveto{22.70555pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.5}{0.0}{0.0}{0.5}{18.62337pt}{7.2859pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$t(\nu)$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{4.26794pt}{34.14365pt}\pgfsys@lineto{7.59016pt}{30.09268pt}\pgfsys@moveto{14.49593pt}{20.79001pt}\pgfsys@lineto{19.41765pt}{13.444pt}\pgfsys@moveto{26.50558pt}{4.0124pt}\pgfsys@lineto{29.87569pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{4.26794pt}{0.0pt}\pgfsys@lineto{9.73848pt}{20.01363pt}\pgfsys@moveto{12.83131pt}{31.19293pt}\pgfsys@lineto{13.6575pt}{34.14365pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{20.48613pt}{0.0pt}\pgfsys@lineto{21.21927pt}{2.81842pt}\pgfsys@moveto{24.29868pt}{14.2249pt}\pgfsys@lineto{29.87569pt}{34.14365pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\simeq\text{ \leavevmode\hbox to57.31pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{25.78658pt}{14.22638pt}\pgfsys@curveto{25.78658pt}{20.61098pt}{20.61098pt}{25.78658pt}{14.22638pt}{25.78658pt}\pgfsys@curveto{7.84178pt}{25.78658pt}{2.66618pt}{20.61098pt}{2.66618pt}{14.22638pt}\pgfsys@curveto{2.66618pt}{7.84178pt}{7.84178pt}{2.66618pt}{14.22638pt}{2.66618pt}\pgfsys@curveto{20.61098pt}{2.66618pt}{25.78658pt}{7.84178pt}{25.78658pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{3.64822pt}{12.4764pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p(t(\mu))$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{53.8837pt}{14.22638pt}\pgfsys@curveto{53.8837pt}{20.41457pt}{48.86732pt}{25.43094pt}{42.67914pt}{25.43094pt}\pgfsys@curveto{36.49095pt}{25.43094pt}{31.47458pt}{20.41457pt}{31.47458pt}{14.22638pt}\pgfsys@curveto{31.47458pt}{8.0382pt}{36.49095pt}{3.02182pt}{42.67914pt}{3.02182pt}\pgfsys@curveto{48.86732pt}{3.02182pt}{53.8837pt}{8.0382pt}{53.8837pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{42.67914pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{32.48097pt}{12.4764pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p(t(\nu))$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{0.0pt}{14.22638pt}\pgfsys@lineto{2.5262pt}{14.22638pt}\pgfsys@moveto{25.92657pt}{14.22638pt}\pgfsys@lineto{31.3346pt}{14.22638pt}\pgfsys@moveto{54.02371pt}{14.22638pt}\pgfsys@lineto{56.90552pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{14.22638pt}{0.0pt}\pgfsys@lineto{14.22638pt}{2.5262pt}\pgfsys@moveto{14.22638pt}{25.92657pt}\pgfsys@lineto{14.22638pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{42.67914pt}{0.0pt}\pgfsys@lineto{42.67914pt}{2.88184pt}\pgfsys@moveto{42.67914pt}{25.57094pt}\pgfsys@lineto{42.67914pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\simeq\text{ \leavevmode\hbox to57.31pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{19.40218pt}{14.22638pt}\pgfsys@curveto{19.40218pt}{17.08492pt}{17.08492pt}{19.40218pt}{14.22638pt}{19.40218pt}\pgfsys@curveto{11.36784pt}{19.40218pt}{9.05058pt}{17.08492pt}{9.05058pt}{14.22638pt}\pgfsys@curveto{9.05058pt}{11.36784pt}{11.36784pt}{9.05058pt}{14.22638pt}{9.05058pt}\pgfsys@curveto{17.08492pt}{9.05058pt}{19.40218pt}{11.36784pt}{19.40218pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{11.81618pt}{13.28194pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mu$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{47.5485pt}{14.22638pt}\pgfsys@curveto{47.5485pt}{16.91568pt}{45.36844pt}{19.09573pt}{42.67914pt}{19.09573pt}\pgfsys@curveto{39.98984pt}{19.09573pt}{37.80978pt}{16.91568pt}{37.80978pt}{14.22638pt}\pgfsys@curveto{37.80978pt}{11.53708pt}{39.98984pt}{9.35703pt}{42.67914pt}{9.35703pt}\pgfsys@curveto{45.36844pt}{9.35703pt}{47.5485pt}{11.53708pt}{47.5485pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{42.67914pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{40.70322pt}{12.50417pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\nu$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{0.0pt}{14.22638pt}\pgfsys@lineto{8.8906pt}{14.22638pt}\pgfsys@moveto{19.56216pt}{14.22638pt}\pgfsys@lineto{37.64981pt}{14.22638pt}\pgfsys@moveto{47.7085pt}{14.22638pt}\pgfsys@lineto{56.90552pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{14.22638pt}{0.0pt}\pgfsys@lineto{14.22638pt}{8.8906pt}\pgfsys@moveto{14.22638pt}{19.56218pt}\pgfsys@lineto{14.22638pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{42.67914pt}{0.0pt}\pgfsys@lineto{42.67914pt}{9.19704pt}\pgfsys@moveto{42.67914pt}{19.25574pt}\pgfsys@lineto{42.67914pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }$$

$$\mapsto$$

Full text

Introduction

The combinatorial structure of double categories has attracted a lot of attention since the notion was introduced by Ehresmann [1963]. Informally, one can describe double categories by the shape of their string diagrams. Unlike 2-categories where the edges are required to flow along a specified direction (usually vertically), 2-cells in double categories can connect to both horizontal and vertical wires. Therefore they not only have a vertical domain and codomain, but also a horizontal domain and codomain. These definitions are made precise in Section 1.

At a first glance, double categories could be considered a more natural categorical axiomatization of planar systems, since they treat the two dimensions of the plane in a dual, interchangeable way. In comparison, the vertical and horizontal compositions in 2-categories are intrisically different, forcing diagrams to flow in a specified direction. However, this uniform behaviour in two dimensions comes at a cost known as the pinwheel problem. Concretely, this problem manifests itself in the fact that not all planar arrangements of 2-cells can be composed, even if all local compatibility conditions are satisfied. For a diagram to be interpreted as a 2-cell it must be binary composable and this can fail if the diagram contains a so-called pinwheel, represented later in Figure 2.

A lot of work has already been dedicated to characterizing which arrangements of 2-cells can be composed in a double category, using order-theoretic representations of these arragements [Dawson and Paré, 1993; Dawson, 1995]. In this work, we focus instead on the word problem for 2-cells in double categories. Given two binary composable diagrams, we want to determine whether they represent the same 2-cell or not. Dawson et al. [2004] have studied this problem in the case of free extensions of double categories, showing for instance that the word problem can become undecidable with the addition of a single free 2-cell.

We study the word problem for free double categories, meaning that no equations are imposed on the generators. The only equations relating expressions in this context are the axioms of double categories. We introduce a correspondence between a free double category and a free 2-category, for which the word problem is solved [Delpeuch and Vicary, 2018]. We obtain as a result a quadratic time algorithm to determine if two double category diagrams are equivalent (Theorem 1).

It might be worth explaining why this word problem is of interest. Word problems have not attracted much attention in category theory so far, perhaps because they are wrongly seen as computational problems of little relevance to mathematics. In fact, studying the word problem for an algebraic structure often surfaces profound algebraic properties of that structure, and is key to understanding its combinatorics. For instance, Squier [1987] established a correspondence between the existence of a convergent presentation for a monoid and its homological type. Group theory in another example: the notion of automatic group [Epstein et al., 1992] was originally motivated by computational properties, but turned out to have a simple characterization in terms of Cayley graphs (ibid.). It has found fruitful applications to the braid group [Charney, 1992] and mapping class groups in general [Mosher, 1995], among others.

Our solution to the word problem for double categories relies on a reduction to the word problem for 2-categories. Here again, the translation used is of its own interest, as it establishes a tight relation between the combinatorics of 2-categories and that of double categories. In fact, we will argue in Section 6 that free 2-categories should be preferred to free double categories, as they are simpler, equally expressive and do not suffer from the pinwheel problem.

The idea of the correspondence is very simple. In order to simulate the horizontal wires of a double category in a 2-category, we simply “rotate the string diagrams by $\frac{\pi}{4}$”. In Section 3, we make this correspondence precise and show that it respects the notions of equivalences on both structures. This lets us solve the word problem for free double categories in Section 5.

\alpha$$\xmapsto{t}$$\alpha

This correspondence between free double categories and free 2-categories is motivated by the word problem but is of interest in its own right: it shows that one does not gain much by considering a free double category instead of the corresponding free 2-category. Reasoning in a 2-category avoids the pinwheel problem entirely as the validity of a string diagram in this structure can be checked locally. Section 6 shows how the translation could be extended to diagrams which include pinwheels, giving them a meaning in the free 2-category. This has also practical implications: one can use the translation to reason about double categories in proof assistants such as homotopy.io [Heidemann et al., 2019] which use a globular notion of n-category.

Acknowledgements

We thank Jamie Vicary, Jules Hedges, Robert Paré, Dorette Pronk and the anonymous reviewer for their feedback on this work. The author is supported by an EPSRC studentship.

1 Double categories

Definition 1.1**.**

Let $\mathcal{C}$ be a category. An internal category in $\mathcal{C}$ consists of the following data:

• •

a pair of objects $M,O$, that we think of as the sets of morphisms and objects

• •

morphisms $d,c\in\mathcal{C}(M,O)$, intuitively the domain and codomain functions

• •

a morphism $\iota\in\mathcal{C}(O,M)$, taking an object to its identity map;

• •

a morphism $\mu\in\mathcal{C}(P,M)$, where $P$ is the pullback (which is therefore required to exist) of $M\xrightarrow{d}O\xleftarrow{c}M$. This represents the multiplication of compatible pairs of morphisms.

These morphisms are required to satisfy equalities, which correspond to the axioms of a category (associativity and unitality of composition, as well as equations for the domains and codomains of identities and composites).

The definition above is chosen such that an internal category in $\mathbf{Set}$ is a small category. The purpose of this concept is that its generality makes it possible to interpret it in other categories.

Definition 1.2**.**

A double category is an internal category in $\mathbf{Cat}$, the category of small categories.

This definition is concise and this conciseness justifies the interest in this structure, which was originally introduced by Ehresmann [1963]. However, it is of little help to build intuition about the nature of such an object, so let us unfold its content. A double category consists of an object category $\mathcal{O}$ and a morphisms category $\mathcal{M}$, with functors $D,C:\mathcal{M}\rightarrow\mathcal{O}$, $I:\mathcal{O}\rightarrow\mathcal{M}$ and $M:\mathcal{P}\rightarrow\mathcal{M}$ where $\mathcal{P}$ is defined as above. We will call

• •

objects of $\mathcal{O}$ as objects of the double category;

• •

morphisms of $\mathcal{O}$ as vertical morphisms of the double category;

• •

objects of $\mathcal{M}$ as horizontal morphisms of the double category;

• •

morphisms of $\mathcal{M}$ as 2-cells of the double category.

Initially, it can seem confusing that objects of $\mathcal{M}$ are thought of as morphisms. The reason for this is that by forgetting morphisms, i.e. taking the image of our internal category via the forgetful functor $\mathbf{Cat}\rightarrow\mathbf{Set}$, we obtain an internal category in $\mathbf{Set}$, i.e. a small category. We will call this the horizontal category of the double category. As its morphisms are the objects of $\mathcal{M}$, this justifies their name. These horizontal morphisms have as domains and codomains objects of $\mathcal{O}$. These objects are also involved in another category, namely $\mathcal{O}$ itself, that we will call the vertical category of the double category.

Any 2-cell $\alpha$ has two horizontal morphisms as domain and codomain, $\text{dom}_{\mathcal{M}}(\alpha)$ and $\text{cod}_{\mathcal{M}}(\alpha)$ as a morphism of $\mathcal{M}$. We will call these the horizontal domain and codomain of $\alpha$. Furthermore, it is associated by the internal category structure to $D(\alpha)$ and $C(\alpha)$, which are vertical morphisms. We will therefore call these the vertical domain and codomain of $\alpha$. Finally, the functoriality of $D$ and $C$ ensures that for instance $D(\operatorname{dom}_{\mathcal{M}}(\alpha))=\operatorname{dom}_{\mathcal{O}}(D(\alpha))$ and similarly for $C$ and $\operatorname{cod}$. This suggests the representation of $\alpha$ as a square:

Although this diagram is similar to commutative diagrams used in category theory, we stress that it is here used in a more general sense, as composing horizontal and vertical morphisms does not make sense in general.

The 2-cells in a double category can be composed in two different ways. First, as morphisms of $\mathcal{M}$, two 2-cells can be composed if they have compatible horizontal domain and codomain. We call this the vertical composition. Second, the functor $M$ defines a composition for 2-cells with compatible vertical domains and codomain, and we call this the horizontal composition. These compositions can be represented with diagrams:

The functoriality of $M$ ensures that these two compositions are compatible: $(\alpha\star\delta)\circ(\beta\star\gamma)=(\alpha\circ\beta)\star(\delta\circ\gamma)$ for all 2-cells such that both sides of the equation are defined. This means that the following diagram is unambiguous:

[TABLE]

Given that the horizontal and vertical compositions are also associative, it is natural to represent composite 2-cells as tilings of rectangles in the plane, with the appropriate conditions on edges to ensure compatibility between the composed 2-cells. Dawson and Pare [1993] have shown that if there are two ways to interpret such a tiling as a tree of horizontal and vertical compositions, then the resulting 2-cells will be equal. However, there exist tilings which satisfy the local compatibility conditions but do not arise from the horizontal and vertical compositions. The minimal example of this is known as the pinwheel and is shown in Figure 2.

It was then shown by Dawson [1995] that this is essentially the only obstacle to composition of diagrams in double categories.

2 Free double categories

Double categories are rich objects and defining them therefore requires some care. Given horizontal and vertical categories with the same objects, and a set of generating tiles whose boundaries are chosen from the horizontal and vertical categories, we want to generate the free double category on these tiles.

One simple approach to generate such a double category would be to use its definition as internal category object in $\mathbf{Cat}$, and simply internalize the definition of a free category on a graph. A graph object in $\mathbf{Cat}$ is called a double graph and is essentially a double category without identities and compositions. Interpreted in $\mathbf{Cat}$, the construction which defines a free category object from a graph object does give a double category, but as pointed out by Dawson and Paré [2002] this imposes important restrictions on the boundaries of the generating tiles: they must be generating morphisms of the resulting vertical and horizontal categories. Therefore, all generated composites have a grid-like shape:

Dawson and Paré [2002] propose a more general construction which allows identities as cell boundaries. To do so they use the notion of reflexive graph: it is a directed graph with designated loops on each vertex. One can define the free category generated by a reflexive graph, where the loops are interpreted as identities. Internalized in $\mathbf{Cat}$, this gives rise to the notion of double reflexive graph which generates a double category. This makes it possible to use generators which have identities as boundaries:

As this is still not as general as it could be, Fiore et al. [2008] introduces the notion of double derivation scheme. A double derivation scheme is a double graph whose horizontal and vertical objects form categories. Therefore, generating a double category from a double derivation scheme makes it possible to use arbitrary boundaries for the generating cells. The main difference with the previous approaches is that the notion of double derivation scheme does not arise by internalizing in $\mathbf{Cat}$ a notion formulated in the internal language of categories. Moreover a double derivation scheme can also introduce algebraic equations between expressions, quotienting the generated structure accordingly. In our case, no such equations are used, so we give a simpler description of the construction.

Definition 2.1**.**

A double signature $S=(A,H,V,C)$ is given by:

• •

a set of objects $A$;

• •

a set of generating horizontal morphisms $H$;

• •

a set of generating vertical morphisms $V$;

• •

a set of generating 2-cells $C$.

Furthermore each $h\in H$ is associated with $\operatorname{dom}h,\operatorname{cod}h\in A$ and similarly for $V$. This defines free categories $H^{*}$ and $V^{*}$. Each $\alpha\in C$ is associated with compatible vertical and horizontal domains and codomains $\operatorname{domh}\alpha,\operatorname{codh}\alpha\in H^{*}$ and $\operatorname{domv}\alpha,\operatorname{codv}\alpha\in V^{*}$. The required compatibility is $\operatorname{dom}\operatorname{domh}\alpha=\operatorname{dom}\operatorname{domv}\alpha$ and three other similar equations.

The set of 2-cells of the double category generated by this data is generated inductively from the generators in $C$, vertical and horizontal identities. From these generators we take the closure by vertical and horizontal composition of compatible cells: this gives us the set of 2-cell expressions on the signature. To obtain the set of 2-cells, we quotient by unitality and associativity of the vertical and horizontal compositions and by the exchange law. Furthermore, horizontal and vertical identities on identity morphisms (depicted as empty 2-cells) are equated. These are precisely the laws of double categories, hence this defines the free double category $S_{d}$ on the given data.

Expressions in double categories can be drawn as string diagrams [Myers, 2016], and in the sequel we will use the terms “expression” and “diagram” interchangeably. Here is an example of a series of equivalences between expressions of 2-cells, drawn as string diagrams:

[TABLE]

We draw horizontal wires in red, this will help us to to distinguish them from vertical wires in the next section. We also ommit region colors as they are irrelevant for equivalences and do not play any role in the word problem.

Our goal in this work is to propose an alternate representation for 2-cells, making it possible to decide whether two expressions of 2-cells are equivalent under these axioms.

3 Translation to 2-categories

Double categories can be seen as a generalization of 2-categories, as a 2-category is a double category where all vertical morphisms are identities. Given the inherent duality in double categories, a 2-category can also be seen as a double category with identity horizontal morphisms.

In this section, we show how a free double category can conversely give rise to a free 2-category. Our goal is to reuse known algorithms for the word problem in 2-categories [Delpeuch and Vicary, 2018] for double categories. To that end we use the string diagram calculus for 2-categories [Selinger, 2011].

Definition 3.1**.**

Given a double signature $S=(A,H,V,C)$, we define the 2-category $S_{2}$ as the free 2-category generated by:

• •

objects $a\in A$;

• •

1-morphisms $h:\operatorname{dom}h\rightarrow\operatorname{cod}h$ for $h\in H$ and $v^{\text{op}}:\operatorname{cod}v\rightarrow\operatorname{dom}v$ for $v\in H$;

• •

2-morphisms $\alpha:\operatorname{domh}\alpha\circ(\operatorname{domv}\alpha)^{\text{op}}\rightarrow(\operatorname{codv}\alpha)^{\text{op}}\circ\operatorname{codh}\alpha$

Note that the vertical generators are reversed in the 2-category, making it possible to compose the horizontal and vertical domains together, and similarly for the codomain.

Definition 3.2**.**

Let $\phi$ be a 2-cell expression in $S_{d}$. We inductively define its translation $t(\phi)$ as a morphism in $S_{2}(\operatorname{domh}\phi\circ(\operatorname{domv}\phi)^{\text{op}},(\operatorname{codv}\phi)^{\text{op}}\circ\operatorname{codh}\phi)$:

[TABLE]

Lemma 3.3**.**

The translation $t$ respects the axioms of double categories, i.e. it extends to a map from 2-cells in $S_{d}$ to 2-cells in $S_{2}$.

Proof 3.4**.**

One can check that unitality and associativity are respected. The exchange law in double categories translates to the exchange law in 2-categories:

\mu$$\nu$$\alpha$$\beta$$\mapsto$$\mapsto$$\simeq$$\mu$$\alpha$$\nu$$\beta$$\mu$$\alpha$$\nu$$\beta

Our goal is to show the converse: if the translations of two expressions in $S_{d}$ are equivalent as morphisms in $S_{2}$, then so are their antecedents in $S_{d}$. To do so, we need to construct a reverse translation, from diagrams in the free 2-category to diagrams in the free double category.

4 Partial tilings

To provide an inverse to the translation $t$, let us first introduce a necessary condition on a diagram in $S_{2}$ to be in the image of $t$.

Definition 4.1**.**

A diagram $\phi\in S_{2}$ is admissible if its domain is of the form $v^{\text{op}};h$ and its codomain is of the form $h^{\prime};v^{\prime\text{op}}$.

For all $\psi\in S_{d}$, $t(\psi)$ is admissible. Conversely, for all admissible $\phi\in S_{2}$, we want to construct a corresponding tiling. To do so, we introduce the notion of partial tiling as an incomplete diagram in the free double category.

Definition 4.2**.**

Let $n\geq 1$, and $h,h_{1},\dots,h_{n}\in H^{*}$ and $v,v_{1},\dots,v_{n}\in V^{*}$. Assume that $h_{i}$ is not an identity for $i>1$ and $v_{i}$ is not an identity for $i<n$.

A partial tiling of type $h,v\rightarrow h_{1},v_{1},\dots,h_{n},v_{n}$ is a subdivision of the following shape into rectangles:

[TABLE]

Each of the rectangles in the subdivision is attributed a generator $\alpha\in C$ or a vertical or horizontal identity, such that the horizontal and vertical domains and codomains match on each edge.

We think of a partial tiling as some upper-left corner of a 2-cell in a double category. We will therefore draw partial tilings just like string diagrams for double categories, as in Figure 3.

Definition 4.3**.**

Two partial tilings are equivalent when they can be related by a series of applications of these rules (where $\alpha$ can be an identity itself):

\alpha$$\simeq$$\alpha$$\simeq$$\alpha$$\alpha$$\simeq$$\alpha$$\simeq$$\alpha

as well as continuous translations of horizontal or vertical boundaries in the subdivision. We denote this equivalence by $\simeq$.

For instance, the two partial tilings in Figure 3 are equivalent.

In the special case where $n=2$, $h_{1}$ and $v_{2}$ are identities and $h=h_{2}$, $v=v_{2}$, and assuming $\operatorname{dom}h=\operatorname{dom}v$, there is an empty partial tiling of type $h,v\rightarrow 1_{\operatorname{cod}v},v,h,1_{\operatorname{cod}h}$:

[TABLE]

Another special case are partial tilings of type $h,v\rightarrow h_{1},v_{1}$ which have a rectangular shape. In this case, we can interpret them as 2-cells, but only if they are binary composable.

Lemma 4.4**.**

A partial tiling of type $h,v\rightarrow h_{1},v_{1}$ is binary composable if it can be obtained by repeated application of the horizontal and vertical composition from generators. In this case, it represents a 2-cell in $S_{d}$, and its meaning is invariant under equivalence of partial tilings.

Proof 4.5**.**

If a diagram is binary composable then by the general associativity result of Dawson and Pare [1993], it can be interpreted as a 2-cell in $S_{d}$ which does not depend on the order of composition chosen. Then, equivalences of partial tilings correspond to unitality of identities when interpreted in a binary composable diagram, so the 2-cell is invariant under these equivalences.

Definition 4.6**.**

Let $h$ be an horizontal morphism in $S_{d}$. It can be uniquely decomposed as a composition of generators $h=h_{1}\circ\dots\circ h_{k}$. We define the length of $h$ as $|h|=k$. Let $0\leq i<k$ and $1\leq j<k$. We say that $h^{\prime}=h_{i+1}\circ\dots\circ h_{j}$ is a factor at index $i$ of $h$. Similar notions are defined for vertical morphisms.

For instance, the factors at index [math] of a morphism $h$ are its prefixes.

Definition 4.7**.**

Let $m$ be a partial tiling of type $h,v\rightarrow h_{1},v_{1},\dots,h_{n},v_{n}$ and let $\alpha:h^{\prime},v^{\prime}\rightarrow h^{\prime\prime},v^{\prime\prime}$ be a generator. A gluing position of $\alpha$ on $m$ is one of the following:

• •

if $h^{\prime}$ is a prefix of $h_{1}$, then $(0,0,0)$ is a gluing position;

• •

if $h^{\prime}$ is a factor of $h_{1}$ at index $i>0$ and $v^{\prime}$ is an identity, then $(0,i,0)$ is a gluing position;

• •

if $v^{\prime}$ is a prefix of $v_{n}$, then $(n,0,0)$ is a gluing position;

• •

if $v^{\prime}$ is a factor of $v_{n}$ at index $i>0$ and $h^{\prime}$ is an identity, then $(n,0,i)$ is a gluing position;

Furthermore, for all $1\leq k<n$:

• •

if $v^{\prime}$ is a prefix of $v_{k}$ and $h^{\prime}$ is a prefix of $h_{k+1}$, then $(k,0,0)$ is a gluing position;

• •

if $v^{\prime}$ is a factor of $v_{k}$ at index $i$ and $h^{\prime}$ is an identity, then $(k,0,i)$ is a gluing position;

• •

if $h^{\prime}$ is a factor of $h_{k+1}$ at index $i$ and $v^{\prime}$ is an identity, then $(k,i,0)$ is a gluing position.

For each gluing position $p$ we define the gluing of $\alpha$ to $m$, denoted by $m\star_{p}\alpha$, by the partial tiling obtained by adjoining $\alpha$ at the designated position, and adding any necessary identity to satisfy the condition of Definition 4.2.

Figure 4 shows all the possible gluing positions. Figure 5 shows how a generator can be glued at multiple positions on a partial tiling and how identities can be used to ensure that the resulting arrangement has non-identity inner boundaries.

Definition 4.8**.**

Let $\phi$ be a diagram in the free 2-category $S_{2}$. We assume that the domain of $\phi$ is of the form $v^{\text{op}};h$ with $v$ and $h$ paths of generators from $S$.

Let $l\in\mathbb{N}$ be a level in $\phi$ and $h_{1};v_{1}^{\text{op}};\dots;h_{n};v_{n}^{\text{op}}$ be the type of the diagram at this height, where $v_{1}$ and $h_{n}$ can possibly be identities unlike the others elements of the sequence.

We associate to this data a partial tiling $p_{k}(\phi):h,v\rightarrow h_{1},v_{1},\dots,h_{n},v_{n}$, by induction on $k$. If $k=0$, $p_{k}(\phi)$ is the empty partial tiling of type $v,h\rightarrow 1,v,h,1$. Otherwise, let $\alpha$ be the generator between levels $k-1$ and $k$. We define $p_{k}(\phi)$ as the gluing of $\alpha$ on $p_{k-1}(\phi)$ at the position indicated by the connection of $\alpha$ to the level $k-1$ of $\phi$.

Finally we define $p(\phi)$ as $p_{f}(\phi)$ for $f$ the final level of $\phi$.

The construction relies on the following two lemmas:

Lemma 4.9**.**

Let $\alpha$ be the generator between slices $k$ and $k+1$ in $\phi$, a diagram in $S_{2}$. If $\alpha$ has at least one input wire, this determines a unique gluing position $g$ of $\alpha$ on $p_{k}(\phi)$.

Proof 4.10**.**

Each wire crossing level $k$ in $\phi$ corresponds to an open wire on the boundary of $p_{k}(\phi)$, either in a vertical or horizontal boundary depending on the colour of the wire.

Let $v^{\text{op}};h$ be the domain of $\alpha$.

By assumption, at least one of $v,h$ is not an identity. Assume first that $v$ is not an identity. As no horizontal inner boundaries of $p_{k}(\phi)$ are identities, as required by Definition 4.2, any contiguous sequence of red wires in $\phi$ corresponds to a contiguous sequence of wires on some vertical boundary $v_{i}$ of $p_{k}(\phi)$.

Let $j$ be such that $v$ is a factor at index $j$ in $v_{i}$. One can then check that $(i,0,j)$ is a valid gluing position for $\alpha$ on $p_{k}(\phi)$.

Similarly, if $h$ is not an identity, then the corresponding wires in $\phi$ determine a unique occurrence of $h$ in a vertical boundary $h_{i}$ of $p_{k}(\phi)$, and by denoting by $j$ the index of $h$ in $h_{i}$, this determines the gluing position $(i-1,j,0)$.

Lemma 4.11**.**

Let again $\alpha$ be the generator between slices $h$ and $h+1$ in $\phi$, a diagram in $S_{2}$. If $\alpha$ has no input wire, meaning that its domain is the identity, then this determines either one or two gluing positions of $\alpha$ on $p_{h}(\phi)$. If there are two such positions $l,l^{\prime}$ then $p_{h}(\phi)\star_{l}\alpha\simeq p_{h}(\phi)\star_{l^{\prime}}\alpha$.

Proof 4.12**.**

Let $h_{1};v_{1}^{\text{op}};\dots;h_{n};v_{n}^{\text{op}}$ be the type of the diagram at height $h$. Again, each wire in this sequence corresponds to an open wire on the boundary of $p_{k}(\phi)$. The wires passing to the left of $\alpha$ in $\phi$ determine a position in this sequence where the generator $\alpha$ is inserted. The gluing positions depend on this position.

If $\alpha$ is bordered by two horizontal wires on each side (respectively two vertical wires), this determines a unique gluing position $(k,i,0)$ (respectively $(k,0,i)$) as in the previous lemma. Similarly, if $\alpha$ neighbours a vertical wire on its left and a horizontal wire on its right, this determines a unique gluing position $(k,0,0)$ as in the previous lemma.

The remaining cases are when $\alpha$ neighbours a horizontal wire on its left and a vertical wire on its right, when $\alpha$ does not have any wire on its left and a vertical one on its right, when it has a horizontal wire on its left and none on its right, or when there are no wires neither on the left or the right of $\alpha$. In this case this determines two gluing positions $l=(k,i,0)$ and $l^{\prime}=(k+1,0,j)$, and Figure 6 shows how $p_{h}(\phi)\star_{l}\alpha\simeq p_{h}(\phi)\star_{l^{\prime}}\alpha$ in this case.

Lemma 4.13**.**

For all 2-cell diagrams $\mu,\nu\in S_{2}$ such that
\mu$$\nu is defined, p(\text{ \leavevmode\hbox to28.85pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{13.91823pt}{21.33957pt}\pgfsys@curveto{13.91823pt}{23.84077pt}{11.89066pt}{25.86835pt}{9.38945pt}{25.86835pt}\pgfsys@curveto{6.88824pt}{25.86835pt}{4.86067pt}{23.84077pt}{4.86067pt}{21.33957pt}\pgfsys@curveto{4.86067pt}{18.83836pt}{6.88824pt}{16.81079pt}{9.38945pt}{16.81079pt}\pgfsys@curveto{11.89066pt}{16.81079pt}{13.91823pt}{18.83836pt}{13.91823pt}{21.33957pt}\pgfsys@closepath\pgfsys@moveto{9.38945pt}{21.33957pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{7.28055pt}{20.51318pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\mu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{23.18173pt}{7.11319pt}\pgfsys@curveto{23.18173pt}{9.4663pt}{21.2742pt}{11.37383pt}{18.9211pt}{11.37383pt}\pgfsys@curveto{16.568pt}{11.37383pt}{14.66046pt}{9.4663pt}{14.66046pt}{7.11319pt}\pgfsys@curveto{14.66046pt}{4.76009pt}{16.568pt}{2.85255pt}{18.9211pt}{2.85255pt}\pgfsys@curveto{21.2742pt}{2.85255pt}{23.18173pt}{4.76009pt}{23.18173pt}{7.11319pt}\pgfsys@closepath\pgfsys@moveto{18.9211pt}{7.11319pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{17.19217pt}{5.60626pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\nu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{3.5566pt}{28.45276pt}\pgfsys@lineto{6.4291pt}{24.94978pt}\pgfsys@moveto{11.98814pt}{17.46092pt}\pgfsys@lineto{16.4716pt}{10.76909pt}\pgfsys@moveto{21.75153pt}{3.74356pt}\pgfsys@lineto{24.89616pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{3.5566pt}{0.0pt}\pgfsys@lineto{8.1585pt}{16.83601pt}\pgfsys@moveto{10.64825pt}{25.83545pt}\pgfsys@lineto{11.38113pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{17.07161pt}{0.0pt}\pgfsys@lineto{17.81375pt}{2.85417pt}\pgfsys@moveto{20.1076pt}{11.35086pt}\pgfsys@lineto{24.89616pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\simeq\text{ \leavevmode\hbox to57.31pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{28.45276pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{23.83656pt}{14.22638pt}\pgfsys@curveto{23.83656pt}{19.534pt}{19.534pt}{23.83656pt}{14.22638pt}{23.83656pt}\pgfsys@curveto{8.91876pt}{23.83656pt}{4.6162pt}{19.534pt}{4.6162pt}{14.22638pt}\pgfsys@curveto{4.6162pt}{8.91876pt}{8.91876pt}{4.6162pt}{14.22638pt}{4.6162pt}\pgfsys@curveto{19.534pt}{4.6162pt}{23.83656pt}{8.91876pt}{23.83656pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{6.69255pt}{12.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\mu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{52.47018pt}{14.22638pt}\pgfsys@curveto{52.47018pt}{19.63388pt}{48.08664pt}{24.01743pt}{42.67914pt}{24.01743pt}\pgfsys@curveto{37.27164pt}{24.01743pt}{32.88809pt}{19.63388pt}{32.88809pt}{14.22638pt}\pgfsys@curveto{32.88809pt}{8.81888pt}{37.27164pt}{4.43533pt}{42.67914pt}{4.43533pt}\pgfsys@curveto{48.08664pt}{4.43533pt}{52.47018pt}{8.81888pt}{52.47018pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{42.67914pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{35.57957pt}{12.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\nu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{0.0pt}{14.22638pt}\pgfsys@lineto{4.4562pt}{14.22638pt}\pgfsys@moveto{23.99658pt}{14.22638pt}\pgfsys@lineto{32.7281pt}{14.22638pt}\pgfsys@moveto{52.63019pt}{14.22638pt}\pgfsys@lineto{56.90552pt}{14.22638pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{14.22638pt}{0.0pt}\pgfsys@lineto{14.22638pt}{4.4562pt}\pgfsys@moveto{14.22638pt}{23.99657pt}\pgfsys@lineto{14.22638pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{42.67914pt}{0.0pt}\pgfsys@lineto{42.67914pt}{4.27534pt}\pgfsys@moveto{42.67914pt}{24.17743pt}\pgfsys@lineto{42.67914pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }.

Similarly, if
\mu$$\nu is defined, then p(\text{ \leavevmode\hbox to28.85pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{13.91823pt}{21.33957pt}\pgfsys@curveto{13.91823pt}{23.84077pt}{11.89066pt}{25.86835pt}{9.38945pt}{25.86835pt}\pgfsys@curveto{6.88824pt}{25.86835pt}{4.86067pt}{23.84077pt}{4.86067pt}{21.33957pt}\pgfsys@curveto{4.86067pt}{18.83836pt}{6.88824pt}{16.81079pt}{9.38945pt}{16.81079pt}\pgfsys@curveto{11.89066pt}{16.81079pt}{13.91823pt}{18.83836pt}{13.91823pt}{21.33957pt}\pgfsys@closepath\pgfsys@moveto{9.38945pt}{21.33957pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{7.28055pt}{20.51318pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\mu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{23.18173pt}{7.11319pt}\pgfsys@curveto{23.18173pt}{9.4663pt}{21.2742pt}{11.37383pt}{18.9211pt}{11.37383pt}\pgfsys@curveto{16.568pt}{11.37383pt}{14.66046pt}{9.4663pt}{14.66046pt}{7.11319pt}\pgfsys@curveto{14.66046pt}{4.76009pt}{16.568pt}{2.85255pt}{18.9211pt}{2.85255pt}\pgfsys@curveto{21.2742pt}{2.85255pt}{23.18173pt}{4.76009pt}{23.18173pt}{7.11319pt}\pgfsys@closepath\pgfsys@moveto{18.9211pt}{7.11319pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{17.19217pt}{5.60626pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\nu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{3.5566pt}{28.45276pt}\pgfsys@lineto{6.4291pt}{24.94978pt}\pgfsys@moveto{11.98814pt}{17.46092pt}\pgfsys@lineto{16.4716pt}{10.76909pt}\pgfsys@moveto{21.75153pt}{3.74356pt}\pgfsys@lineto{24.89616pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{3.5566pt}{0.0pt}\pgfsys@lineto{8.1585pt}{16.83601pt}\pgfsys@moveto{10.64825pt}{25.83545pt}\pgfsys@lineto{11.38113pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{17.07161pt}{0.0pt}\pgfsys@lineto{17.81375pt}{2.85417pt}\pgfsys@moveto{20.1076pt}{11.35086pt}\pgfsys@lineto{24.89616pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\simeq\text{ \leavevmode\hbox to28.85pt{\vbox to57.31pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-14.42638pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} \pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{28.45276pt}{-14.22638pt}\pgfsys@moveto{28.45276pt}{-14.22638pt}\pgfsys@lineto{0.0pt}{-14.22638pt}\pgfsys@lineto{0.0pt}{42.67914pt}\pgfsys@lineto{28.45276pt}{42.67914pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{42.67914pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{24.53696pt}{0.0pt}\pgfsys@curveto{24.53696pt}{5.69444pt}{19.92082pt}{10.31058pt}{14.22638pt}{10.31058pt}\pgfsys@curveto{8.53194pt}{10.31058pt}{3.9158pt}{5.69444pt}{3.9158pt}{0.0pt}\pgfsys@curveto{3.9158pt}{-5.69444pt}{8.53194pt}{-10.31058pt}{14.22638pt}{-10.31058pt}\pgfsys@curveto{19.92082pt}{-10.31058pt}{24.53696pt}{-5.69444pt}{24.53696pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{7.12682pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\nu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{24.3893pt}{28.45276pt}\pgfsys@curveto{24.3893pt}{34.06564pt}{19.83926pt}{38.61568pt}{14.22638pt}{38.61568pt}\pgfsys@curveto{8.6135pt}{38.61568pt}{4.06346pt}{34.06564pt}{4.06346pt}{28.45276pt}\pgfsys@curveto{4.06346pt}{22.83987pt}{8.6135pt}{18.28984pt}{14.22638pt}{18.28984pt}\pgfsys@curveto{19.83926pt}{18.28984pt}{24.3893pt}{22.83987pt}{24.3893pt}{28.45276pt}\pgfsys@closepath\pgfsys@moveto{14.22638pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.8}{0.0}{0.0}{0.8}{6.69255pt}{26.45276pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\mu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}{}} {{{{{}}{}{}{}{}{{}}}{}}}{}{}{}{{}{}} {{{{{}}{}{}{}{}{{}}}{}}}{}{{{{{}}{}{}{}{}{{}}}{}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}{}}}{{}}{}{}{}\pgfsys@moveto{14.22638pt}{-14.22638pt}\pgfsys@lineto{14.22638pt}{-10.47057pt}\pgfsys@moveto{14.22638pt}{10.47058pt}\pgfsys@lineto{14.22638pt}{18.12985pt}\pgfsys@moveto{14.22638pt}{38.77568pt}\pgfsys@lineto{14.22638pt}{42.67914pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}{}} {{{{{}}{}{}{}{}{{}}}{}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}{}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@lineto{24.69696pt}{0.0pt}\pgfsys@moveto{3.75581pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}{}} {{{{{}}{}{}{}{}{{}}}{}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}{}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{28.45276pt}{28.45276pt}\pgfsys@lineto{24.54932pt}{28.45276pt}\pgfsys@moveto{3.90347pt}{28.45276pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }.

Proof 4.14**.**

By duality let us prove the result for the first case, horizontal composition. Let \phi=\text{ \leavevmode\hbox to28.85pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{28.45276pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{13.91823pt}{21.33957pt}\pgfsys@curveto{13.91823pt}{23.84077pt}{11.89066pt}{25.86835pt}{9.38945pt}{25.86835pt}\pgfsys@curveto{6.88824pt}{25.86835pt}{4.86067pt}{23.84077pt}{4.86067pt}{21.33957pt}\pgfsys@curveto{4.86067pt}{18.83836pt}{6.88824pt}{16.81079pt}{9.38945pt}{16.81079pt}\pgfsys@curveto{11.89066pt}{16.81079pt}{13.91823pt}{18.83836pt}{13.91823pt}{21.33957pt}\pgfsys@closepath\pgfsys@moveto{9.38945pt}{21.33957pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{7.28055pt}{20.51318pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\mu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{23.18173pt}{7.11319pt}\pgfsys@curveto{23.18173pt}{9.4663pt}{21.2742pt}{11.37383pt}{18.9211pt}{11.37383pt}\pgfsys@curveto{16.568pt}{11.37383pt}{14.66046pt}{9.4663pt}{14.66046pt}{7.11319pt}\pgfsys@curveto{14.66046pt}{4.76009pt}{16.568pt}{2.85255pt}{18.9211pt}{2.85255pt}\pgfsys@curveto{21.2742pt}{2.85255pt}{23.18173pt}{4.76009pt}{23.18173pt}{7.11319pt}\pgfsys@closepath\pgfsys@moveto{18.9211pt}{7.11319pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{17.19217pt}{5.60626pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\nu}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{3.5566pt}{28.45276pt}\pgfsys@lineto{6.4291pt}{24.94978pt}\pgfsys@moveto{11.98814pt}{17.46092pt}\pgfsys@lineto{16.4716pt}{10.76909pt}\pgfsys@moveto{21.75153pt}{3.74356pt}\pgfsys@lineto{24.89616pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{3.5566pt}{0.0pt}\pgfsys@lineto{8.1585pt}{16.83601pt}\pgfsys@moveto{10.64825pt}{25.83545pt}\pgfsys@lineto{11.38113pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{17.07161pt}{0.0pt}\pgfsys@lineto{17.81375pt}{2.85417pt}\pgfsys@moveto{20.1076pt}{11.35086pt}\pgfsys@lineto{24.89616pt}{28.45276pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}. Let $h$ be the level between $\mu$ and $\nu$ in $\phi$.

Assume first that the red edge connecting $\mu$ and $\nu$ is not empty (it is not an identity vertical morphism). Then p_{h}(\phi)=\text{ \leavevmode\hbox to51.62pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 5.89056pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{} {}{} {}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{-5.69057pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{22.76228pt}\pgfsys@lineto{45.52458pt}{22.76228pt}\pgfsys@lineto{45.52458pt}{28.45287pt}\pgfsys@lineto{-5.69057pt}{28.45287pt}\pgfsys@lineto{-5.69057pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{22.76228pt}{0.0pt}\pgfsys@lineto{22.76228pt}{22.76228pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{-5.69057pt}{22.76228pt}\pgfsys@lineto{0.0pt}{22.76228pt}\pgfsys@lineto{0.0pt}{28.45287pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{19.78998pt}{11.38113pt}\pgfsys@curveto{19.78998pt}{16.02527pt}{16.02527pt}{19.78998pt}{11.38113pt}{19.78998pt}\pgfsys@curveto{6.737pt}{19.78998pt}{2.97229pt}{16.02527pt}{2.97229pt}{11.38113pt}\pgfsys@curveto{2.97229pt}{6.737pt}{6.737pt}{2.97229pt}{11.38113pt}{2.97229pt}\pgfsys@curveto{16.02527pt}{2.97229pt}{19.78998pt}{6.737pt}{19.78998pt}{11.38113pt}\pgfsys@closepath\pgfsys@moveto{11.38113pt}{11.38113pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{4.78908pt}{9.63115pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\mu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{-5.69057pt}{11.38113pt}\pgfsys@lineto{2.83229pt}{11.38116pt}\pgfsys@moveto{19.93004pt}{11.38116pt}\pgfsys@lineto{22.76228pt}{11.38113pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{11.38113pt}{28.45287pt}\pgfsys@lineto{11.38116pt}{19.93004pt}\pgfsys@moveto{11.38116pt}{2.8323pt}\pgfsys@lineto{11.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{} {}{}{}\pgfsys@moveto{34.14343pt}{28.45287pt}\pgfsys@lineto{34.14343pt}{22.76228pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and $p(\phi)$ is obtained from $p_{h}(\phi)$ by gluing on it the generators in $\nu$. Since the vertical codomain of $\mu$ passes to the left of $\nu$, these generators are glued on positions $(k,i,j)$ with $k>0$. Performing these gluings on an empty diagram gives $p(\nu)$, so $p(\phi)$ is equivalent to the required double diagram.

If there is no red edge connecting $\mu$ to $\nu$ then p_{h}(\phi)=\text{ \leavevmode\hbox to51.62pt{\vbox to28.85pt{\pgfpicture\makeatletter\hbox{\hskip 5.89056pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{} {}{} {}{} {}{} {}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{-5.69057pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{22.76228pt}\pgfsys@lineto{45.52458pt}{22.76228pt}\pgfsys@lineto{45.52458pt}{28.45287pt}\pgfsys@lineto{-5.69057pt}{28.45287pt}\pgfsys@lineto{-5.69057pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{22.76228pt}{0.0pt}\pgfsys@lineto{22.76228pt}{22.76228pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{22.76228pt}{0.0pt}\pgfsys@lineto{45.52458pt}{0.0pt}\pgfsys@lineto{45.52458pt}{22.76228pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{} {}{} {}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{ }\pgfsys@color@gray@fill{.5}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}{}\pgfsys@moveto{-5.69057pt}{22.76228pt}\pgfsys@lineto{0.0pt}{22.76228pt}\pgfsys@lineto{0.0pt}{28.45287pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{19.78998pt}{11.38113pt}\pgfsys@curveto{19.78998pt}{16.02527pt}{16.02527pt}{19.78998pt}{11.38113pt}{19.78998pt}\pgfsys@curveto{6.737pt}{19.78998pt}{2.97229pt}{16.02527pt}{2.97229pt}{11.38113pt}\pgfsys@curveto{2.97229pt}{6.737pt}{6.737pt}{2.97229pt}{11.38113pt}{2.97229pt}\pgfsys@curveto{16.02527pt}{2.97229pt}{19.78998pt}{6.737pt}{19.78998pt}{11.38113pt}\pgfsys@closepath\pgfsys@moveto{11.38113pt}{11.38113pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7}{0.0}{0.0}{0.7}{4.78908pt}{9.63115pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{p(\mu)}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{}\pgfsys@moveto{-5.69057pt}{11.38113pt}\pgfsys@lineto{2.83229pt}{11.38116pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{}{} {}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{11.38113pt}{28.45287pt}\pgfsys@lineto{11.38116pt}{19.93004pt}\pgfsys@moveto{11.38116pt}{2.8323pt}\pgfsys@lineto{11.38113pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{} {}{}{}\pgfsys@moveto{34.14343pt}{28.45287pt}\pgfsys@lineto{34.14343pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and $p(\phi)$ is obtained from $p_{h}(\phi)$ by gluing the generators in $\nu$ on the second part of its vertical codomain, so it can again be rewritten into the required form by unitality.

Lemma 4.15**.**

For any 2-cell diagram $\phi\in S_{d}$, $p(t(\phi))\simeq\phi$.

Proof 4.16**.**

By induction on $\phi$. If $\phi$ is a generator or the identity, the result holds.

If $\phi$ is a horizontal or vertical composition, then we use Lemma 4.13 and the induction hypothesis of the composed diagrams:

[TABLE]

Lemma 4.17**.**

Let $\phi,\phi^{\prime}$ be admissible diagrams in $S_{2}$ with $\phi\sim\phi^{\prime}$. Then $p(\phi)\simeq p(\phi^{\prime})$.

Proof 4.18**.**

By induction we can assume that $\phi$ and $\phi^{\prime}$ are related by a single exchange, swapping the generators between levels $h-1$, $h$ and $h+1$. Let $\alpha$ be the generator between levels $h-1$ and $h$ and $\beta$ the one between $h$ and $h+1$. It suffices to check that $p_{h-1}(\phi)\star_{l}\alpha\star_{l^{\prime}}\beta\simeq p_{h-1}(\phi)\star_{m}\beta\star_{m^{\prime}}\alpha$ where $l,l^{\prime}$ are the gluing positions for the generators in $\phi$ and $m,m^{\prime}$ are their counterparts in $\phi^{\prime}$. By a tedious case analysis one can check that because the generators at these slices can be exchanged, this ensures that the induced gluing positions are disjoint, such that the equivalence above either holds trivially (the partial tilings being syntactically equal) or via equivalences analogous to those of Figure 6.

5 Word problem

We can use the translation defined in the previous section to solve the word problem for double categories:

Theorem 1**.**

Let $S$ be a double signature. The word problem for 2-cells in the free double category $S_{d}$ can be solved in $O(ve)$, where $v$ is the number of generators in the expressions and $e$ the number of connecting edges between them.

Proof 5.1**.**

Given two diagrams $\phi,\phi^{\prime}$ in $S_{d}$, we can compute their translation $t(\phi),t(\phi^{\prime})$ in linear time. Then, we can check if these diagrams are equivalent as 2-cells in $S_{2}$ using the algorithm of Delpeuch and Vicary [2018], in $O(ve)$. As $p$ is faithful (Lemma 4.17), this determines if $\phi$ and $\phi^{\prime}$ are equivalent in $S_{d}$.

6 Conclusion

We have solved the word problem for free double categories by reducing it to the word problem for free 2-categories.

Interestingly, our translation $p$ from the free 2-category to the free double category works for all admissible diagrams, and admissibility is a simple condition on the domain and codomain. We are not requiring any global condition such as binary composability on the 2-cell. As a consequence, this translation $p$ can produce tilings which are not binary composable.

[TABLE]

It is therefore tempting to extend the forward translation $t$ to double category diagrams which are not binary composable. By the characterization of Dawson [1995] of non-composable diagrams, it is sufficient to translate the two pinwheels: by induction, all diagrams could then be interpreted. However, there could potentially be multiple ways to decompose a diagram as a tree of binary and pinwheel composites, so to define $t$ properly we would need an equivalent of the general associativity result of Dawson and Pare [1993] with pinwheel composition. That would only be possible given an appropriate notion of equivalence, which would amount to developing a notion of “double category with pinwheels”. This does not strike us as a particularly useful notion as it would be rather complicated, with four different composition operators and many axioms to relate their applications, only to represent planar systems.

What this really means is that free 2-categories already provide the appropriate notion of “free double category with pinwheel composites”, in the sense that they capture the desired combinatorics with a much simpler axiomatization.

This fact has been observed at an intuitive level by Reutter and Vicary [2019] who modeled biunitary connections in a 2-category rather than a double category, by using the same rotation. They noticed that biunitaries forming a pinwheel pattern could be composed into a new biunitary. As double categories are not equipped with such a composition, a 2-categorical model provides a more useful representation. Modelling biunitaries in double categories would artificially forbid pinwheel composites which are actually allowed physically. We suspect that other uses of double categories, for instance in computer science [Bruni et al., 2002], could be recast in 2-categories without loss of expressivity, as they do not rely on the exclusion of pinwheel composites.