Varieties of Cubical Sets

Ulrik Buchholtz; Edward Morehouse

arXiv:1701.08189·math.CT·April 20, 2017

Varieties of Cubical Sets

Ulrik Buchholtz, Edward Morehouse

PDF

Open Access

TL;DR

This paper introduces various notions of cubical sets based on algebraic theories, proving their effectiveness in modeling classical homotopy theory and identifying strict test categories where products align with homotopy types.

Contribution

It defines new classes of cubical sets using substructural algebraic theories and establishes their properties as test categories for homotopy modeling.

Findings

01

All defined sites are test categories modeling homotopy theory

02

Some sites are strict test categories with product-homotopy type correspondence

03

Clarifies the algebraic structures underlying cubical sets in homotopy theory

Abstract

We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning that the corresponding presheaf categories of cubical sets model classical homotopy theory. We delineate exactly which ones are even strict test categories, meaning that products of cubical sets correspond to products of homotopy types.

Tables2

Table 1. Table 1: Cubical axioms

Axiom	Lang. req.	Name
$x \lor (y \lor z) = (x \lor y) \lor z$	$(\cdot, \lor)$	$\lor$ -associativity
$0 \lor x = x = x \lor 0$	$(\cdot, \lor)$	$\lor$ -unit
$1 \lor x = 1 = x \lor 1$	$(w, \lor)$	$\lor$ -absorption
$x \lor y = y \lor x$	$(e, \lor)$	$\lor$ -symmetry
$x \lor x = x$	$(ec, \lor)$	$\lor$ -idempotence
$x \land (y \land z) = (x \land y) \land z$	$(\cdot, \land)$	$\land$ -associativity
$1 \land x = x = x \land 1$	$(\cdot, \land)$	$\land$ -unit
$0 \land x = 0 = x \land 0$	$(w, \land)$	$\land$ -absorption
$x \land y = y \land x$	$(e, \land)$	$\land$ -symmetry
$x \land x = x$	$(ec, \land)$	$\land$ -idempotence
$x^{''} = x$	$(\cdot, {}^{'})$	^′-involution
$0^{'} = 1$	$(\cdot, {}^{'})$	^′-computation
$x \land (y \lor z) = (x \land y) \lor (x \land z)$	$(ec, \lor \land)$	distributive law 1
$x \lor (y \land z) = (x \lor y) \land (x \lor z)$	$(ec, \lor \land)$	distributive law 2
$x = x \lor (x \land y) = x \land (x \lor y)$	$(wec, \lor \land)$	lattice-absorption
${(x \lor y)}^{'} = x^{'} \land y^{'}$	$(\cdot, \lor \land^{'})$	de Morgan’s law
$x \land x^{'} \leq y \lor y^{'}$	$(wec, \lor \land^{'})$	Kleene’s law

Table 2. Table 2: Which canonical cube categories ℂ ( a , b ) subscript ℂ 𝑎 𝑏 \mathbb{C}_{(a,b)} are test (t) or even strict test (st) categories. The bottom-right corner refers to the cube categories corresponding to de Morgan, Kleene and boolean algebras.

a $∖$ b	$\cdot$	^′	$\lor$	$\land$	$\lor, \land$	$\lor, \land^{'}$
w	t	t	st	st	st	st
we	t	t	st	st	st	st
wec	st	st	st	st	st	st/st/st

Equations28

A

A

{w, e, c}

{w, e, c}

ε

ε

τ

δ

(0, 1, \lor, \land,^{'})

(0, 1, \lor, \land,^{'})

{\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{8.53592pt}\pgfsys@curveto{0.0pt}{1.87842pt}{0.0pt}{-1.87842pt}{0.0pt}{-8.53592pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{14.22647pt}\pgfsys@lineto{0.0pt}{14.22647pt}\pgfsys@curveto{-3.14284pt}{14.22647pt}{-5.69055pt}{11.67876pt}{-5.69055pt}{8.53592pt}\pgfsys@lineto{-5.69055pt}{8.53592pt}\pgfsys@curveto{-5.69055pt}{5.39308pt}{-3.14284pt}{2.84537pt}{0.0pt}{2.84537pt}\pgfsys@lineto{0.0pt}{2.84537pt}\pgfsys@curveto{3.14284pt}{2.84537pt}{5.69055pt}{5.39308pt}{5.69055pt}{8.53592pt}\pgfsys@lineto{5.69055pt}{8.53592pt}\pgfsys@curveto{5.69055pt}{11.67876pt}{3.14284pt}{14.22647pt}{0.0pt}{14.22647pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{2.84537pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.44728pt}{7.35536pt}\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{\begin{math}{\eta_{i}}\end{math}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{-2.84537pt}\pgfsys@lineto{0.0pt}{-2.84537pt}\pgfsys@curveto{-3.14284pt}{-2.84537pt}{-5.69055pt}{-5.39308pt}{-5.69055pt}{-8.53592pt}\pgfsys@lineto{-5.69055pt}{-8.53592pt}\pgfsys@curveto{-5.69055pt}{-11.67876pt}{-3.14284pt}{-14.22647pt}{0.0pt}{-14.22647pt}\pgfsys@lineto{0.0pt}{-14.22647pt}\pgfsys@curveto{3.14284pt}{-14.22647pt}{5.69055pt}{-11.67876pt}{5.69055pt}{-8.53592pt}\pgfsys@lineto{5.69055pt}{-8.53592pt}\pgfsys@curveto{5.69055pt}{-5.39308pt}{3.14284pt}{-2.84537pt}{0.0pt}{-2.84537pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{-14.22647pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.33159pt}{-10.68869pt}\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{\begin{math}{\varepsilon}\end{math}} }}\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}}\quad=\quad\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}

{\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{8.53592pt}\pgfsys@curveto{0.0pt}{1.87842pt}{0.0pt}{-1.87842pt}{0.0pt}{-8.53592pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{14.22647pt}\pgfsys@lineto{0.0pt}{14.22647pt}\pgfsys@curveto{-3.14284pt}{14.22647pt}{-5.69055pt}{11.67876pt}{-5.69055pt}{8.53592pt}\pgfsys@lineto{-5.69055pt}{8.53592pt}\pgfsys@curveto{-5.69055pt}{5.39308pt}{-3.14284pt}{2.84537pt}{0.0pt}{2.84537pt}\pgfsys@lineto{0.0pt}{2.84537pt}\pgfsys@curveto{3.14284pt}{2.84537pt}{5.69055pt}{5.39308pt}{5.69055pt}{8.53592pt}\pgfsys@lineto{5.69055pt}{8.53592pt}\pgfsys@curveto{5.69055pt}{11.67876pt}{3.14284pt}{14.22647pt}{0.0pt}{14.22647pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{2.84537pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.44728pt}{7.35536pt}\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{\begin{math}{\eta_{i}}\end{math}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{-2.84537pt}\pgfsys@lineto{0.0pt}{-2.84537pt}\pgfsys@curveto{-3.14284pt}{-2.84537pt}{-5.69055pt}{-5.39308pt}{-5.69055pt}{-8.53592pt}\pgfsys@lineto{-5.69055pt}{-8.53592pt}\pgfsys@curveto{-5.69055pt}{-11.67876pt}{-3.14284pt}{-14.22647pt}{0.0pt}{-14.22647pt}\pgfsys@lineto{0.0pt}{-14.22647pt}\pgfsys@curveto{3.14284pt}{-14.22647pt}{5.69055pt}{-11.67876pt}{5.69055pt}{-8.53592pt}\pgfsys@lineto{5.69055pt}{-8.53592pt}\pgfsys@curveto{5.69055pt}{-5.39308pt}{3.14284pt}{-2.84537pt}{0.0pt}{-2.84537pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{-14.22647pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.33159pt}{-10.68869pt}\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{\begin{math}{\varepsilon}\end{math}} }}\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}}\quad=\quad\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}

{\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}\pgfsys@moveto{0.0pt}{10.2432pt}\pgfsys@curveto{0.0pt}{-0.40878pt}{0.0pt}{-6.41985pt}{0.0pt}{-17.07182pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{15.93375pt}\pgfsys@lineto{0.0pt}{15.93375pt}\pgfsys@curveto{-3.14284pt}{15.93375pt}{-5.69055pt}{13.38603pt}{-5.69055pt}{10.2432pt}\pgfsys@lineto{-5.69055pt}{10.2432pt}\pgfsys@curveto{-5.69055pt}{7.10036pt}{-3.14284pt}{4.55264pt}{0.0pt}{4.55264pt}\pgfsys@lineto{0.0pt}{4.55264pt}\pgfsys@curveto{3.14284pt}{4.55264pt}{5.69055pt}{7.10036pt}{5.69055pt}{10.2432pt}\pgfsys@lineto{5.69055pt}{10.2432pt}\pgfsys@curveto{5.69055pt}{13.38603pt}{3.14284pt}{15.93375pt}{0.0pt}{15.93375pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{4.55264pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.44728pt}{9.06264pt}\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{\begin{math}{\eta_{i}}\end{math}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}{} {}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{}\pgfsys@moveto{7.62721pt}{-5.92317pt}\pgfsys@lineto{0.0pt}{1.70404pt}\pgfsys@lineto{-7.62721pt}{-5.92317pt}\pgfsys@lineto{0.0pt}{-13.55038pt}\pgfsys@closepath\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{\text{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-19.47356pt}\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{\begin{math}{\rho}\end{math}} }}\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}}\quad=\quad\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{3.41458pt}\pgfsys@curveto{0.0pt}{-4.57445pt}{0.0pt}{-9.0828pt}{0.0pt}{-17.07182pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{9.10513pt}\pgfsys@lineto{0.0pt}{9.10513pt}\pgfsys@curveto{-3.14284pt}{9.10513pt}{-5.69055pt}{6.55742pt}{-5.69055pt}{3.41458pt}\pgfsys@lineto{-5.69055pt}{3.41458pt}\pgfsys@curveto{-5.69055pt}{0.27174pt}{-3.14284pt}{-2.27597pt}{0.0pt}{-2.27597pt}\pgfsys@lineto{0.0pt}{-2.27597pt}\pgfsys@curveto{3.14284pt}{-2.27597pt}{5.69055pt}{0.27174pt}{5.69055pt}{3.41458pt}\pgfsys@lineto{5.69055pt}{3.41458pt}\pgfsys@curveto{5.69055pt}{6.55742pt}{3.14284pt}{9.10513pt}{0.0pt}{9.10513pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{-2.27597pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.79599pt}{2.72958pt}\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{\begin{math}{\eta_{j}}\end{math}} }}\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}}}

{\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}{}{}{}{{}}{}\pgfsys@moveto{0.0pt}{10.2432pt}\pgfsys@curveto{0.0pt}{-0.40878pt}{0.0pt}{-6.41985pt}{0.0pt}{-17.07182pt}\pgfsys@stroke\pgfsys@invoke{ }\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{15.93375pt}\pgfsys@lineto{0.0pt}{15.93375pt}\pgfsys@curveto{-3.14284pt}{15.93375pt}{-5.69055pt}{13.38603pt}{-5.69055pt}{10.2432pt}\pgfsys@lineto{-5.69055pt}{10.2432pt}\pgfsys@curveto{-5.69055pt}{7.10036pt}{-3.14284pt}{4.55264pt}{0.0pt}{4.55264pt}\pgfsys@lineto{0.0pt}{4.55264pt}\pgfsys@curveto{3.14284pt}{4.55264pt}{5.69055pt}{7.10036pt}{5.69055pt}{10.2432pt}\pgfsys@lineto{5.69055pt}{10.2432pt}\pgfsys@curveto{5.69055pt}{13.38603pt}{3.14284pt}{15.93375pt}{0.0pt}{15.93375pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{4.55264pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.44728pt}{9.06264pt}\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{\begin{math}{\eta_{i}}\end{math}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}{} {}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{}\pgfsys@moveto{7.62721pt}{-5.92317pt}\pgfsys@lineto{0.0pt}{1.70404pt}\pgfsys@lineto{-7.62721pt}{-5.92317pt}\pgfsys@lineto{0.0pt}{-13.55038pt}\pgfsys@closepath\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{\text{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-19.47356pt}\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{\begin{math}{\rho}\end{math}} }}\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}}\quad=\quad\leavevmode\hbox to34.54pt{\vbox to34.54pt{\pgfpicture\makeatletter\hbox{\hskip 17.27182pt\lower-17.27182pt\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{ }{} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@moveto{-17.07182pt}{17.07182pt}\pgfsys@lineto{-17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{-17.07182pt}\pgfsys@lineto{17.07182pt}{17.07182pt}\pgfsys@closepath\pgfsys@moveto{17.07182pt}{-17.07182pt}\pgfsys@clipnext\pgfsys@stroke\pgfsys@invoke{ }{{{}}{}{{}}{}{}{{}}{}{{}}{}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{}}{}{{}}{}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{} {{}}{{}{}}{{}} {{{}}{{}}}{{}}{{}}{{{}}{{}}}{{}}{}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{3.41458pt}\pgfsys@curveto{0.0pt}{-4.57445pt}{0.0pt}{-9.0828pt}{0.0pt}{-17.07182pt}\pgfsys@stroke\pgfsys@invoke{ } {}{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{ }\pgfsys@stroke@opacity{0.9}\pgfsys@invoke{ }\pgfsys@fill@opacity{0.9}\pgfsys@invoke{ }{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{0.0pt}{9.10513pt}\pgfsys@lineto{0.0pt}{9.10513pt}\pgfsys@curveto{-3.14284pt}{9.10513pt}{-5.69055pt}{6.55742pt}{-5.69055pt}{3.41458pt}\pgfsys@lineto{-5.69055pt}{3.41458pt}\pgfsys@curveto{-5.69055pt}{0.27174pt}{-3.14284pt}{-2.27597pt}{0.0pt}{-2.27597pt}\pgfsys@lineto{0.0pt}{-2.27597pt}\pgfsys@curveto{3.14284pt}{-2.27597pt}{5.69055pt}{0.27174pt}{5.69055pt}{3.41458pt}\pgfsys@lineto{5.69055pt}{3.41458pt}\pgfsys@curveto{5.69055pt}{6.55742pt}{3.14284pt}{9.10513pt}{0.0pt}{9.10513pt}\pgfsys@closepath\pgfsys@moveto{-5.69055pt}{-2.27597pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.79599pt}{2.72958pt}\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{\begin{math}{\eta_{j}}\end{math}} }}\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}}}

a

a

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsHomotopy and Cohomology in Algebraic Topology · Algebraic structures and combinatorial models · Advanced Topics in Algebra

Full text

11institutetext: Department of Philosophy, Carnegie Mellon University,

Pittsburgh, PA 15213, USA

Current address: Fachbereich Mathematik, Technische Universität Darmstadt,

Schlossgartenstraße 7, 64289 Darmstadt, Germany

11email: [email protected] 22institutetext: Carnegie Mellon School of Computer Science,

5000 Forbes Avenue, Pittsburgh, PA 15213, USA

Current address: Department of Mathematics and Computer Science,

Wesleyan University,

265 Church Street, Middletown, CT 06459, USA

22email: [email protected]

Varieties of Cubical Sets

Ulrik Buchholtz 11

Edward Morehouse 22

Abstract

We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning that the corresponding presheaf categories of cubical sets model classical homotopy theory. We delineate exactly which ones are even strict test categories, meaning that products of cubical sets correspond to products of homotopy types.

1 Introduction

There has been substantial interest recently in the use of cubical structure as a basis for higher-dimensional type theories [2, 3, 4, 1]. A question that quickly arises is, what sort of cubical structure, because there are several plausible candidates to choose from.

The suitability of a given cubical structure as a basis for a higher-dimensional type theory is dependent on at least two considerations: its proof-theoretic characteristics (e.g. completeness with respect to a given class of models, decidability of equality of terms, existence of canonical forms) and its homotopy-theoretic characteristics, most importantly, that the synthetic homotopy theory to which it gives rise should agree with the standard homotopy theory for topological spaces.

Contributions.

In this paper we organize various notions of cubical sets along several axes, using substructural algebraic theories as a guiding principle [10]. We define a range of cube categories (or cubical sites), categories $\mathbb{C}$ for which the corresponding presheaf category $\widehat{\mathbb{C}}$ can be thought of as a category of cubical sets. We then consider each of these from the perspective of test categories [7], which relates presheaf categories and homotopy theory. We give a full analysis of our cubical sites as test categories.

1.1 Cube Categories

Our cube categories are presented as monoidal categories with a single generating object, $X$ , representing an abstract dimension. To give such a presentation, then, is to give a collection of morphism generators, $f:X^{\otimes n}\to X^{\otimes m}$ , and a collection of equations between parallel morphisms. Such a presentation is known in the literature as a “PRO”. Two closely-related notions are those of “PROP” and of “Lawvere theory”, the difference being that a PROP assumes that the monoidal category is symmetric, and a Lawvere theory further assumes that it is cartesian. These additional assumptions manifest themselves in the proof theory as the admissibility of certain structural rules: in a PROP, the structural rule of exchange is admissible, and in a Lawvere theory weakening and contraction are admissible as well.

The distinguishing property of a theory making it “cubical”, rather than of some other “shape”, is the presence of two generating morphisms, $d^{0},d^{1}:1\to X$ representing the face maps (where “ $1$ ” is the monoidal unit). This is because combinatorially, an $n$ -dimensional cube has $2n$ many $(n-1)$ -cube faces, namely, two in each dimension.

1.2 Test Categories

In his epistolary research diary, Pursuing Stacks, Grothendieck set out a program for the study of abstract homotopy. The homotopy theory of topological spaces can be described as that of (weak) higher-dimensional groupoids. Higher-dimensional groupoids also arise from combinatorially-presented structures, such as simplicial or, indeed, cubical sets, which can thus be seen as alternative presentations of the classical homotopy category, Hot. That is, Hot arises either from the category of topological spaces, or from the category of simplicial sets, by inverting a class of morphisms (the weak equivalences).

Recall that for any small category $A$ and any cocomplete category $\mathcal{E}$ , there is an equivalence between functors $i:A\to\mathcal{E}$ and adjunctions

[TABLE]

where $i_{!}$ is the left Kan extension of $i$ , and $i^{*}(X)(a)=\operatorname{Hom}_{\mathcal{E}}(i(a),X)$ .111In this paper, all small categories are considered as strict categories, and Cat denotes the $1$ -category of these. Here $\widehat{A}$ is the category of functors $A^{\mathrm{op}}\to\textup{Set}$ , also known as the presheaf topos of $A$ . The category of simplicial sets is defined as the presheaf category $\textup{sSet}=\widehat{\Delta}$ , where $\Delta$ is the category of non-empty finite totally ordered sets and order-preserving maps.

The category of small categories, Cat, likewise presents the homotopy category, by inverting the functors that become weak equivalences of simplicial sets after applying the nerve functor, which is the right adjoint functor $N=i^{*}$ coming from the inclusion $\Delta\hookrightarrow\textup{Cat}$ . Grothendieck realized that this allows us to compare the presheaf category $\widehat{A}$ , for any small category $A$ , with the homotopy category in a canonical way, via the functor $i_{A}:A\to\textup{Cat}$ given by $i_{A}(a)=A_{/a}$ . The left Kan extension is in this case also denoted $i_{A}$ and we have $i_{A}(X)=A_{/X}$ for $X$ in $\widehat{A}$ . He identified the notion of a test category, which is one for which the homotopy category of its category of presheaves is equivalent to the homotopy category via the right adjoint $i_{A}^{*}$ , after localization at the weak equivalences. In other words, presheaves over a test category are models for homotopy types of spaces/ $\infty$ -groupoids. In this way, the simplex category $\Delta$ is a test category, and the classical cube category of Serre and Kan, $\mathbb{C}_{(\mathrm{w},{\cdot})}$ in our notation, is also a test category.

One perceived benefit of the simplex category $\Delta$ is that the induced functor $\textup{sSet}\to\textup{Hot}$ preserves products, whereas the functor $\widehat{\mathbb{C}_{(\mathrm{w},{\cdot})}}\to\textup{Hot}$ does not. A test category $A$ for which the functor $\widehat{A}\to\textup{Hot}$ preserves products is called a strict test category. We shall show that most natural cube categories are in fact strict test categories.

2 Cube categories

In this paper, we consider as base categories the syntactic categories for a range of monoidal theories, all capturing some aspect of the notion of an interval. We call the resulting categories “cube categories”, because the monoidal powers of the interval then correspond to cubes222Here we say “cube” for short instead of “hypercube” for an arbitrary dimensional power of an interval. A prefix will indicate the dimension, as in [math]-cube, $1$ -cube, etc..

The generating morphisms for these cube categories can be classified either as structural, natural families corresponding to structural rules of a proof theory, or as algebraic, distinguished by the property of having coarity one. Our cube categories vary along three dimensions: the structural rules present, the signature of algebraic function symbols, and the equational theory.

This section is organized as follows: in subsection 2.1 we recall the basics of algebraic theories in monoidal categories, and in subsection 2.2 we discuss how monoidal languages are interpreted in monoidal categories. Then we introduce in subsection 2.3 the monoidal languages underlying our cubical theories, so that in subsection 2.4 we can introduce the standard interpretations of these and our cubical theories. In subsection 2.5 we give a tour of the resulting cube categories.

2.1 Monoidal algebraic theories

We assume the reader is familiar with ordinary algebraic theories and their categorical incarnations as Lawvere theories. The idea of monoidal algebraic theories as described by [10] is to generalize this to cases where only a subset of the structural rules (weakening, exchange and contraction) are needed to describe the axioms. Think for example of the theory of monoids over a signature of a neutral element $1$ and a binary operation. The axioms state that $1x=x=x1$ (in the context of one variable $x$ ) and $x(yz)=(xy)z$ (in the context of the variables $x$ , $y$ and $z$ ). Note that the terms in these equations each contain all the variables of the context and in the same order. Thus, no structural rules are needed to form the equations, and hence the notion of a monoid makes sense in any monoidal category.

Let us now make this more precise. For the structural rules, we follow Mauri (ibid.) and consider any subset of $\{\mathrm{w},\mathrm{e},\mathrm{c}\}$ ( $\mathrm{w}$ for weakening, $\mathrm{e}$ for exchange, and $\mathrm{c}$ for contraction), except that whenever $\mathrm{c}$ is present, so is $\mathrm{e}$ . Thus we consider the following lattice of subsets of structural rules:

[TABLE]

It would be possible to consider monoidal theories over operations that have any number of incoming and outgoing edges, representing morphisms $f:A_{1}\otimes\dots\otimes A_{n}\to B_{1}\otimes\dots\otimes B_{m}$ in a monoidal category, where the $A_{i}$ and $B_{j}$ are sorts. However, it simplifies matters considerably, and suffices for our purposes, to consider only operations of the usual kind in algebra, with any arity of incoming edges and exactly one outgoing edge, as in $f:A_{1}\otimes\dots\otimes A_{n}\to B$ .

Furthermore, we shall consider only single-sorted theories, defined over a signature $\Sigma$ given by a set of function symbols with arities. For a single-sorted signature, the types can of course be identified with the natural numbers.

A (single-sorted, algebraic) monoidal language consists of a pair of a set of structural rules together with an algebraic signature. A term $t$ in a context of $n$ free variables $x_{1},\dots,x_{n}$ is built up from the function symbols in such a way that when we list the free variables in $t$ from left to right:

•

every variables occurs unless $\mathrm{w}$ (weakening) is a structural rule;

•

the variables occur in order unless $\mathrm{e}$ (exchange) is a structural rule; and

•

there are no duplicated variables unless $\mathrm{c}$ (contraction) is a structural rule.

For the precise rules regarding term formation and the proof theory of equalities of terms, we refer to [10].

2.2 Interpretations

An interpretation of a monoidal language in a monoidal category $(\mathcal{E},1,\otimes)$ will consist of an object $X$ representing the single sort, together with morphisms representing the structural rules and morphisms representing the function symbols (including constants).

The structural rules $\mathrm{w}$ , $\mathrm{e}$ , $\mathrm{c}$ are interpreted respectively by morphisms

[TABLE]

satisfying certain laws [10, (27–36)]. These laws specify also the interaction between these morphisms and the morphisms corresponding to the function symbols. When $\mathcal{E}$ is symmetric monoidal, we interpret $\tau$ by the braiding of $\mathcal{E}$ , and when $\mathcal{E}$ is cartesian monoidal, we interpret everything using the cartesian structure. A function symbol $f$ of arity $n$ is interpreted by a morphism $\lvert f\rvert:X^{\otimes n}\to X$ . This morphism and the structural morphisms are required to interact nicely, e.g., $\varepsilon\circ\lvert f\rvert=\varepsilon^{\otimes n}$ (cf. loc. cit.).

In a syntactic category for the empty theory (of which the syntactic category for a non-empty theory is a quotient), every morphism factors uniquely as a structural morphism followed by a functional one (op. cit., Prop. 5.1). When we impose a theory, we may of course lose uniqueness, but we still have existence.

2.3 Cubical monoidal languages

All of our cubical signatures will include the two endpoints of the interval as nullary function symbols, [math] and $1$ . For the rest, we consider the two “connections” $\vee$ and $\wedge$ , as well as the reversal, indicated by a prime, ′. This gives us the following lattice of 6 signatures:

[TABLE]

Combined with the 6 possible combinations of structural rules, we are thus dealing with 36 distinct languages.

Definition 1

Let $L_{(a,b)}$ , where $a$ is one of the six substrings of “ $\mathrm{wec}$ ” corresponding to (2) and $b$ one of the six substrings of “ ${\vee}{\wedge}{}^{\prime}$ ” corresponding to (3), denote the language with structural rules from $a$ and signature obtained from $(0,1)$ by expansion with the elements of $b$ .

We shall, however, mostly consider the 18 languages with weakening present (otherwise we are dealing with semi-cubical sets).

The third dimension of variation for our cube categories is the algebraic theory for a given language. Here we shall mostly pick the theory of a particular standard structure, so let us pause our discussion of cube categories to introduce our standard structures.

2.4 The canonical cube categories

We consider the interval structures of the following objects in the cartesian monoidal categories Top and Set (so all structural rules are supported, interpreted by the global structure):

•

the standard topological interval, $I=[0,1]$ in Top;

•

the standard $2$ -element set, $I=\mathbbold{2}=\{0,1\}$ in Set.

For the topological interval, we take $x\vee y=\max\{x,y\}$ , $x\wedge y=\min\{x,y\}$ and $x^{\prime}=1-x$ . These formulas also apply to the $2$ -element set $\mathbbold{2}$ .

We can also consider the $3$ -element Kleene algebra (cf. subsection 2.5) $\mathbbold{3}=\{0,u,1\}$ with $u^{\prime}=u$ and the $4$ -element de Morgan algebra $\mathbb{D}=\{0,u,v,1\}$ with $u^{\prime}=u$ and $v^{\prime}=v$ in Set (called the diamond), as further structures. It is interesting to note here that $\mathbbold{3}$ has the same theory as $[0,1]$ in the full language, namely the theory of Kleene algebras [5]. Of course, $\mathbbold{2}$ gives us the theory of Boolean algebras, while $\mathbb{D}$ gives the theory of de Morgan algebras.

Definition 2

With $(a,b)$ as in Def. 1, and $T$ a theory in the language $L_{(a,b)}$ , let $\mathbb{C}_{(a,b)}(T)$ denote the syntactic category of the theory $T$ . We write $\mathbb{C}_{(a,b)}$ for short for $\mathbb{C}_{(a,b)}(\mathrm{Th}([0,1]))$ for the syntactic category of the topological interval with respect to the monoidal language $L_{(a,b)}$ .

We say that $\mathbb{C}_{(a,b)}$ is the canonical cube category for the language $L_{(a,b)}$ .

Proposition 1

The canonical cube category $\mathbb{C}_{(a,b)}$ is isomorphic to the monoidal subcategory of Top generated by $[0,1]$ with respect to the language $L_{(a,b)}$ .

In fact, since the forgetful functor $\textup{Top}\to\textup{Set}$ is faithful, we get the same theory in every language whether we consider the interval $[0,1]$ in Top or in Set, and it generates the same monoidal subcategory in either case.

Proposition 2

If $L$ is a cubical language strictly smaller than the maximal language, $L_{(\mathrm{wec},\vee\wedge{}^{\prime})}$ , then the theory of the standard structure $[0,1]$ is the same as the theory of the standard structure $\mathbbold{2}=\{0,1\}$ in Set. For $L_{(\mathrm{wec},\vee\wedge{}^{\prime})}$ the theory of $[0,1]$ equals the theory of the three-element Kleene algebra, $\mathbbold{3}$ , and is in fact the theory of Kleene algebras.

Proof

If $L$ does not have reversal, then we can find for any points $a<b$ in $[0,1]$ a homomorphism $f:[0,1]\to\mathbbold{2}$ in Set with $f(a)<f(b)$ (cut between $a$ and $b$ ), so $[0,1]$ and $\mathbbold{2}$ have the same theory.

If $L$ does not have contraction, each term is monotone in each variable. By pushing reversals towards the variables and applying the absorption laws, we can find for each resulting term $s[x,y_{1},\dots y_{n}]$ instantiations $b_{1},\dots,b_{n}\in\mathbbold{2}$ with $s[0,b_{1},\dots,b_{n}]\neq s[1,b_{1},\dots,b_{n}]$ . It follows that if two terms agree on instantiations in $\mathbbold{2}$ , then they use each variable the same way: either with or without a reversal. Hence we can ignore the reversals and use the previous case.

The last assertion is proved by [5].∎

Corollary 1

For each canonical cube category $\mathbb{C}_{(a,b)}$ we have decidable equality of terms.

Proof

This follows because equality is decidable in the theory of Kleene algebras, as this theory is characterized by the object $\mathbbold{3}$ . Hence we can decide equality by the method of “truth-tables”, however, relative to the elements of $\mathbbold{3}$ .∎

Of course, any algorithm for equality in the theory of Kleene algebras can be used, including the one based on disjunctive normal forms (op. cit.).

We can in the presence of weakening quite simply give explicit axiomatizations for each of the canonical cube categories $\mathbb{C}_{(a,b)}$ : take the subset of axioms in Tab. 1 that make sense in the language $L_{(a,b)}$ . Without weakening, this will not suffice, as we should need infinitely many axioms to ensure for instance that $s\wedge 0=t\wedge 0$ where $s,t$ are terms in the same variable context.

When we compare our canonical cube categories to the categories of [6], we find $\mathbb{I}=\mathbb{C}_{(\mathrm{w},{\cdot})}$ , $\mathbb{J}=\mathbb{C}_{(\mathrm{w},\vee\wedge)}$ , $\mathbb{K}=\mathbb{C}_{(\mathrm{we},\vee\wedge)}$ , and $!\mathbb{K}=\mathbb{C}_{(\mathrm{we},\vee\wedge^{\prime})}$ .

For the full language, $L_{(\mathrm{wec},{\vee}{\wedge}^{\prime})}$ , there are two additional interesting cube categories: $\mathbb{C}_{\mathrm{dM}}$ (de Morgan algebras) and $\mathbb{C}_{\mathrm{BA}}$ (boolean algebras), where de Morgan algebras satisfy all the laws of Tab. 1 except Kleene’s law, and boolean algebras of course satisfy additionally the law $x\vee x^{\prime}=1$ . The case of de Morgan algebras is noteworthy as the basis of the cubical model of type theory of [4].

Definition 3

For each of our cube categories $\mathbb{C}$ , we write $[n]$ for the object representing a context of $n$ variables, and we write $\square^{n}$ for the image of $[n]$ under the Yoneda embedding $\operatorname{y}:\mathbb{C}\hookrightarrow\widehat{\mathbb{C}}$ .

2.5 A tour of the menagerie

2.5.1 Plain cubes

In the canonical cube category for the language $L_{(\mathrm{w},{\cdot})}$ the monoidal unit $[0]$ is terminal and the interpretation of weakening is generated by the unique degeneracy map $\varepsilon:{[1]}\to{[0]}$ . The points [math] and $1$ are interpreted by face maps $\eta_{0},\eta_{1}:{[0]}\to{[1]}$ . In the following we let $\{i,j\}$ range over $\{0,1\}$ with the assumption that $i\not=j$ .

Because $[0]$ is terminal we have the face-degeneracy laws, $\varepsilon\circ\eta_{i}=\operatorname{Id}_{[0]}$ , which we represent string-diagrammatically as:

[TABLE]

This law is invisible in the algebraic notation.

In a presheaf $T$ , the face maps give rise to reindexing functions between the fibers, $\partial^{i}_{k}:{T[n+1]}\to{T[n]}$ , where $1\leq k\leq n+1$ . In particular, when $n$ is [math] these pick out the respective boundary points of an interval. Similarly, the degeneracy map gives rise to reindexing functions between the fibers, $\ast_{k}:{T[n]}\to{T[n+1]}$ , where $1\leq k\leq n+1$ . In particular, when $n$ is [math] this determines a degenerate interval $\ast(a)\in T[1]$ on a point $a\in T[0]$ , and the face-degeneracy laws tell us its boundary points: $\partial^{0}(\ast(a))=\partial^{1}(\ast(a))=a$ .

Adding the structural law of exchange to the language adds a natural isomorphism $\tau:{[2]}\to{[2]}$ to the syntactic category. In a presheaf, this lets us permute any adjacent pair of a cube’s dimensions by reflecting it across the corresponding diagonal (hyper)plane. In particular, $T(\tau)$ reflects a square across its main diagonal.

2.5.2 Cubes with diagonals

In the canonical cube category for the language $L_{(\mathrm{wec},{\cdot})}$ the monoidal product is cartesian and the interpretation of contraction is generated by the diagonal map $\delta:{[1]}\to{[2]}$ . In this case, the pair $(\delta,\varepsilon)$ forms a cocommutative comonoid.

Because $\delta$ is natural we have the face-diagonal laws, $\delta\circ\eta_{i}=\eta_{i}\otimes\eta_{i}$ , which we represent string-diagrammatically as:

[TABLE]

In a presheaf $T$ , the diagonal map gives rise to reindexing functions between the fibers, $d_{k}:{T[n+2]}\to{T[n+1]}$ , where $1\leq k\leq n+1$ . In particular, when $n$ is [math] this picks out the main diagonal of a square, and the face-diagonal laws tell us its boundary points.

In the cubical semantics, the fact that $\varepsilon$ is a comonoid counit for $\delta$ tells us that the diagonal of a square formed by degenerating an interval is just that interval. Likewise, the fact that $\delta$ is coassociative tells us that the main diagonal interval of a higher-dimensional cube is well-defined.

2.5.3 Cubes with reversals

In the canonical cube category for the language $L_{({\cdot},\mathrm{{}^{\prime}})}$ we have an involutive reversal map $\rho:{[1]}\to{[1]}$ . A reversal acts by swapping the face maps, giving the face-reversal laws, $\rho\circ\eta_{i}=\eta_{j}$ , which we represent string-diagrammatically as:

[TABLE]

This embodies the equations $0^{\prime}=1$ and $1^{\prime}=0$ .

In a presheaf $T$ , the reversal map gives rise to endomorphisms on the fibers, $!_{k}:{T[n+1]}\to{T[n+1]}$ , where $1\leq k\leq n+1$ . In particular, when $n$ is [math] this reverses an interval, and the face-reversal laws tell us its boundary points.

If the signature contains weakening, then we have the reversal-degeneracy law, $\varepsilon\circ\rho=\varepsilon$ . In the cubical interpretation, this says that a degenerate interval is invariant under reversal. If the signature contains contraction, then we have the reversal-diagonal law, $\delta\circ\rho=(\rho\otimes\rho)\circ\delta$ . Cubically, this says that the reversal of a square’s diagonal is the diagonal of the square resulting from reversing in each dimension.

2.5.4 Cubes with connections

In the canonical cube category for the language $L_{(\mathrm{w},\vee\wedge)}$ , the connectives are interpreted by connection maps $\mu_{0},\mu_{1}:{[2]}\to{[1]}$ . Each pair $(\mu_{i},\eta_{i})$ forms a monoid. Furthermore, the unit for each monoid is an absorbing element for the other: $\mu_{j}\circ(\eta_{i}\otimes\operatorname{Id})=\eta_{i}\circ\varepsilon=\mu_{j}\circ(\operatorname{Id}\otimes\eta_{i})$ . [6] call such structures “dioids”, so we refer to these as the dioid absorption laws, and represent them string-diagrammatically as:

[TABLE]

Equationally, these amount to the ${\vee}$ - and ${\wedge}$ -absorption laws of Tab. 1.

In the cubical semantics, connections can be seen as a variant form of degeneracy, identifying adjacent, rather than opposite, faces of a cube. Of course in order for this to make sense, a cube must have at least two dimensions. In a presheaf $T$ , the connection maps give rise to reindexing functions between the fibers, $\ulcorner_{k},\lrcorner_{k}:{T[n+1]}\to{T[n+2]}$ , where $1\leq k\leq n+1$ . In particular, when $n$ is [math] these act as follows:

[TABLE]

It may help to think of the interval $f$ as a folded paper fan, with its “hinge” at the domain end in the case of $\lrcorner$ , and at the codomain end in the case of $\ulcorner$ . The respective connected squares are then obtained by “opening the fan”. The monoid unit laws give us the (generally) non-degenerate faces of a connected square, while the dioid absorption laws give us the (necessarily) degenerate ones. Monoid associativity says that multiply-connected higher-dimensional cubes are well-defined.

Because $[0]$ is terminal we also have the connection-degeneracy laws, $\varepsilon\circ\mu_{i}=\varepsilon\otimes\varepsilon$ , which say that a connected square arising from a degenerate interval is a doubly-degenerate square. In the presence of exchange, we further assume that the $\mu_{i}$ are commutative. In the cubical semantics, this implies that connected cubes are invariant under reflection across their connected dimensions.

When adding contraction to the signature, we must give a law for rewriting a diagonal following a connection such that the structural maps come first. This is done by the connection-diagonal laws, $\delta\circ\mu_{i}=(\mu_{i}\otimes\mu_{i})\circ(\operatorname{Id}\otimes\tau\otimes\operatorname{Id})\circ(\delta\otimes\delta)$ , which we represent string-diagrammatically as:

[TABLE]

Algebraically, this says that two copies of a conjunction consists of a pair of conjunctions, each on copies of the respective terms; cubically, it gives the connected square on the diagonal interval of another square in terms of a product of diagonals in the $4$ -cube resulting from connecting each dimension separately. The whole structure, then, is a pair of bicommutative bimonoids, $(\delta,\varepsilon,\mu_{i},\eta_{i})$ related by the dioid absorption laws. We refer to these as linked bimonoids.

Additionally, we may impose the laws of bounded, modular, or distributive lattices, each of which implies its predecessors, and all of which imply the diagonal-connection laws, $\mu_{i}\circ\delta=\operatorname{Id}_{[1]}$ , known in the literature (rather generically) as “special” laws. These correspond to the ${\vee}$ - and ${\wedge}$ -idempotence laws of Tab. 1.

2.5.5 The full signature

When both reversals and connections are present, the de Morgan laws, $\rho\circ\mu_{i}=\mu_{j}\circ(\rho\otimes\rho)$ permute reversals before connections:

[TABLE]

These laws imply each other as well as their nullary versions, the face-reversal laws.

Using the algebraic characterization of order in a lattice, $x\wedge y=x\Longleftrightarrow x\leq y\Longleftrightarrow x\vee y=y$ , we can express the Kleene law as $\mu_{i}\circ(\mu_{i}\otimes\mu_{j})\circ(\operatorname{Id}\otimes\rho\otimes\operatorname{Id}\otimes\rho)\circ(\delta\otimes\delta)=\mu_{i}\circ(\operatorname{Id}\otimes\rho)\circ(\delta\otimes\varepsilon)$ :

[TABLE]

Finally, we arrive at the structure of a boolean algebra by assuming the Hopf laws, $\mu_{i}\circ(\operatorname{Id}\otimes\rho)\circ\delta=\eta_{j}\circ\varepsilon$ :

[TABLE]

Cubically, these say that the anti-diagonal of a connected square is degenerate.

3 Test categories

As mentioned in the introduction, a test category is a small category $A$ such that the presheaf category $\widehat{A}$ can model the homotopy category after a canonical localization. Here we recall the precise definitions (cf. [8]).

The inclusion functor $i:\Delta\to\textup{Cat}$ induces via (1) an adjunction $i_{!}:\widehat{\Delta}\leftrightarrows\textup{Cat}:N$ where the right adjoint $N$ is the nerve functor. This allows us to transfer the homotopy theory of simplicial sets to the setting of (strict) small categories, in that we define a functor $f:A\to B$ to be a weak equivalence if $N(f)$ is a weak equivalence of simplicial sets. A small category $A$ is called aspheric (or weakly contractible) if the canonical functor $A\to 1$ is a weak equivalence. Since any natural transformation of functors induces a homotopy, it follows that any category with a natural transformation between the identity functor and a constant endofunctor is contractible, and hence aspheric. In particular, a category with an initial or terminal object is aspheric. It follows from Quillen’s Theorem A [11] that a functor $f:A\to B$ is a weak equivalence, if it is aspheric, meaning that all the slice categories $A_{/b}$ are aspheric, for $b\in B$ .333We follow Grothendieck and let the slice $A_{/b}$ denote the comma category $(f\downarrow b)$ of the functors $f:A\to B$ and $b:1\to B$ . Similarly, the coslice ${}_{b\setminus{}}A$ denotes $(b\downarrow f)$ . By duality, so is any coaspheric functor $f:A\to B$ , one for which the coslice categories ${}_{b\setminus{}}A$ , for $b\in B$ , are all aspheric. Finally, we say that a presheaf $X$ in $\widehat{A}$ is aspheric, if $A_{/X}$ is (note that $A_{/X}$ is the category of elements of $X$ ).

For any small category $A$ , we can use the adjunction induced by the functor $i_{A}:A\to\textup{Cat}$ , $i_{A}(a)=A_{/a}$ (as mentioned in subsection 1.2) to define the class of weak equivalences in $\widehat{A}$ , $\mathcal{W}_{A}$ ; namely, $f:X\to Y$ in $\widehat{A}$ is in $\mathcal{W}_{A}$ if $i_{A}(f):A_{/X}\to A_{/Y}$ is a weak equivalence of categories. Following Grothendieck, we make the following definitions:

•

$A$ is a weak test category if the induced functor $\overline{i_{A}}:(\mathcal{W}_{A})^{-1}\widehat{A}\to\textup{Hot}$ is an equivalence of categories (the inverse is then $\overline{i_{A}^{*}}$ ).

•

$A$ is a local test category if all the slices $A_{/a}$ are weak test categories.

•

$A$ is a test category if $A$ is both a weak and a local test category.

•

$A$ is a strict test category if $A$ is a test category and the functor $\widehat{A}\to\textup{Hot}$ preserves finite products.

The goal of the rest of this section is to prove that all the cube categories with weakening are test categories, and to establish exactly which ones are strict test categories. First we introduce Grothendieck interval objects. These allow us to show that any cartesian cube category is a strict test category (Cor. 2) as well as to show that all the cube categories are test categories (Cor. 3). Then we adapt an argument of [9] to show that any cube category with a connection is a strict test category (Thm. 3.3). Finally, we adapt another argument of his to show that the four remaining cube categories fail to be strict test categories (Thm. 3.4). The end result is summarized in Tab. 2.

In order to study test categories, [7] introduced the notion of an interval (segment in the terminology of [8]) in a presheaf category $\widehat{A}$ . This is an object $I$ equipped with two global elements $d^{0},d^{1}$ . As such, it is just a structure for the initial cubical language, $L_{({\cdot},{\cdot})}$ in the cartesian monoidal category $\widehat{A}$ , and $\square^{1}$ is thus canonically a Grothendieck interval in all our categories of cubical sets, $\widehat{\mathbb{C}}$ .

An interval is separated if the equalizer of $d^{0}$ and $d^{1}$ is the initial presheaf, $\varnothing$ . For cubical sets, this is the case if and only if $0=1$ is not derivable in the base category, in any variable context.

The following theorem is due to [7, 44(c)], cf. Thm. 2.6 of [9]. We say that $A$ is totally aspheric if $A$ is non-empty and all the products $\operatorname{y}(a)\times\operatorname{y}(b)$ are aspheric, where $\operatorname{y}:A\to\widehat{A}$ is the Yoneda embedding.

Theorem 3.1 (Grothendieck)

If $A$ is a small category that is totally aspheric and has a separated aspheric interval, then $A$ is a strict test category.

Corollary 2

If $\mathbb{C}$ is any canonical cube category over the full set of structural rules, $\mathbb{C}_{(\mathrm{wec},b)}$ , or the cartesian cube category of de Morgan algebras or that of boolean algebras, then $\mathbb{C}$ is a strict test category.

Proof

Since $\mathbb{C}$ has finite products it is totally aspheric, as the Yoneda embedding preserves finite products. The Grothendieck interval corresponding to the $1$ -cube is representable and hence aspheric. This interval is separated as $0=1$ is not derivable in any context.∎

The following theorem is from [7, 44(d), Prop. on p. 86]:

Theorem 3.2 (Grothendieck)

If $A$ is a small aspheric category with a separated aspheric interval $(I,d^{0},d^{1})$ in $\widehat{A}$ , and $i:A\to\textup{Cat}$ is a functor such that for any $a$ in $A$ , $i(a)$ has a final object, and there is a map of intervals $i_{!}(I)\to\mathbbold{2}$ in Cat, then $A$ is a test category.

In this case, $i$ is in fact a weak test functor, meaning that $i^{*}:\textup{Cat}\to\widehat{A}$ induces an equivalence $\textup{Hot}\to(\mathcal{W}_{A})^{-1}\widehat{A}$ .

Corollary 3

Any canonical cube category $\mathbb{C}$ is a test category.

Proof

The conditions of the theorem hold trivially for any cube category without reversal, taking $i$ to be the canonical functor sending $I$ to $\mathbbold{2}$ . If we have reversals, then we can define $i$ by sending $I$ to the category with three objects, $\{0\},\{1\},\{0,1\}$ and arrows $\{0\},\{1\}\to\{0,1\}$ . Since this is a Kleene algebra, this functor is well-defined in all cases.∎

The cube categories $\mathbb{C}_{\mathrm{dM}}$ and $\mathbb{C}_{\mathrm{BA}}$ of de Morgan and boolean algebras are test categories by Cor. 2.

We now turn to the question of which non-cartesian cube categories are strict test categories. The following theorem was proved by [9, Prop. 3.3] for the case of $\mathbb{C}_{(\mathrm{w},{\vee})}$ . The same proof works more generally, so we obtain:

Theorem 3.3

Any canonical cube category $\mathbb{C}_{(a,b)}$ where $b$ includes one of the connections $\vee$ , $\wedge$ is a strict test category.

That leaves four cases: $(\mathrm{w},{\cdot})$ , $(\mathrm{w},{{}^{\prime}})$ , $(\mathrm{we},{\cdot})$ , $(\mathrm{we},{{}^{\prime}})$ . The first of these, the “classical” cube category, is not a strict test category by the argument of [9, Sec. 5].

Note the unique factorizations we have for these categories: every morphism $f:[m]\to[n]$ factors as degeneracies, followed by (possibly) symmetries, followed by (possibly) reversals, followed by face maps. The isomorphisms are exactly the compositions of reversals and symmetries (if any).

Next, we use variations of the argument of Maltsiniotis (loc. cit.) to show that none of these four sites are strict test categories by analyzing the homotopy type of the slice category $\mathbb{C}_{/\square^{1}\times\square^{1}}$ in each case.

Theorem 3.4

The canonical cube categories $\mathbb{C}_{(\mathrm{w},{\cdot})}$ , $\mathbb{C}_{(\mathrm{w},{{}^{\prime}})}$ , $\mathbb{C}_{(\mathrm{we},{\cdot})}$ and $\mathbb{C}_{(\mathrm{we},{{}^{\prime}})}$ are not strict test categories.

Proof

Let $\mathbb{C}$ be one of these categories. We shall find a full subcategory $A$ of $\mathbb{C}_{/\square^{1}\times\square^{1}}$ that is not aspheric, and such that the inclusion is a weak equivalence. Hence $\mathbb{C}_{/\square^{1}\times\square^{1}}$ is not aspheric, and $\mathbb{C}$ cannot be a strict test category.

An object of the slice category $\mathbb{C}_{/\square^{1}\times\square^{1}}$ is given by a dimension and two terms corresponding to that dimension. We can thus represent it by a variable context $x_{1}\cdots x_{n}$ (for an $n$ -cube $[n]$ ) and two terms $s,t$ in that context.

For the classical cube category case $(\mathrm{w},{\cdot})$ , we let $A$ contain the following objects, cf. [9, Prop. 5.2]:

•

$4$ zero-dimensional objects $({\cdot},(i,j))$ , $i,j\in\{0,1\}$ .

•

$5$ one-dimensional objects; $4$ corresponding to the sides of a square, $(x,(i,x))$ and $(x,(x,i))$ with $i\in\{0,1\}$ , and $1$ corresponding to its diagonal, $(x,(x,x))$ .

•

$2$ two-dimensional objects: $(xy,(x,y))$ and $(xy,(y,x))$ (let us call them, respectively, the northern and southern hemispheres).

In the presence of the exchange rule, we do not need both of the two-dimensional objects (so we retain, say, the northern hemisphere), and in the presence of reversal, we need additionally the anti-diagonal, $(x,(x,x^{\prime}))$ .

Note that in each case $A$ is a partially ordered set (there is at most one morphism between any two objects), and we illustrate the incidence relations between the objects in Fig. 1. The figure also illustrates how to construct functors $F:A\to\textup{Top}$ , which are cofibrant with respect to the Reedy model structure on this functor category, where $A$ itself is considered a directed Reedy category relative to the obvious dimension assignment (points of dimension zero, lines of dimension one, and the hemispheres of dimension two). We conclude that the homotopy colimit of $F$ (in Top) is weakly equivalent to the ordinary colimit of $F$ , which is seen to be equivalent to $S^{2}\vee S^{1}$ , $S^{2}\vee S^{1}\vee S^{1}$ , $S^{1}$ and $S^{1}\vee S^{1}$ , respectively for the cases $(\mathrm{w},{\cdot})$ , $(\mathrm{w},{{}^{\prime}})$ , $(\mathrm{we},{\cdot})$ and $(\mathrm{we},{{}^{\prime}})$ . Since $F$ takes values in contractible spaces, this homotopy colimit represents in each case the homotopy type of the nerve of $A$ . It follows that $A$ is not aspheric.

It remains to see that the inclusion $A\hookrightarrow\mathbb{C}_{/\square^{1}\times\square^{1}}$ is in each case a weak equivalence. For this we use the dual of Quillen’s Theorem A, and show that for each object $(x_{1}\cdots x_{n},(s,t))$ (written $(s,t)$ for short) of $\mathbb{C}_{/\square^{1}\times\square^{1}}$ , the coslice category $B_{(s,t)}={}_{(s,t)\setminus}A$ has an initial object, and is hence aspheric.

As in Maltsiniotis (loc. cit.), we make case distinctions on $(s,t)$ . Note that for the languages under consideration, a term can have at most one free variable.

•

$(s,t)=(x(^{\prime}),y(^{\prime}))$ for distinct variables $x,y$ . The initial object is a hemisphere (the northern one in the presence of exchange, the southern one without exchange and in case $x,y$ appear in reversed order in the variable context).

•

$(s,t)=(x,x)$ or $(x^{\prime},x^{\prime})$ . The initial object is then the diagonal in $A$ .

•

$(s,t)=(x,x^{\prime})$ or $(x^{\prime},x)$ . The initial object is here the anti-diagonal.

•

$(s,t)=(i,x(^{\prime}))$ or $(x(^{\prime}),i)$ . The initial object is the corresponding side of the square.

•

$(s,t)=(i,j)$ . The initial object is then the corresponding vertex of the square.∎

We remark that this proof method fails in the presence of a connection, where terms can now refer to multiple variables. And in the presence of contraction, the diagonal $(x,x)$ is incident on the northern hemisphere, which is then a maximal element in $A$ , and hence $A$ is contractible. These observations explain why it is only those four cases that can fail to give strict test categories.

4 Conclusion

We have espoused a systematic algebraic framework for describing notions of cubical sets, and we have shown that all reasonable cubical sites are test categories. We have shown that a cubical site is a strict test category precisely when it is cartesian monoidal or includes one of the connections.

To improve our understanding of the homotopy theory of each cubical site, we need to investigate the induced Quillen equivalence between the corresponding category of cubical sets $\widehat{\mathbb{C}}$ with the Cisinski model structure and the category of simplicial sets $\widehat{\Delta}$ with the Kan model structure. For instance, we can ask whether the fibrations are those satisfying the cubical Kan filling conditions. Furthermore, to model type theory, one should probably require that the model structures lift to algebraic model structures. We leave all this for future work.

5 Acknowledgements

We wish to thank the members of the HoTT group at Carnegie Mellon University for many fruitful discussions, in particular Steve Awodey who has encouraged the study of cartesian cube categories since 2013 and who has been supportive of our work, as well as Bob Harper who has also been very supportive. Additionally, we deeply appreciate the influence of Bas Spitters who inspired us with a seminar presentation of a different approach to showing that $\mathbb{C}_{(\mathrm{wec},{\cdot})}$ is a strict test category.

The authors gratefully acknowledge the support of the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.

Bibliography11

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] Carlo Angiuli, Robert Harper and Todd Wilson “Computational Higher-Dimensional Type Theory” To appear In POPL ’17: Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ACM, 2017
2[2] Steve Awodey “A cubical model of homotopy type theory” Lecture notes from a series of lectures for the Stockholm Logic group In Ar Xiv e-prints , 2016 ar Xiv: 1607.06413 [math.CT]
3[3] Marc Bezem, Thierry Coquand and Simon Huber “A model of type theory in cubical sets” In 19th International Conference on Types for Proofs and Programs 26 , LIP Ics. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2014, pp. 107–128 DOI: 10.4230/LIP Ics.TYPES.2013.107 · doi ↗
4[4] Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg “Cubical Type Theory: a constructive interpretation of the univalence axiom” To appear In 21st International Conference on Types for Proofs and Programs (TYPES 2015) , LIP Ics. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2016
5[5] Mai Gehrke, Carol L. Walker and Elbert A. Walker “Normal forms and truth tables for fuzzy logics” Selected papers from the 21st Linz Seminar on Fuzzy Set Theory (2000) In Fuzzy Sets and Systems 138.1 , 2003, pp. 25–51 DOI: 10.1016/S 0165-0114(02)00566-3 · doi ↗
6[6] Marco Grandis and Luca Mauri “Cubical sets and their site” In Theory Appl. Categ. 11 , 2003, pp. No. 8, 185–211 URL: http://www.tac.mta.ca/tac/volumes/11/8/11-08abs.html
7[7] Alexander Grothendieck “Pursuing Stacks” Manuscript, 1983 URL: http://thescrivener.github.io/Pursuing Stacks/
8[8] Georges Maltsiniotis “La théorie de l’homotopie de Grothendieck” In Astérisque 301 , 2005 URL: https://webusers.imj-prg.fr/~georges.maltsiniotis/ps/prstnew.pdf