\relax 
\providecommand\hyper@newdestlabel[2]{}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}Simple type theories}{79}{chapter.2}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{chap:simple}{{2}{79}{Simple type theories}{chapter.2}{}}
\newlabel{chap:simple@cref}{{[chapter][2][]2}{[1][79][]79}}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}Towards multicategories}{79}{section.2.1}\protected@file@percent }
\newlabel{sec:why-multicats}{{2.1}{79}{Towards multicategories}{section.2.1}{}}
\newlabel{sec:why-multicats@cref}{{[section][1][2]2.1}{[1][79][]79}}
\newlabel{princ:independence}{{{$\ast $}}{79}{Towards multicategories}{AMS.13}{}}
\newlabel{princ:independence@cref}{{[equation][2147483647][]{$\ast $}}{[1][79][]79}}
\newlabel{princ:ump}{{{$\dagger $}}{80}{Towards multicategories}{AMS.14}{}}
\newlabel{princ:ump@cref}{{[equation][2147483647][]{$\dagger $}}{[1][80][]80}}
\citation{cs:multicats}
\citation{hermida:coh-univ}
\citation{leinster:higher-opds}
\citation{burroni:t-cats}
\citation{baez:why-ncats}
\@writefile{brf}{\backcite{cs:multicats,hermida:coh-univ,leinster:higher-opds,burroni:t-cats}{{81}{2.1}{AMS.14}}}
\newlabel{princ:structural}{{{$\ddagger $}}{81}{Towards multicategories}{AMS.15}{}}
\newlabel{princ:structural@cref}{{[equation][2147483647][]{$\ddagger $}}{[1][81][]81}}
\newlabel{princ:adm}{{{\S  }}{81}{Towards multicategories}{AMS.16}{}}
\newlabel{princ:adm@cref}{{[equation][2147483647][]{\S  }}{[1][81][]81}}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Introduction to multicategories}{82}{section.2.2}\protected@file@percent }
\newlabel{sec:multicats-catth}{{2.2}{82}{Introduction to multicategories}{section.2.2}{}}
\newlabel{sec:multicats-catth@cref}{{[section][2][2]2.2}{[1][82][]82}}
\@writefile{brf}{\backcite{baez:why-ncats}{{82}{1}{Hfootnote.12}}}
\newlabel{defn:multigraph}{{2.2.1}{83}{}{defn.2.2.1}{}}
\newlabel{defn:multigraph@cref}{{[defn][1][]2.2.1}{[1][83][]83}}
\citation{leinster:higher-opds}
\citation{hermida:multicats}
\citation{leinster:higher-opds}
\@writefile{brf}{\backcite{leinster:higher-opds}{{84}{2.2}{defn.2.2.2}}}
\newlabel{defn:multicat-tensor}{{2.2.3}{84}{}{defn.2.2.3}{}}
\newlabel{defn:multicat-tensor@cref}{{[defn][3][]2.2.3}{[1][84][]84}}
\newlabel{thm:multicat-repr}{{2.2.4}{84}{}{thm.2.2.4}{}}
\newlabel{thm:multicat-repr@cref}{{[thm][4][2,2]2.2.4}{[1][84][]84}}
\@writefile{brf}{\backcite{hermida:multicats,leinster:higher-opds}{{85}{2.2}{thm.2.2.4}}}
\newlabel{thm:multicat-prod}{{2.2.5}{85}{}{thm.2.2.5}{}}
\newlabel{thm:multicat-prod@cref}{{[thm][5][2,2]2.2.5}{[1][85][]85}}
\newlabel{thm:multicat-coprod}{{2.2.6}{85}{}{thm.2.2.6}{}}
\newlabel{thm:multicat-coprod@cref}{{[thm][6][2,2]2.2.6}{[1][85][]85}}
\newlabel{ex:multicat-defns}{{2.2.1}{86}{}{@ex.2.2.1}{}}
\newlabel{ex:multicat-defns@cref}{{[@ex][1][2,2]2.2.1}{[1][86][]86}}
\newlabel{ex:multicat-repr}{{2.2.2}{86}{}{@ex.2.2.2}{}}
\newlabel{ex:multicat-repr@cref}{{[@ex][2][2,2]2.2.2}{[1][86][]86}}
\newlabel{ex:mcat-lax-func}{{2.2.3}{86}{}{@ex.2.2.3}{}}
\newlabel{ex:mcat-lax-func@cref}{{[@ex][3][2,2]2.2.3}{[1][86][]86}}
\newlabel{ex:mcat-strong-func}{{2.2.4}{86}{}{@ex.2.2.4}{}}
\newlabel{ex:mcat-strong-func@cref}{{[@ex][4][2,2]2.2.4}{[1][86][]86}}
\newlabel{ex:multicat-coprod}{{2.2.5}{86}{}{@ex.2.2.5}{}}
\newlabel{ex:multicat-coprod@cref}{{[@ex][5][2,2]2.2.5}{[1][86][]86}}
\@writefile{toc}{\contentsline {section}{\numberline {2.3}Multiposets and monoidal posets}{86}{section.2.3}\protected@file@percent }
\newlabel{sec:multiposets-monpos}{{2.3}{86}{Multiposets and monoidal posets}{section.2.3}{}}
\newlabel{sec:multiposets-monpos@cref}{{[section][3][2]2.3}{[1][86][]86}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}Multiposets}{86}{subsection.2.3.1}\protected@file@percent }
\newlabel{sec:multiposets}{{2.3.1}{86}{Multiposets}{subsection.2.3.1}{}}
\newlabel{sec:multiposets@cref}{{[subsection][1][2,3]2.3.1}{[1][86][]86}}
\newlabel{thm:multiposet-cutadm}{{2.3.1}{87}{}{thm.2.3.1}{}}
\newlabel{thm:multiposet-cutadm@cref}{{[thm][1][2,3]2.3.1}{[1][87][]87}}
\newlabel{thm:multiposet-multicutadm}{{2.3.2}{87}{}{thm.2.3.2}{}}
\newlabel{thm:multiposet-multicutadm@cref}{{[thm][2][2,3]2.3.2}{[1][87][]87}}
\newlabel{thm:multiposet-initial}{{2.3.3}{87}{}{thm.2.3.3}{}}
\newlabel{thm:multiposet-initial@cref}{{[thm][3][2,3]2.3.3}{[1][87][]87}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Sequent calculus for monoidal posets}}{88}{figure.2.1}\protected@file@percent }
\newlabel{fig:seqcalc-monpos}{{2.1}{88}{Sequent calculus for monoidal posets}{figure.2.1}{}}
\newlabel{fig:seqcalc-monpos@cref}{{[figure][1][2]2.1}{[1][88][]88}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.2}Sequent calculus for monoidal posets}{88}{subsection.2.3.2}\protected@file@percent }
\newlabel{sec:seqcalc-monpos}{{2.3.2}{88}{Sequent calculus for monoidal posets}{subsection.2.3.2}{}}
\newlabel{sec:seqcalc-monpos@cref}{{[subsection][2][2,3]2.3.2}{[1][88][]88}}
\newlabel{thm:monpos-identity}{{2.3.4}{88}{}{thm.2.3.4}{}}
\newlabel{thm:monpos-identity@cref}{{[thm][4][2,3]2.3.4}{[1][88][]88}}
\newlabel{thm:monpos-cutadm}{{2.3.5}{89}{}{thm.2.3.5}{}}
\newlabel{thm:monpos-cutadm@cref}{{[thm][5][2,3]2.3.5}{[1][88][]89}}
\newlabel{eq:monpos-cutam-1}{{2.3.6}{89}{Sequent calculus for monoidal posets}{equation.2.3.6}{}}
\newlabel{eq:monpos-cutam-1@cref}{{[equation][6][2,3]2.3.6}{[1][89][]89}}
\newlabel{eq:monpos-cutam-2}{{2.3.7}{89}{Sequent calculus for monoidal posets}{equation.2.3.7}{}}
\newlabel{eq:monpos-cutam-2@cref}{{[equation][7][2,3]2.3.7}{[1][89][]89}}
\newlabel{thm:monpos-multicutadm}{{2.3.8}{90}{}{thm.2.3.8}{}}
\newlabel{thm:monpos-multicutadm@cref}{{[thm][8][2,3]2.3.8}{[1][90][]90}}
\newlabel{thm:monpos-initial}{{2.3.9}{91}{}{thm.2.3.9}{}}
\newlabel{thm:monpos-initial@cref}{{[thm][9][2,3]2.3.9}{[1][90][]91}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.3}Natural deduction for monoidal posets}{91}{subsection.2.3.3}\protected@file@percent }
\newlabel{sec:natded-monpos}{{2.3.3}{91}{Natural deduction for monoidal posets}{subsection.2.3.3}{}}
\newlabel{sec:natded-monpos@cref}{{[subsection][3][2,3]2.3.3}{[1][91][]91}}
\newlabel{rmk:context-splitting-1}{{2.3.10}{91}{}{rmk.2.3.10}{}}
\newlabel{rmk:context-splitting-1@cref}{{[rmk][10][]2.3.10}{[1][91][]91}}
\newlabel{ex:natded-monpos}{{2.3.1}{92}{}{@ex.2.3.1}{}}
\newlabel{ex:natded-monpos@cref}{{[@ex][1][2,3]2.3.1}{[1][92][]92}}
\newlabel{ex:monpos-invertible}{{2.3.2}{92}{}{@ex.2.3.2}{}}
\newlabel{ex:monpos-invertible@cref}{{[@ex][2][2,3]2.3.2}{[1][92][]92}}
\newlabel{ex:monpos-mslat}{{2.3.3}{92}{}{@ex.2.3.3}{}}
\newlabel{ex:monpos-mslat@cref}{{[@ex][3][2,3]2.3.3}{[1][92][]92}}
\newlabel{ex:monpos-jslat}{{2.3.4}{92}{}{@ex.2.3.4}{}}
\newlabel{ex:monpos-jslat@cref}{{[@ex][4][2,3]2.3.4}{[1][92][]92}}
\@writefile{toc}{\contentsline {section}{\numberline {2.4}Multicategories and monoidal categories}{93}{section.2.4}\protected@file@percent }
\newlabel{sec:multicat-moncat}{{2.4}{93}{Multicategories and monoidal categories}{section.2.4}{}}
\newlabel{sec:multicat-moncat@cref}{{[section][4][2]2.4}{[1][92][]93}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.1}Multicategories}{93}{subsection.2.4.1}\protected@file@percent }
\newlabel{sec:multicats}{{2.4.1}{93}{Multicategories}{subsection.2.4.1}{}}
\newlabel{sec:multicats@cref}{{[subsection][1][2,4]2.4.1}{[1][93][]93}}
\newlabel{thm:multicat-linear}{{2.4.2}{95}{}{lem.2.4.2}{}}
\newlabel{thm:multicat-linear@cref}{{[lem][2][]2.4.2}{[1][95][]95}}
\newlabel{thm:multicat-tad}{{2.4.3}{95}{}{lem.2.4.3}{}}
\newlabel{thm:multicat-tad@cref}{{[lem][3][]2.4.3}{[1][95][]95}}
\newlabel{thm:multicat-subadm}{{2.4.4}{96}{}{thm.2.4.4}{}}
\newlabel{thm:multicat-subadm@cref}{{[thm][4][2,4]2.4.4}{[1][96][]96}}
\newlabel{thm:multicat-subassoc}{{2.4.5}{96}{}{thm.2.4.5}{}}
\newlabel{thm:multicat-subassoc@cref}{{[thm][5][2,4]2.4.5}{[1][96][]96}}
\newlabel{item:multicat-subassoc-1}{{(a)}{96}{}{Item.113}{}}
\newlabel{item:multicat-subassoc-1@cref}{{[enumi][1][](a)}{[1][96][]96}}
\citation{leinster:higher-opds}
\newlabel{item:multicat-subassoc-2}{{(b)}{97}{}{Item.114}{}}
\newlabel{item:multicat-subassoc-2@cref}{{[enumi][2][](b)}{[1][96][]97}}
\@writefile{brf}{\backcite{leinster:higher-opds}{{97}{2.4.1}{Item.114}}}
\newlabel{thm:multicat-initial}{{2.4.6}{97}{}{thm.2.4.6}{}}
\newlabel{thm:multicat-initial@cref}{{[thm][6][2,4]2.4.6}{[1][97][]97}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4.2}Monoidal categories}{97}{subsection.2.4.2}\protected@file@percent }
\newlabel{sec:moncat}{{2.4.2}{97}{Monoidal categories}{subsection.2.4.2}{}}
\newlabel{sec:moncat@cref}{{[subsection][2][2,4]2.4.2}{[1][97][]97}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Simple type theory for monoidal categories}}{98}{figure.2.2}\protected@file@percent }
\newlabel{fig:moncat}{{2.2}{98}{Simple type theory for monoidal categories}{figure.2.2}{}}
\newlabel{fig:moncat@cref}{{[figure][2][2]2.2}{[1][98][]98}}
\newlabel{thm:moncat-linear}{{2.4.7}{98}{}{lem.2.4.7}{}}
\newlabel{thm:moncat-linear@cref}{{[lem][7][]2.4.7}{[1][98][]98}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces Substitution in the simple type theory for monoidal categories}}{99}{figure.2.3}\protected@file@percent }
\newlabel{fig:moncat-sub}{{2.3}{99}{Substitution in the simple type theory for monoidal categories}{figure.2.3}{}}
\newlabel{fig:moncat-sub@cref}{{[figure][3][2]2.3}{[1][99][]99}}
\newlabel{thm:moncat-tad}{{2.4.8}{99}{}{lem.2.4.8}{}}
\newlabel{thm:moncat-tad@cref}{{[lem][8][]2.4.8}{[1][98][]99}}
\newlabel{thm:moncat-subadm}{{2.4.9}{99}{}{lem.2.4.9}{}}
\newlabel{thm:moncat-subadm@cref}{{[lem][9][]2.4.9}{[1][99][]99}}
\newlabel{thm:moncat-initial}{{2.4.10}{100}{}{thm.2.4.10}{}}
\newlabel{thm:moncat-initial@cref}{{[thm][10][2,4]2.4.10}{[1][100][]100}}
\newlabel{rmk:moncat-pres}{{2.4.11}{101}{}{rmk.2.4.11}{}}
\newlabel{rmk:moncat-pres@cref}{{[rmk][11][]2.4.11}{[1][101][]101}}
\newlabel{ex:repmulticat-moncat}{{2.4.1}{101}{}{@ex.2.4.1}{}}
\newlabel{ex:repmulticat-moncat@cref}{{[@ex][1][2,4]2.4.1}{[1][101][]101}}
\newlabel{ex:moncat-multisubadm}{{2.4.2}{101}{}{@ex.2.4.2}{}}
\newlabel{ex:moncat-multisubadm@cref}{{[@ex][2][2,4]2.4.2}{[1][101][]101}}
\newlabel{ex:moncat-context-splitting}{{2.4.3}{101}{}{@ex.2.4.3}{}}
\newlabel{ex:moncat-context-splitting@cref}{{[@ex][3][2,4]2.4.3}{[1][101][]101}}
\newlabel{item:moncat-context-splitting-1}{{(a)}{101}{}{Item.115}{}}
\newlabel{item:moncat-context-splitting-1@cref}{{[enumi][1][](a)}{[1][101][]101}}
\newlabel{ex:debruijn-context-concat}{{2.4.4}{101}{}{@ex.2.4.4}{}}
\newlabel{ex:debruijn-context-concat@cref}{{[@ex][4][2,4]2.4.4}{[1][101][]101}}
\@writefile{toc}{\contentsline {section}{\numberline {2.5}Adding products and coproducts}{101}{section.2.5}\protected@file@percent }
\newlabel{sec:multicat-prod-coprod}{{2.5}{101}{Adding products and coproducts}{section.2.5}{}}
\newlabel{sec:multicat-prod-coprod@cref}{{[section][5][2]2.5}{[1][101][]101}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Distributive monoidal categories with products}}{102}{figure.2.4}\protected@file@percent }
\newlabel{fig:moncat-prod-coprod}{{2.4}{102}{Distributive monoidal categories with products}{figure.2.4}{}}
\newlabel{fig:moncat-prod-coprod@cref}{{[figure][4][2]2.4}{[1][102][]102}}
\newlabel{thm:moncat-prod-coprod-superlin}{{2.5.1}{103}{}{lem.2.5.1}{}}
\newlabel{thm:moncat-prod-coprod-superlin@cref}{{[lem][1][]2.5.1}{[1][103][]103}}
\newlabel{thm:moncat-prod-coprod-tad}{{2.5.2}{103}{}{lem.2.5.2}{}}
\newlabel{thm:moncat-prod-coprod-tad@cref}{{[lem][2][]2.5.2}{[1][103][]103}}
\newlabel{eq:ttt-arg}{{2.5.3}{103}{Adding products and coproducts}{equation.2.5.3}{}}
\newlabel{eq:ttt-arg@cref}{{[equation][3][2,5]2.5.3}{[1][103][]103}}
\newlabel{thm:moncat-prod-coprod-subadm}{{2.5.4}{103}{}{thm.2.5.4}{}}
\newlabel{thm:moncat-prod-coprod-subadm@cref}{{[thm][4][2,5]2.5.4}{[1][103][]103}}
\newlabel{thm:moncat-prod-coprod-initial}{{2.5.5}{103}{}{thm.2.5.5}{}}
\newlabel{thm:moncat-prod-coprod-initial@cref}{{[thm][5][2,5]2.5.5}{[1][103][]103}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.5}{\ignorespaces Substitution for distributive monoidal categories with products}}{104}{figure.2.5}\protected@file@percent }
\newlabel{fig:moncat-prod-coprod-sub}{{2.5}{104}{Substitution for distributive monoidal categories with products}{figure.2.5}{}}
\newlabel{fig:moncat-prod-coprod-sub@cref}{{[figure][5][2]2.5}{[1][103][]104}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.6}{\ignorespaces Equality rules for distributive monoidal categories with products}}{104}{figure.2.6}\protected@file@percent }
\newlabel{fig:moncat-prod-coprod-equiv}{{2.6}{104}{Equality rules for distributive monoidal categories with products}{figure.2.6}{}}
\newlabel{fig:moncat-prod-coprod-equiv@cref}{{[figure][6][2]2.6}{[1][103][]104}}
\newlabel{ex:moncat-prod-coprod-context}{{2.5.1}{105}{}{@ex.2.5.1}{}}
\newlabel{ex:moncat-prod-coprod-context@cref}{{[@ex][1][2,5]2.5.1}{[1][105][]105}}
\@writefile{toc}{\contentsline {section}{\numberline {2.6}Some generalized multicategories}{105}{section.2.6}\protected@file@percent }
\newlabel{sec:cartmulti}{{2.6}{105}{Some generalized multicategories}{section.2.6}{}}
\newlabel{sec:cartmulti@cref}{{[section][6][2]2.6}{[1][105][]105}}
\newlabel{eq:symm-multicat-action}{{2.6.1}{105}{Some generalized multicategories}{equation.2.6.1}{}}
\newlabel{eq:symm-multicat-action@cref}{{[equation][1][2,6]2.6.1}{[1][105][]105}}
\newlabel{eq:cartmulticat-action}{{2.6.2}{105}{Some generalized multicategories}{equation.2.6.2}{}}
\newlabel{eq:cartmulticat-action@cref}{{[equation][2][2,6]2.6.2}{[1][105][]105}}
\citation{dp:relevant-cats}
\@writefile{brf}{\backcite{dp:relevant-cats}{{106}{(d)}{Item.120}}}
\newlabel{defn:fS-multicategory}{{2.6.4}{106}{}{defn.2.6.4}{}}
\newlabel{defn:fS-multicategory@cref}{{[defn][4][]2.6.4}{[1][106][]106}}
\newlabel{item:cartmulti-1}{{(a)}{106}{}{Item.124}{}}
\newlabel{item:cartmulti-1@cref}{{[enumi][1][](a)}{[1][106][]106}}
\newlabel{item:cartmulti-2}{{(b)}{106}{}{Item.125}{}}
\newlabel{item:cartmulti-2@cref}{{[enumi][2][](b)}{[1][106][]106}}
\newlabel{item:cartmulti-3}{{(c)}{106}{}{Item.126}{}}
\newlabel{item:cartmulti-3@cref}{{[enumi][3][](c)}{[1][106][]106}}
\newlabel{item:cartmulti-4}{{(d)}{107}{}{Item.127}{}}
\newlabel{item:cartmulti-4@cref}{{[enumi][4][](d)}{[1][106][]107}}
\newlabel{thm:symm-multicat-repr}{{2.6.5}{107}{}{thm.2.6.5}{}}
\newlabel{thm:symm-multicat-repr@cref}{{[thm][5][2,6]2.6.5}{[1][107][]107}}
\newlabel{thm:semicart-multicat-repr}{{2.6.6}{107}{}{thm.2.6.6}{}}
\newlabel{thm:semicart-multicat-repr@cref}{{[thm][6][2,6]2.6.6}{[1][107][]107}}
\citation{street:absolute}
\newlabel{thm:cart-multicat-repr}{{2.6.7}{108}{}{thm.2.6.7}{}}
\newlabel{thm:cart-multicat-repr@cref}{{[thm][7][2,6]2.6.7}{[1][108][]108}}
\newlabel{rmk:absolute}{{2.6.8}{108}{}{rmk.2.6.8}{}}
\newlabel{rmk:absolute@cref}{{[rmk][8][]2.6.8}{[1][108][]108}}
\citation{dp:relevant-cats}
\@writefile{brf}{\backcite{street:absolute}{{109}{2.6.8}{rmk.2.6.8}}}
\newlabel{thm:moncat-repr-closed}{{2.6.9}{109}{}{thm.2.6.9}{}}
\newlabel{thm:moncat-repr-closed@cref}{{[thm][9][2,6]2.6.9}{[1][109][]109}}
\newlabel{ex:gen-multicat-repr}{{2.6.1}{109}{}{@ex.2.6.1}{}}
\newlabel{ex:gen-multicat-repr@cref}{{[@ex][1][2,6]2.6.1}{[1][109][]109}}
\newlabel{ex:club-generators}{{2.6.2}{109}{}{@ex.2.6.2}{}}
\newlabel{ex:club-generators@cref}{{[@ex][2][2,6]2.6.2}{[1][109][]109}}
\newlabel{ex:cartmulti-oneplace}{{2.6.3}{109}{}{@ex.2.6.3}{}}
\newlabel{ex:cartmulti-oneplace@cref}{{[@ex][3][2,6]2.6.3}{[1][109][]109}}
\newlabel{ex:distrib}{{2.6.4}{109}{}{@ex.2.6.4}{}}
\newlabel{ex:distrib@cref}{{[@ex][4][2,6]2.6.4}{[1][109][]109}}
\newlabel{ex:absolute}{{2.6.5}{109}{}{@ex.2.6.5}{}}
\newlabel{ex:absolute@cref}{{[@ex][5][2,6]2.6.5}{[1][109][]109}}
\newlabel{ex:relevance-moncat}{{2.6.6}{110}{}{@ex.2.6.6}{}}
\newlabel{ex:relevance-moncat@cref}{{[@ex][6][2,6]2.6.6}{[1][109][]110}}
\@writefile{brf}{\backcite{dp:relevant-cats}{{110}{2.6.6}{@ex.2.6.6}}}
\newlabel{ex:cocartesian-clubs}{{2.6.7}{110}{}{@ex.2.6.7}{}}
\newlabel{ex:cocartesian-clubs@cref}{{[@ex][7][2,6]2.6.7}{[1][109][]110}}
\@writefile{toc}{\contentsline {section}{\numberline {2.7}Intuitionistic logic}{110}{section.2.7}\protected@file@percent }
\newlabel{sec:logic}{{2.7}{110}{Intuitionistic logic}{section.2.7}{}}
\newlabel{sec:logic@cref}{{[section][7][2]2.7}{[1][110][]110}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7.1}\ensuremath  {\mathfrak  {S}}\xspace  -monoidal lattices}{110}{subsection.2.7.1}\protected@file@percent }
\newlabel{sec:monoidal-lattices}{{2.7.1}{110}{\fS -monoidal lattices}{subsection.2.7.1}{}}
\newlabel{sec:monoidal-lattices@cref}{{[subsection][1][2,7]2.7.1}{[1][110][]110}}
\newlabel{thm:natded-logic-cutadm}{{2.7.1}{111}{}{lem.2.7.1}{}}
\newlabel{thm:natded-logic-cutadm@cref}{{[lem][1][]2.7.1}{[1][111][]111}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.7}{\ignorespaces Natural deduction for closed \ensuremath  {\mathfrak  {S}}\xspace  -monoidal lattices}}{112}{figure.2.7}\protected@file@percent }
\newlabel{fig:natded-logic}{{2.7}{112}{Natural deduction for closed \fS -monoidal lattices}{figure.2.7}{}}
\newlabel{fig:natded-logic@cref}{{[figure][7][2]2.7}{[1][111][]112}}
\newlabel{thm:natded-logic-multicutadm}{{2.7.2}{113}{}{lem.2.7.2}{}}
\newlabel{thm:natded-logic-multicutadm@cref}{{[lem][2][]2.7.2}{[1][113][]113}}
\newlabel{thm:natded-logic-initial}{{2.7.3}{113}{}{thm.2.7.3}{}}
\newlabel{thm:natded-logic-initial@cref}{{[thm][3][2,7]2.7.3}{[1][113][]113}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7.2}Heyting algebras}{114}{subsection.2.7.2}\protected@file@percent }
\newlabel{sec:heyting-algebras}{{2.7.2}{114}{Heyting algebras}{subsection.2.7.2}{}}
\newlabel{sec:heyting-algebras@cref}{{[subsection][2][2,7]2.7.2}{[1][114][]114}}
\newlabel{thm:cart-constctx}{{2.7.4}{114}{}{lem.2.7.4}{}}
\newlabel{thm:cart-constctx@cref}{{[lem][4][]2.7.4}{[1][114][]114}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.8}{\ignorespaces Natural deduction for Heyting algebras}}{115}{figure.2.8}\protected@file@percent }
\newlabel{fig:natded-heyting}{{2.8}{115}{Natural deduction for Heyting algebras}{figure.2.8}{}}
\newlabel{fig:natded-heyting@cref}{{[figure][8][2]2.8}{[1][115][]115}}
\newlabel{thm:heyting-strucadm}{{2.7.5}{115}{}{lem.2.7.5}{}}
\newlabel{thm:heyting-strucadm@cref}{{[lem][5][]2.7.5}{[1][115][]115}}
\newlabel{thm:heyting-initial}{{2.7.6}{116}{}{lem.2.7.6}{}}
\newlabel{thm:heyting-initial@cref}{{[lem][6][]2.7.6}{[1][116][]116}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7.3}Natural deduction and logic}{116}{subsection.2.7.3}\protected@file@percent }
\newlabel{sec:natded-logic}{{2.7.3}{116}{Natural deduction and logic}{subsection.2.7.3}{}}
\newlabel{sec:natded-logic@cref}{{[subsection][3][2,7]2.7.3}{[1][116][]116}}
\citation{wadler:pat}
\newlabel{rmk:soundness-completeness}{{2.7.8}{119}{}{rmk.2.7.8}{}}
\newlabel{rmk:soundness-completeness@cref}{{[rmk][8][]2.7.8}{[1][119][]119}}
\@writefile{brf}{\backcite{wadler:pat}{{119}{2.7.3}{rmk.2.7.8}}}
\newlabel{ex:cart-typetheory}{{2.7.1}{121}{}{@ex.2.7.1}{}}
\newlabel{ex:cart-typetheory@cref}{{[@ex][1][2,7]2.7.1}{[1][120][]121}}
\newlabel{ex:nnlem}{{2.7.2}{121}{}{@ex.2.7.2}{}}
\newlabel{ex:nnlem@cref}{{[@ex][2][2,7]2.7.2}{[1][121][]121}}
\newlabel{ex:heyt-bool}{{2.7.3}{121}{}{@ex.2.7.3}{}}
\newlabel{ex:heyt-bool@cref}{{[@ex][3][2,7]2.7.3}{[1][121][]121}}
\newlabel{ex:demorgan}{{2.7.4}{121}{}{@ex.2.7.4}{}}
\newlabel{ex:demorgan@cref}{{[@ex][4][2,7]2.7.4}{[1][121][]121}}
\newlabel{ex:frames}{{2.7.5}{121}{}{@ex.2.7.5}{}}
\newlabel{ex:frames@cref}{{[@ex][5][2,7]2.7.5}{[1][121][]121}}
\newlabel{ex:not-lem}{{2.7.6}{121}{}{@ex.2.7.6}{}}
\newlabel{ex:not-lem@cref}{{[@ex][6][2,7]2.7.6}{[1][121][]121}}
\newlabel{ex:relevance-eg}{{2.7.7}{121}{}{@ex.2.7.7}{}}
\newlabel{ex:relevance-eg@cref}{{[@ex][7][2,7]2.7.7}{[1][121][]121}}
\newlabel{ex:seqcalc-logic}{{2.7.8}{122}{}{@ex.2.7.8}{}}
\newlabel{ex:seqcalc-logic@cref}{{[@ex][8][2,7]2.7.8}{[1][121][]122}}
\newlabel{ex:hilbert}{{2.7.9}{122}{}{@ex.2.7.9}{}}
\newlabel{ex:hilbert@cref}{{[@ex][9][2,7]2.7.9}{[1][122][]122}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.9}{\ignorespaces The simply typed $\ensuremath  {\your@lambda }\xspace  $-calculus with products and coproducts}}{123}{figure.2.9}\protected@file@percent }
\newlabel{fig:stlc}{{2.9}{123}{The simply typed $\lambda $-calculus with products and coproducts}{figure.2.9}{}}
\newlabel{fig:stlc@cref}{{[figure][9][2]2.9}{[1][123][]123}}
\newlabel{ex:cocartesian-typetheory}{{2.7.10}{123}{}{@ex.2.7.10}{}}
\newlabel{ex:cocartesian-typetheory@cref}{{[@ex][10][2,7]2.7.10}{[1][122][]123}}
\@writefile{toc}{\contentsline {section}{\numberline {2.8}Simply typed $\ensuremath  {\your@lambda }\xspace  $-calculus}{123}{section.2.8}\protected@file@percent }
\newlabel{sec:stlc}{{2.8}{123}{Simply typed $\lambda $-calculus}{section.2.8}{}}
\newlabel{sec:stlc@cref}{{[section][8][2]2.8}{[1][123][]123}}
\newlabel{thm:stlc-uniqderiv}{{2.8.1}{124}{}{lem.2.8.1}{}}
\newlabel{thm:stlc-uniqderiv@cref}{{[lem][1][]2.8.1}{[1][124][]124}}
\newlabel{thm:stlc-strucadm}{{2.8.2}{124}{}{lem.2.8.2}{}}
\newlabel{thm:stlc-strucadm@cref}{{[lem][2][]2.8.2}{[1][124][]124}}
\newlabel{thm:stlc-subadm}{{2.8.4}{125}{}{lem.2.8.4}{}}
\newlabel{thm:stlc-subadm@cref}{{[lem][4][]2.8.4}{[1][125][]125}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.10}{\ignorespaces Substitution in simply typed $\ensuremath  {\your@lambda }\xspace  $-calculus}}{126}{figure.2.10}\protected@file@percent }
\newlabel{fig:stlc-sub}{{2.10}{126}{Substitution in simply typed $\lambda $-calculus}{figure.2.10}{}}
\newlabel{fig:stlc-sub@cref}{{[figure][10][2]2.10}{[1][125][]126}}
\newlabel{thm:stlc-subassoc}{{2.8.5}{126}{}{lem.2.8.5}{}}
\newlabel{thm:stlc-subassoc@cref}{{[lem][5][]2.8.5}{[1][126][]126}}
\newlabel{eq:sub-contr-1}{{2.8.6}{127}{Simply typed $\lambda $-calculus}{equation.2.8.6}{}}
\newlabel{eq:sub-contr-1@cref}{{[equation][6][2,8]2.8.6}{[1][127][]127}}
\newlabel{eq:sub-contr-2}{{2.8.7}{127}{Simply typed $\lambda $-calculus}{equation.2.8.7}{}}
\newlabel{eq:sub-contr-2@cref}{{[equation][7][2,8]2.8.7}{[1][127][]127}}
\newlabel{thm:stlc-initial}{{2.8.8}{127}{}{thm.2.8.8}{}}
\newlabel{thm:stlc-initial@cref}{{[thm][8][2,8]2.8.8}{[1][127][]127}}
\newlabel{rmk:ctx-judgment}{{2.8.9}{128}{}{rmk.2.8.9}{}}
\newlabel{rmk:ctx-judgment@cref}{{[rmk][9][]2.8.9}{[1][128][]128}}
\newlabel{ex:stlc-cartmulti}{{2.8.1}{129}{}{@ex.2.8.1}{}}
\newlabel{ex:stlc-cartmulti@cref}{{[@ex][1][2,8]2.8.1}{[1][128][]129}}
\newlabel{ex:church-numerals}{{2.8.2}{129}{}{@ex.2.8.2}{}}
\newlabel{ex:church-numerals@cref}{{[@ex][2][2,8]2.8.2}{[1][129][]129}}
\newlabel{ex:combinatory-logic}{{2.8.3}{129}{}{@ex.2.8.3}{}}
\newlabel{ex:combinatory-logic@cref}{{[@ex][3][2,8]2.8.3}{[1][129][]129}}
\newlabel{item:cl1}{{(a)}{129}{}{Item.150}{}}
\newlabel{item:cl1@cref}{{[enumi][1][](a)}{[1][129][]129}}
\newlabel{item:cl2}{{(b)}{129}{}{Item.151}{}}
\newlabel{item:cl2@cref}{{[enumi][2][](b)}{[1][129][]129}}
\@writefile{toc}{\contentsline {section}{\numberline {2.9}Cartesian presentations}{130}{section.2.9}\protected@file@percent }
\newlabel{sec:cartesian-presentations}{{2.9}{130}{Cartesian presentations}{section.2.9}{}}
\newlabel{sec:cartesian-presentations@cref}{{[section][9][2]2.9}{[1][129][]130}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.9.1}Finite-product theories}{130}{subsection.2.9.1}\protected@file@percent }
\newlabel{sec:fp-theories}{{2.9.1}{130}{Finite-product theories}{subsection.2.9.1}{}}
\newlabel{sec:fp-theories@cref}{{[subsection][1][2,9]2.9.1}{[1][130][]130}}
\newlabel{thm:free-Smoncat-Smulti}{{2.9.1}{131}{}{thm.2.9.1}{}}
\newlabel{thm:free-Smoncat-Smulti@cref}{{[thm][1][2,9]2.9.1}{[1][131][]131}}
\citation{lawvere:functsem}
\@writefile{brf}{\backcite{lawvere:functsem}{{132}{2.9.1}{thm.2.9.1}}}
\citation{bkp:2dmonads}
\citation{lawvere:functsem}
\newlabel{thm:free-catprod-cartmulti}{{2.9.2}{133}{}{thm.2.9.2}{}}
\newlabel{thm:free-catprod-cartmulti@cref}{{[thm][2][2,9]2.9.2}{[1][132][]133}}
\@writefile{brf}{\backcite{bkp:2dmonads}{{133}{2.9.1}{thm.2.9.2}}}
\@writefile{brf}{\backcite{lawvere:functsem}{{133}{2.9.1}{thm.2.9.2}}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.9.2}Presheaves on multicategories}{133}{subsection.2.9.2}\protected@file@percent }
\newlabel{sec:multicat-pshf}{{2.9.2}{133}{Presheaves on multicategories}{subsection.2.9.2}{}}
\newlabel{sec:multicat-pshf@cref}{{[subsection][2][2,9]2.9.2}{[1][133][]133}}
\newlabel{defn:multicat-pshf}{{2.9.4}{133}{}{defn.2.9.4}{}}
\newlabel{defn:multicat-pshf@cref}{{[defn][4][]2.9.4}{[1][133][]133}}
\newlabel{thm:multicat-pshf-catctx}{{2.9.5}{134}{}{thm.2.9.5}{}}
\newlabel{thm:multicat-pshf-catctx@cref}{{[thm][5][2,9]2.9.5}{[1][134][]134}}
\newlabel{thm:multicat-yoneda}{{2.9.6}{134}{}{cor.2.9.6}{}}
\newlabel{thm:multicat-yoneda@cref}{{[cor][6][]2.9.6}{[1][134][]134}}
\citation{lambek:stlc-ccc}
\@writefile{brf}{\backcite{lambek:stlc-ccc}{{135}{2.9.2}{Item.166}}}
\newlabel{ex:catprod-ehnr-again}{{2.9.1}{136}{}{@ex.2.9.1}{}}
\newlabel{ex:catprod-ehnr-again@cref}{{[@ex][1][2,9]2.9.1}{[1][135][]136}}
\newlabel{ex:catprod-thy-noprod}{{2.9.2}{136}{}{@ex.2.9.2}{}}
\newlabel{ex:catprod-thy-noprod@cref}{{[@ex][2][2,9]2.9.2}{[1][135][]136}}
\newlabel{ex:free-Smoncat-Smulti}{{2.9.3}{136}{}{@ex.2.9.3}{}}
\newlabel{ex:free-Smoncat-Smulti@cref}{{[@ex][3][2,9]2.9.3}{[1][136][]136}}
\newlabel{ex:free-catprod-cartmulti}{{2.9.4}{136}{}{@ex.2.9.4}{}}
\newlabel{ex:free-catprod-cartmulti@cref}{{[@ex][4][2,9]2.9.4}{[1][136][]136}}
\newlabel{ex:catctx-ctxjdg}{{2.9.5}{136}{}{@ex.2.9.5}{}}
\newlabel{ex:catctx-ctxjdg@cref}{{[@ex][5][2,9]2.9.5}{[1][136][]136}}
\@writefile{toc}{\contentsline {section}{\numberline {2.10}Symmetric monoidal categories}{136}{section.2.10}\protected@file@percent }
\newlabel{sec:symmoncat}{{2.10}{136}{Symmetric monoidal categories}{section.2.10}{}}
\newlabel{sec:symmoncat@cref}{{[section][10][2]2.10}{[1][136][]136}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.10.1}Shuffles}{136}{subsection.2.10.1}\protected@file@percent }
\newlabel{sec:shuffles}{{2.10.1}{136}{Shuffles}{subsection.2.10.1}{}}
\newlabel{sec:shuffles@cref}{{[subsection][1][2,10]2.10.1}{[1][136][]136}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.11}{\ignorespaces Type theory for symmetric monoidal categories}}{138}{figure.2.11}\protected@file@percent }
\newlabel{fig:smc}{{2.11}{138}{Type theory for symmetric monoidal categories}{figure.2.11}{}}
\newlabel{fig:smc@cref}{{[figure][11][2]2.11}{[1][137][]138}}
\newlabel{thm:smc-exchadm}{{2.10.3}{139}{}{lem.2.10.3}{}}
\newlabel{thm:smc-exchadm@cref}{{[lem][3][]2.10.3}{[1][137][]139}}
\newlabel{thm:smc-superlin}{{2.10.4}{139}{}{lem.2.10.4}{}}
\newlabel{thm:smc-superlin@cref}{{[lem][4][]2.10.4}{[1][139][]139}}
\newlabel{thm:smc-tad}{{2.10.5}{139}{}{lem.2.10.5}{}}
\newlabel{thm:smc-tad@cref}{{[lem][5][]2.10.5}{[1][139][]139}}
\citation{leinster:higher-opds}
\citation{may:goils}
\citation{leinster:higher-opds}
\@writefile{brf}{\backcite{leinster:higher-opds}{{140}{2.10.1}{lem.2.10.5}}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.10.2}Symmetric $\tensor $-presentations}{140}{subsection.2.10.2}\protected@file@percent }
\newlabel{sec:symm-tensor-pres}{{2.10.2}{140}{Symmetric $\tensor $-presentations}{subsection.2.10.2}{}}
\newlabel{sec:symm-tensor-pres@cref}{{[subsection][2][2,10]2.10.2}{[1][140][]140}}
\@writefile{brf}{\backcite{may:goils}{{140}{2.10.2}{subsection.2.10.2}}}
\@writefile{brf}{\backcite{leinster:higher-opds}{{140}{2.10.2}{subsection.2.10.2}}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.12}{\ignorespaces Axioms for a bimonoid}}{141}{figure.2.12}\protected@file@percent }
\newlabel{fig:smc-bimonoid}{{2.12}{141}{Axioms for a bimonoid}{figure.2.12}{}}
\newlabel{fig:smc-bimonoid@cref}{{[figure][12][2]2.12}{[1][141][]141}}
\newlabel{thm:multicat-day}{{2.10.6}{141}{}{thm.2.10.6}{}}
\newlabel{thm:multicat-day@cref}{{[thm][6][2,10]2.10.6}{[1][141][]141}}
\citation{day:closed}
\newlabel{ex:smc}{{2.10.1}{143}{}{@ex.2.10.1}{}}
\newlabel{ex:smc@cref}{{[@ex][1][2,10]2.10.1}{[1][143][]143}}
\newlabel{ex:multicat-day}{{2.10.2}{143}{}{@ex.2.10.2}{}}
\newlabel{ex:multicat-day@cref}{{[@ex][2][2,10]2.10.2}{[1][143][]143}}
\@writefile{brf}{\backcite{day:closed}{{143}{2.10.2}{@ex.2.10.2}}}
\newlabel{ex:moncat-pres}{{2.10.3}{143}{}{@ex.2.10.3}{}}
\newlabel{ex:moncat-pres@cref}{{[@ex][3][2,10]2.10.3}{[1][143][]143}}
\newlabel{ex:smc-usage}{{2.10.4}{143}{}{@ex.2.10.4}{}}
\newlabel{ex:smc-usage@cref}{{[@ex][4][2,10]2.10.4}{[1][143][]143}}
\newlabel{ex:semicart-relevance-strucadm}{{2.10.5}{143}{}{@ex.2.10.5}{}}
\newlabel{ex:semicart-relevance-strucadm@cref}{{[@ex][5][2,10]2.10.5}{[1][143][]143}}
\citation{dp:relevant-cats}
\@writefile{brf}{\backcite{dp:relevant-cats}{{145}{2.10.2}{Item.190}}}
\citation{day:closed}
\@writefile{brf}{\backcite{day:closed}{{149}{2.10.2}{Item.209}}}
\@setckpt{simple}{
\setcounter{page}{150}
\setcounter{equation}{6}
\setcounter{enumi}{3}
\setcounter{enumii}{2}
\setcounter{enumiii}{0}
\setcounter{enumiv}{0}
\setcounter{footnote}{5}
\setcounter{mpfootnote}{0}
\setcounter{part}{0}
\setcounter{chapter}{2}
\setcounter{section}{10}
\setcounter{subsection}{2}
\setcounter{subsubsection}{0}
\setcounter{paragraph}{0}
\setcounter{subparagraph}{0}
\setcounter{figure}{12}
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{section@level}{2}
\setcounter{Item}{212}
\setcounter{Hfootnote}{16}
\setcounter{bookmark@seq@number}{45}
\setcounter{thm}{6}
\setcounter{@ex}{5}
}