\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{coherence theorem}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{higher_category_theory}{}\paragraph*{{Higher category theory}}\label{higher_category_theory}

[[!include higher category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{descriptions_of_free_algebras}{Descriptions of free algebras}\dotfill \pageref*{descriptions_of_free_algebras} \linebreak
\noindent\hyperlink{strictification}{Strictification}\dotfill \pageref*{strictification} \linebreak
\noindent\hyperlink{relating_coherence_theorems}{Relating coherence theorems}\dotfill \pageref*{relating_coherence_theorems} \linebreak
\noindent\hyperlink{ListOfTheorems}{List of coherence theorems}\dotfill \pageref*{ListOfTheorems} \linebreak
\noindent\hyperlink{general_frameworks_for_coherence_theorems}{General frameworks for coherence theorems}\dotfill \pageref*{general_frameworks_for_coherence_theorems} \linebreak
\noindent\hyperlink{2monads}{2-monads}\dotfill \pageref*{2monads} \linebreak
\noindent\hyperlink{operads}{Operads}\dotfill \pageref*{operads} \linebreak
\noindent\hyperlink{clubs}{Clubs}\dotfill \pageref*{clubs} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Generally, a \textbf{coherence theorem} in [[category theory]] and [[higher category theory]] asserts that a [[coherence law]] is satisfied: it is a means of getting a handle on categorical structures where laws only hold up to [[isomorphism]] or higher [[k-morphism]] equivalences. Precisely, it can mean one of several slightly different things.

\hypertarget{descriptions_of_free_algebras}{}\subsubsection*{{Descriptions of free algebras}}\label{descriptions_of_free_algebras}

Given a [[doctrine]], such as the doctrine for monoidal categories, a coherence theorem may provide a full or partial algorithm for deciding equality in free algebras. Usually such a doctrine is specified only by certain ``generating'' operations and constraint morphisms between them; the coherence question then consists in determining exactly what additional operations and morphisms are derivable from these, and in particular when two such derived morphisms are equal. For instance, one may be interested in the coherence problem for closed categories: how does one decide equality of morphisms in freely generated closed categories, or in other words, how does one decide which diagrams (generated from the closed structure) commute?

The first, and perhaps easiest, coherence theorem is Mac Lane's, which says that in a free [[monoidal category]], \emph{every} diagram of constraint morphisms commutes. The especially nice form of this theorem should not lead one to expect that all coherence theorems are of the form ``every diagram commutes''---in many categorical structures, it is \emph{not} the case that all diagrams of constraints commute, and so the coherence question must address more precisely \emph{which} diagrams of constraints commute. For instance, in a [[braided monoidal category]] not every diagram of constraints commutes, but the coherence theorem gives a concise classification of those that do in terms of their underlying braids.

This sort of coherence theorem is often the most useful when actually working with algebras in a doctrine, since it provides a way to tell whether two particular composites of constraints which may arise in practice are actually equal. One should beware, however, that coherence theorems only relate to the behavior of \emph{free} algebras, or equivalently to the equality of \emph{formally defined} composites. Even in a structure having a coherence theorem of the ``every diagram commutes'' sort, it may happen in a \emph{particular} algebra that there exist diagrams of constraints which do not commute. For instance, one can find a monoidal category containing objects $x,y,z$ such that $x\otimes (y\otimes z) = (x\otimes y)\otimes z$ on the nose, but such that the [[associator]] isomorphism $a_{x,y,z}:x\otimes (y\otimes z) \stackrel{\simeq}{\to} (x\otimes y)\otimes z$ is not the identity. (For example, [[skeletons]] of naturally occurring monoidal categories often have this property. This issue also arises in the classification of [[2-groups]] via cohomology.)

\hypertarget{strictification}{}\subsubsection*{{Strictification}}\label{strictification}

On the other hand, given a doctrine for ``weak'' categorical structures of some sort, a coherence theorem may provide a means for fully or partially strictifying such structures, to the effect that every weak structure is weakly equivalent to a strictified structure. The applicable version of Mac Lane's original coherence theorem here is that every monoidal category is (monoidally) equivalent to a \emph{strict} monoidal category. Similarly, every [[bicategory]] is equivalent to a [[strict 2-category]].

As before, one should not be misled by these examples into thinking that all coherence theorems are of the form ``every weak thing is equivalent to a strict thing.'' For example, the strictification coherence theorem for symmetric monoidal categories states that every symmetric monoidal category is symmetric-monoidally equivalent, not to a commutative monoid in $Cat$, but to a symmetric strict monoidal category, whose monoidal structure is strict but whose symmetry is not. This may be regarded as a ``partial'' or ``semi-''strictification result.

Naturally, it should not be thought that coherence problems are restricted to 1-category theory. For instance, the main result in Gordon, Power and Street's \emph{Coherence for Tricategories} is that every [[tricategory]] is equivalent (not to a [[strict 3-category]] but) to a [[Gray-category]]. This is another example of a semi-strictification result, and is the tip of an iceberg of hoped-for further coherence theorems for algebraic notions of $n$-category.

\hypertarget{relating_coherence_theorems}{}\subsubsection*{{Relating coherence theorems}}\label{relating_coherence_theorems}

These two senses of ``coherence theorem'' are connected, of course. On the one hand, an explicit description of the free algebras for a doctrine is often helpful, if not essential, in proving a strictification result, since in a strict structure where constraints become equalities, many more diagrams will turn out to commute (being composed of identities). On the other hand, given a strictification theorem, if we have an explicit description of the strict structure (which is generally easier to come by), we can often deduce a characterization of the free algebras for the weak structure.

One thing to beware of is that even for structures whose free-algebra coherence theorem is of the form ``all diagrams commute,'' it does not necessarily follow that all such algebras can be fully strictified.

\hypertarget{ListOfTheorems}{}\subsection*{{List of coherence theorems}}\label{ListOfTheorems}

\begin{itemize}%
\item [[coherence theorem for monoidal categories]]


\item [[coherence theorem for symmetric monoidal categories]]


\item [[coherence theorem for braided monoidal categories]]


\item [[coherence theorem for tortile categories]]


\item [[coherence theorem for closed symmetric monoidal categories]]


\item \href{/nlab/show/bicategory#Coherence}{coherence theorem for bicategories}


\item [[Lack's coherence theorem]] (not a true coherence theorem)


\item \href{/nlab/show/tricategory#Coherence}{coherence theorem for tricategories}


\item [[coherence theorem for bicategories with finite limits]]


\item [[coherence theorem for monoidal bicategories]]


\item [[coherence theorem for braided monoidal bicategories]]


\item [[coherence theorem for symmetric monoidal bicategories]]



\end{itemize}
\hypertarget{general_frameworks_for_coherence_theorems}{}\subsection*{{General frameworks for coherence theorems}}\label{general_frameworks_for_coherence_theorems}

There exist several general frameworks for describing ``doctrines'' or algebraic structures on categories, which can be used to describe free algebras and state coherence theorems. All are closely related.

\hypertarget{2monads}{}\subsubsection*{{2-monads}}\label{2monads}

A [[2-monad]] can be regarded as the ``extensional essence'' of an algebraic structure on categories (or on objects of some other 2-category). Of course, if $T$ is a 2-monad describing some structure, then $T A$ is the free such structure on $A$; thus the first sort of coherence theorem can be precisely stated as ``describe $T A$ as explicitly as possible in terms of $A$.''

However, the notion of monad is so general that in practice, for proving coherence theorems it is useful to have a more explicit way of ``presenting'' a monad in terms of generating operations and relations; this is the purpose of the structures presented below, such as [[operads]] and [[clubs]]. Not all monads can be presented in such a more explicit way, but for those that can, it is a very useful simplification.

The notion of \emph{strict} 2-monad on a [[strict 2-category]] also provides a general way to state a strictification theorem, although one must beware that this theorem is not always true, and when it is true, it doesn't necessarily give what one was looking for. This general ``coherence theorem schema'' for a 2-monad $T$ would be that every [[pseudoalgebra for a 2-monad|pseudo]] $T$-algebra is equivalent to a strict one. A stronger statement, which is true in most cases when the weaker version is, would be that the inclusion

\begin{displaymath}
Str T Alg \hookrightarrow Ps T Alg
\end{displaymath}
of the 2-category of strict $T$-algebras and strict $T$-morphisms into the 2-category of pseudo $T$-algebras and pseudo $T$-morphisms has a strict left 2-adjoint, usually written $(-)'$, and moreover for a pseudo algebra $A$, the unit $A \to A'$ is an [[equivalence]] in $Ps T Alg$. Thus $A$ is not only equivalent to a strict $T$-algebra, it is equivalent to a canonically defined one which is characterized by a universal property.

This ``coherence theorem'' is true in a lot of generality, although there are 2-monads for which it fails (see (\hyperlink{Shulman}{Shulman})). However, often it leaves a lot of work to be done in order to extract what is commonly thought of as a coherence theorem. This is because the notion of pseudo $T$-algebra is always an \emph{unbiased} weak structure, whereas it is more usual to study biased structures. Moreover, in most cases, proving an equivalence between biased and unbiased notions requires the full strength of the coherence theorem (in the description-of-free-algebras sense) for the biased notion!

\hypertarget{operads}{}\subsubsection*{{Operads}}\label{operads}

See [[operad]].

\hypertarget{clubs}{}\subsubsection*{{Clubs}}\label{clubs}

See [[club]].

\hypertarget{references}{}\subsection*{{References}}\label{references}

[[Saunders Mac Lane]] discusses some of the history of the coherence problem in section 5 of

\begin{itemize}%
\item [[Saunders Mac Lane]], Topology and Logic as a Source of Algebra (Retiring Presidential Address), \emph{Bulletin of the AMS} 82:1, January 1976. (\href{https://projecteuclid.org/euclid.bams/1183537593}{euclid})

\end{itemize}
An account of some of the history of (proofs of) coherence theorems is at

\begin{itemize}%
\item \href{linear+type+theory#HistoryCategoricalSemantics}{linear type theory -- History of categorical semantics} .

\end{itemize}
See also at \emph{[[Kelly-Mac Lane graph]]}, at \emph{[[proof net]]} and at \emph{[[Trimble rewiring]]} for more on the [[syntax|syntactic]] proofs of coherence.

For specific references see at the above sub-entries in the \hyperlink{ListOfTheorems}{List of coherence theorems}.

See also

\begin{itemize}%
\item [[Steve Lack]], Codescent objects and coherence, \href{http://www.ams.org/mathscinet-getitem?mr=1935980}{MR}


\item [[Mike Shulman]], ``Not every pseudoalgebra is equivalent to a strict one'', \emph{Adv. Math.} 229 no. 3 (2012), 2024--2041, \href{http://arxiv.org/abs/1005.1520}{arXiv}



\end{itemize}
[[!redirects coherence theorems]]



\end{document}