text:
\section*{Introduction}

The notion of tricategory, introduced by Gordon, Power, and
Street~\cite{Gordon-Power-Street} in 1995, seems still to represent the
highest-dimensional explicit weak categorical structure that can be manipulated
by hand (i.e.~without methods of homotopy theory), and is therefore an
important test bed for higher-categorical ideas.  In this work we investigate
the nature of weak units at this level.  While coherence for weak associativity
is rather well understood, thanks to the geometrical insight provided by the
Stasheff associahedra~\cite{Stasheff:1963}, coherence for unit structures is
more mysterious, and so far there seems to be no clear geometric pattern for the
coherence laws for units in higher dimensions.  Specific interest in weak units
stems from Simpson's conjecture~\cite{Simpson:9810}, according to which strict
$n$-groupoids with weak units should model all homotopy $n$-types.

In the present paper, working in the setting of a strict $2$-category $\mathscr{C}$ with a
strict tensor product, we define a notion of weak unit by simple axioms that
involve only the notion of equivalence, and hence in principle make sense in all
dimensions.  Briefly, a weak unit is a cancellable pseudo-idempotent.  We
work out the basic theory of such units, and compare with the notion extracted
from the definition of tricategory.  In the companion paper {\em Weak units and
homotopy $3$-types}~\cite{Joyal-Kock:traintracks} we employ this notion of unit
to prove a version of Simpson's conjecture for $1$-connected homotopy $3$-types,
which is the first nontrivial case.  The strictness assumptions of the present
paper should be justified by that result.

\bigskip

By cancellable pseudo-idempotent we mean a pair $(I,\alpha)$ where $I$ is an
object in $\mathscr{C}$ such that tensoring with $I$ from either side is an equivalence of
$2$-categories, and $\alpha: I \otimes I \isopil I$ is an equi-arrow (i.e.~an
arrow admitting a pseudo-inverse).  The remarkable fact about this definition is
that $\alpha$, viewed as a multiplication map, comes with canonical higher order
data built in: it possesses a canonical associator $\cel A$
which automatically satisfies the pentagon equation.
This is our Theorem~\ref{thmA}.  The point is that the arrow $\alpha$ alone,
thanks to the cancellability of $I$, induces all the usual structure of left and right
constraints with all the $2$-cell data that goes into them and the axioms they
must satisfy.

\bigskip

As a warm-up to the various constructions and ideas, we start out in
Section~\ref{sec:dim1} by briefly running through the corresponding theory for
cancellable-idempotent units in monoidal $1$-categories.  This theory has been
treated in detail in \cite{Kock:0507349}.

The rest of the paper is dedicated to the case of monoidal
$2$-categories.  In Section~\ref{sec:dim2-main} we give the definitions
and state the main results:
Theorem~\ref{thmA} says that there is a canonical associator $2$-cell for
$\alpha$, and that this $2$-cell automatically satisfies the
pentagon equation.
Theorem~\ref{thmB} states  that unit morphisms automatically
are compatible with the associators of Theorem~\ref{thmA}.
Theorem~\ref{thmC} states that the $2$-category of units is
contractible if non-empty.  Hence, `being unital' is, up to homotopy, a property
rather than a structure.

Next follow three sections dedicated to proofs of each of these three theorems.
In Section~\ref{sec:left-right} we show how the map $\alpha:II\isopil I$ alone
induces left and right constraints, which in turn are used to construct the
associator and establish the pentagon equation.  The left and right
constraints are not canonical, but surprisingly the associator does not depend
on the choice of them.  In Section~\ref{sec:catArr} we prove Theorem~\ref{thmB} by
interpreting it as a statement about units in the $2$-category of arrows, where
it is possible to derive it from Theorem~\ref{thmA}. In Section~\ref{sec:contractibility}
we prove Theorem~\ref{thmC}. The key ingredient is to use the left and right constraints
to link up all the units, and to show that the unit morphisms are precisely
those compatible with the left and right constraints; this makes them
`essentially unique' in the required sense.

In Section~\ref{sec:classical} we go through the basic theory of classical units
(i.e.~as extracted from the definition of
tricategory~\cite{Gordon-Power-Street}).  Finally, in
Section~\ref{sec:comparison} we show that the two notions of unit are
equivalent.  This is our Theorem~\ref{thmE}. A curiosity implied by the arguments in this
section is that the left and right axioms for the $2$-cell data in the
Gordon-Power-Street
definition (denoted TA2 and TA3 in \cite{Gordon-Power-Street}) imply each other.

(We have no Theorem D.)

\bigskip

This notion of weak units as cancellable idempotents is precisely what can be
extracted from the more abstract, Tamsamani-style, theory of fair
$n$-categories~\cite{Kock:0507116} by making an arbitrary choice of a fixed weak
unit.  In the theory of fair categories, the key object is a contractible space
of all weak units, rather than any particular point in that space, and handling
this space as a whole bypasses coherence issues.  However, for the sake of
understanding what the theory entails, and for the sake of concrete
computations, it is interesting to make a choice and study the ensuing coherence
issues, as we do in this paper.  The resulting approach is very much in the
spirit of the classical theory of monoidal categories, bicategories, and
tricategories, and provides some new insight to these theories.  To stress this
fact we have chosen to formulate everything from scratch in such classical
terms, without reference to the theory of fair categories.

In the case of monoidal $1$-categories, the cancellable-idempotent viewpoint on
units goes back to Saavedra~\cite{Saavedra}.  The importance of this viewpoint
in higher categories was first suggested by Simpson~\cite{Simpson:9810}, in
connection with his weak-unit conjecture.  He gave an ad hoc definition in this
style, as a mere indication of what needed to be done, and raised the question
of whether higher homotopical data would have to be specified.  The surprising
answer is, at least here in dimension $3$, that specifying $\alpha$ is enough,
then the higher homotopical data is automatically built in.

\bigskip

This paper was essentially written in 2004, in parallel with
\cite{Joyal-Kock:traintracks}.  We are ourselves to blame for the delay of
getting it out of the door.  The present form of the paper represents only half
of what was originally planned to go into the paper.  The second half should
contain an analysis of strong monoidal functors (along the lines of what was
meanwhile treated just in the $1$-dimensional case \cite{Kock:0507349}), and
also a construction of the `universal unit', hinted at in \cite{Kock:0507116}.
We regret that these ambitions should hold back the present material for so
long, and have finally decided to make this first part available {\em as is}, in
the belief that it is already of some interest and can well stand alone.

\begin{blanko*}{Acknowledgements.}
  We thank Georges Maltsiniotis for pointing out to us that the
  cancellable-idempotent notion of unit in dimension $1$ goes back to
  Saavedra~\cite{Saavedra}, and we thank Josep Elgueta for catching an error in
  an earlier version of our comparison with tricategories.  The first-named
  author was supported by the NSERC. The second-named author was very happy to
  be a CIRGET postdoc at the UQAM in 2004, and currently holds support from
  grants MTM2006-11391 and MTM2007-63277 of Spain.
\end{blanko*}

\section{Units in monoidal categories}
\label{sec:dim1}

It is helpful first briefly to recall the relevant results for
monoidal categories, referring the reader to \cite{Kock:0507349} for
further details of this case.

\begin{blanko}{Semi-monoidal categories.}
  A {\em semi-monoidal category} is a category $\mathscr{C}$ equipped with a tensor
  product (which we denote by plain juxtaposition), i.e.~an associative functor
  \begin{eqnarray*}
    \mathscr{C}\times\mathscr{C} & \longrightarrow & \mathscr{C}  \\
    (X,Y) & \longmapsto & XY .
  \end{eqnarray*}
  For simplicity we assume strict associativity,
  $X(YZ)=(XY)Z$.
\end{blanko}

\begin{blanko}{Monoidal categories.}
  (Mac Lane~\cite{MacLane:naturalAssociativity}.)  A semi-monoidal category $\mathscr{C}$ is a
  {\em monoidal category} when it is furthermore equipped with a distinguished
  object $I$ and natural isomorphisms
\begin{diagram}[w=4ex,tight]
I X & \rTo^{\lambda_X}  & X
  &  \lTo^{\rho_X}  &  X I
\end{diagram}
obeying the following rules (cf.~\cite{MacLane:naturalAssociativity}):
\begin{align}

  \lambda_I &= \rho_I \\

  \lambda_{XY} &= \lambda_X Y \\

 \rho_{XY} &= X\rho_Y \\

  X\lambda_Y &= \rho_X Y \label{Kelly}
\end{align}
\end{blanko}
Naturality of $\lambda$ and $\rho$ implies
\begin{equation}\label{naturality1}
  \lambda_{IX} = I\lambda_X ,  \qquad \rho_{XI} = \rho_X I   ,
\end{equation}
independently of Axioms (1)--(4).

\begin{BM}
  Tensoring with $I$ from either side is an equivalence of categories.
\end{BM}

\begin{lemma}
  {\rm (Kelly~\cite{Kelly:MacLanesCoherence}.)}  Axiom~(4) implies axioms
  (1), (2), and (3).
\end{lemma}
\begin{dem}
    (4) implies (2):
    Since tensoring with $I$ on the left is an equivalence, it is
    enough to prove $I \lambda_{XY} = I\lambda_X Y$.  But this
    follows from Axiom~(4) applied twice (swap $\lambda$ out
    for a $\rho$ and swap back again only on the nearest factor):
    $$
    I\lambda_{XY} = \rho_I XY = I \lambda_X Y .
    $$
    Similarly for $\rho$, establishing (3).

    (4) and (2) implies (1):
  Since tensoring with $I$ on the right is an equivalence, it is
  enough to prove $\lambda_I I = \rho_I I$.  But this follows from
  (2), (5), and (4):
  $$
  \lambda_I I = \lambda_{II} = I \lambda_I = \rho_I I .
  $$

  \vspace{-2em}
\end{dem}

The following alternative notion of unit object goes back to
Saavedra~\cite{Saavedra}.  A thorough treatment of the notion was given in
\cite{Kock:0507349}.

\begin{blanko}{Units as cancellable pseudo-idempotents.}\label{unit1}
  An object $I$ in a semi-monoidal category $\mathscr{C}$ is called {\em cancellable} if the two
  functors $\mathscr{C}\to\mathscr{C}$
  \begin{eqnarray*}
    X & \longmapsto & IX\\
    X & \longmapsto & XI
  \end{eqnarray*}
  are fully faithful.
  By definition, a {\em pseudo-idempotent} is
  an object $I$ equipped with an isomorphism $\alpha : II \isopil I$.
  Finally we define a {\em unit object} in $\mathscr{C}$ to be a cancellable pseudo-idempotent.
\end{blanko}

\begin{lemma}\label{Kelly-lemma}
  {\rm \cite{Kock:0507349}}
  Given a unit object $(I,\alpha)$ in a semi-monoidal category $\mathscr{C}$, for each
  object $X$ there are unique arrows
  \begin{diagram}[w=4ex,tight]
    I X & \rTo^{\lambda_X}  & X
    &  \lTo^{\rho_X}  &  X I
  \end{diagram}
  such that
  \begin{eqnarray*}

    (\cel{L}) &  & I\lambda_X = \alpha X  \\

    (\cel{R}) &  & \rho_X I = X \alpha .
  \end{eqnarray*}
  The $\lambda_X$ and $\rho_X$ are isomorphisms and natural in $X$.
\end{lemma}

\begin{dem}
  Let $\mathbb{L}: \mathscr{C}\to \mathscr{C}$ denote the functor defined by tensoring with $I$
  on the left.  Since $\mathbb{L}$ is fully faithful, we have a bijection
  $$
  \operatorname{Hom}(IX,X) \to \operatorname{Hom}(IIX,IX).
  $$
  Now take $\lambda_X$ to be the inverse image of $\alpha X$; it is an
  isomorphism since $\alpha X$ is.  Naturality follows by considering more
  generally the bijection
  $$
  \operatorname{Nat}(\mathbb{L},\operatorname{id}_\mathscr{C}) \to \operatorname{Nat}(\mathbb{L}\circ \mathbb{L}, \mathbb{L})
  ;
  $$
  let $\lambda$ be the inverse image of the natural
  transformation whose components are $\alpha X$.
  Similarly on the right.
\end{dem}

\begin{lemma}\label{Kelly-dim1}
  {\rm \cite{Kock:0507349}}
  For $\lambda$ and $\rho$ as above, the Kelly axiom~\eqref{Kelly} holds:
  $$
  X \lambda_Y = \rho_X Y .
  $$
  Therefore, by Lemma~\ref{Kelly-lemma} a semi-monoidal category with
  a unit object is a monoidal category in the classical sense.
\end{lemma}

\begin{dem}
  In the commutative square
  \begin{diagram}[w=6ex,h=4.5ex,tight]
    XIIY & \rTo^{XI\lambda_Y}  & XIY  \\
    \dTo<{\rho_X I Y}  &    & \dTo>{\rho_X Y}  \\
    XIY  & \rTo_{X\lambda_Y}  & XY
  \end{diagram}
  the top arrow is equal to $X  \alpha  Y$, by $X$ tensor
  (\cel{L}),
  and the left-hand arrow is also equal to $X  \alpha  Y$, by (\cel{R}) tensor $Y$.
  Since $X\alpha Y$ is an isomorphism, it follows that $X \lambda_Y = \rho_X Y$.
\end{dem}

\begin{lemma}\label{ass+eq}
  For a unit object $(I,\alpha)$ we have:
  (i) The map $\alpha:II\to I$ is associative.
  (ii) The two functors $X\mapsto IX$ and $X\mapsto XI$ are equivalences.
\end{lemma}

\begin{dem}
  Since $\alpha$ is invertible, associativity amounts to the equation $I \alpha
  = \alpha I$, which follows from the previous proof by setting $X=Y=I$ and
  applying $\cel L$ and $\cel R$ once again.  To see that $\mathbb{L}$ is an
  equivalence, just note that it is isomorphic to the identity via $\lambda$.
\end{dem}

\begin{blanko}{Uniqueness of units.}
  Just as in a semi-monoid a unit element is unique if it exists, one can
  show~\cite{Kock:0507349} that in a semi-monoidal category, any two units are
  uniquely isomorphic.  This statement does not involve $\lambda$ and $\rho$,
  but the proof does: the canonical isomorphism $I \isopil J$ is the composite
  $I \stackrel{\rho_I^{\scriptscriptstyle -1}}{\rTo} IJ \stackrel{\lambda_J}{\rTo} J$.
\end{blanko}

\section{Units in monoidal $2$-categories: definition and main results}
\label{sec:dim2-main}

In this section we set up the necessary terminology and notation, give the main
definition, and state the main results.

\begin{blanko}{$2$-categories.}
  We work in a strict $2$-category $\mathscr{C}$.  We use the symbol $\#$ to denote
  composition of arrows and horizontal composition of $2$-cells in $\mathscr{C}$, always
  written from the left to the right, and occasionally decorating the symbol $\#$ by
  the name of the object where the two arrows or $2$-cells are composed.  By an
  {\em equi-arrow} in $\mathscr{C}$ we understand an arrow $f$ admitting an
  (unspecified) pseudo-inverse, i.e.~an arrow $g$ in the opposite direction such
  that $f \# g$ and $g \# f$ are isomorphic to the respective identity arrows,
  and such that the comparison $2$-cells satisfy the usual triangle equations
  for adjunctions.

  We shall make extensive use of arguments with pasting diagrams
  \cite{Kelly-Street:2cat}.
  Our drawings of $2$-cells should be read from bottom to top, so that for
  example
  \begin{diagram}[w=3ex,h=3.5ex,tight]
  X    && \rTo^h    && Z    \\
  &\rdTo_f    & \raisebox{4pt}{\cel U}     & \ruTo_g  &  \\
  &    & Y    & &
  \end{diagram}
  denotes $\cel U : f \,\underset Y \#\, g \Rightarrow h$.  The symbol $\copyright$
  will denote identity $2$-cells.

  The few $2$-functors we need all happen to be strict.
  By {\em natural transformation} we always mean pseudo-natural transformation.
  Hence a natural transformation $u: F \Rightarrow G$ between two $2$-functors
  from $\mathscr{D}$ to $\mathscr{C}$ is given by an arrow $u_X: FX\to GX$ for each object
  $X\in \mathscr{D}$, and an invertible $2$-cell
  \begin{diagram}[w=6ex,h=4.5ex,tight]
  FX & \rTo^{u_X}  & GX  \\
  \dTo<{F(x)}  &  u_x  & \dTo>{G(x)}  \\
  FX'  & \rTo_{u_{X'}}  & GX'
  \end{diagram}
  for each arrow $x: X\to X'$ in $\mathscr{D}$, subject to the usual compatibility
  conditions~\cite{Kelly-Street:2cat}.  The modifications we shall need will
  happen to be invertible.
\end{blanko}

\begin{blanko}{Semi-monoidal $2$-categories.}\label{semimonoidal}
  By {\em semi-monoidal $2$-category} we mean a $2$-category $\mathscr{C}$ equipped with
  a tensor product, i.e.~an associative $2$-functor
\begin{eqnarray*}
  \otimes : \mathscr{C}\times\mathscr{C} & \longrightarrow & \mathscr{C}  \\
  (X,Y) & \longmapsto & XY ,
\end{eqnarray*}
denoted by plain juxtaposition.  We already assumed $\mathscr{C}$ to be a strict
$2$-category, and we also require $\otimes$ to be a strict $2$-functor and to
be strictly associative: $(XY)Z=X(YZ)$.  This is mainly for convenience, to
keep the focus on unit issues.

Note that the tensor product of two equi-arrows is again an equi-arrow, since
its pseudo-inverse can be taken to be the tensor product of the pseudo-inverses.
\end{blanko}

\begin{blanko}{Semi-monoids.}
  A {\em semi-monoid} in $\mathscr{C}$ is a triple
  $(X,\alpha,\text{\rm \textsf{\AA}})$ consisting of an
  object $X$, a multiplication map $\alpha: X X \to X$,
  and an invertible $2$-cell $\text{\rm \textsf{\AA}}$ called the {\em associator},
  $$
  \begin{diagram}[w=6ex,h=4.5ex,tight]
  XXX & \rTo^{\alpha X}  & X X  \\
  \dTo<{X\alpha} &  {\scriptstyle \text{\rm \textsf{\AA}}}  & \dTo>\alpha \\
  X X  & \rTo_{\alpha} & X
  \end{diagram}
$$
  required to satisfy the `pentagon equation':
$$
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  XXXX&\rTo^{\alpha XX}&XXX&&&&\\
  \dTo<{XX\alpha}&\rdTo>{X\alpha X}&\psr{\text{\rm \textsf{\AA}} X}&\rdTo>{\alpha X}&&&\\
  XXX&\psr{X\text{\rm \textsf{\AA}}}&XXX&\rTo^{\alpha X}&XX\\
  &\rdTo_{X\alpha}&\dTo<{X\alpha}&\text{\rm \textsf{\AA}}&\dTo>{\alpha}\\
  &&XX&\rTo_{\alpha}&X
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  XXXX&\rTo^{\alpha XX}&XXX&&&&\\
  \dTo<{XX\alpha}&\copyright&\dTo>{X\alpha}&\rdTo>{\alpha X}&&&\\
  XXX&\rTo_{\alpha X}&XX&\psr{\text{\rm \textsf{\AA}}}&XX\\
  &\rdTo_{X\alpha}&\psr{\text{\rm \textsf{\AA}}}&\rdTo<{\alpha}&\dTo>{\alpha}\\
  &&XX&\rTo_{\alpha}&X
\end{diagram}
$$
In the applications, $\alpha$ will be an equi-arrow, and hence we will have
$$
\text{\rm \textsf{\AA}} = \cel A  \underset{XX}{\#}  \alpha
$$
for a some unique invertible
$$
\cel A: X\alpha \Rightarrow \alpha X,
$$
which it will more convenient to work with.
In this case, the pentagon equation is equivalent to the more compact equation
\begin{equation}\label{shortApentagon}
\begin{diagram}[w=6ex,h=6ex,tight]
  XXXX&\rTo^{\alpha XX}&XXX\\
  \leftglob{XX\alpha}\lift{0}{X\cel{A}}\rightglob{X\alpha X}&\shuft{20}{\text{\rm \textsf{\AA}} X}&\rightglob{\alpha X}\\
  XXX&\rTo_{\alpha X}&XX
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XXXX&\rTo^{\alpha XX}&XXX\\
  \leftglob{XX\alpha}&\shuft{-20}{\copyright}&\leftglob{X\alpha}\lift{0}{\cel{A}}\rightglob{\alpha X}\\
  XXX&\rTo_{\alpha X}&XX
\end{diagram}
\end{equation}
which we shall also make use of.
\end{blanko}

\begin{blanko}{Semi-monoid maps.}\label{semimonoid-map}
  A {\em semi-monoid map} $f: (X,\alpha,\text{\rm \textsf{\AA}}) \to (Y,\beta,\cel{B})$ is
  the data of an arrow $f:X\to Y$ in $\mathscr{C}$ together with an invertible
  $2$-cell
  \begin{diagram}[w=6ex,h=4.5ex,tight]
  X  X & \rTo^{f f}  & Y Y  \\
  \dTo<\alpha  &  \cel{F}  & \dTo>\beta  \\
  X  & \rTo_f  & Y
  \end{diagram}
  such that this cube commutes:
$$
\def\sdf#1{\rotstart{-36.87 rotate}\hbox to0pt {\vsize 0pt \hss\(\scriptstyle #1\)\hss}\rotfinish}
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  &&YYY&\rTo^{\beta Y}& YY \\
  & \ruTo^{fff} &\sdf{\cel{F}f}& \ruTo^{ff} & \dTo>\beta \\
  XXX&\rTo^{\alpha X}&XX&\sdf{\cel F}&Y\\
  \dTo<{X\alpha}&\text{\rm \textsf{\AA}}&\dTo>{\alpha}&\ruTo_f&\\
  XX&\rTo_{\alpha}&X&&
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  &&YYY&\rTo^{\beta Y}&YY\\
  & \ruTo^{fff}&\dTo<{Y \beta}&\cel{B}&\dTo>{\beta}\\
  XXX&\sdf{f\cel F}&YY&\rTo_{\beta}&Y \\
  \dTo<{X\alpha}&\ruTo_{ff}&\sdf{\cel F}&\ruTo_f&\\
  XX&\rTo_{\alpha}&X&&
\end{diagram}
$$

When $\beta$ is an equi-arrow, the cube equation is equivalent to the simpler
equation:
\begin{equation}\label{shortSemimonoidMap}
\begin{diagram}[w=6ex,h=6ex,tight]
  XXX&\rTo^{fff}&YYY\\
  \leftglob{X\alpha}\lift{0}{\cel{A}}\rightglob{\alpha X}&\shuft{20}{\cel{F}f}&\rightglob{\beta Y}\\
  XX&\rTo_{ff}&YY
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XXX&\rTo^{fff}&YYY\\
  \leftglob{X\alpha}&\shuft{-20}{f\cel{F}}&\leftglob{Y\beta}\lift{0}{\cel{B}}\rightglob{\beta Y}\\
  XX&\rTo_{ff}&YY
\end{diagram}
\end{equation}
which will be useful.
\end{blanko}

\begin{blanko}{Semi-monoid transformations.}\label{semimonoid-transf}
  A {\em semi-monoid transformation} between two parallel semi-monoid maps $(f,\cel{F})$ and
  $(g,\cel{G})$
  is a $2$-cell $\cel{T}: f \Rightarrow g$ in $\mathscr{C}$ such that this cylinder
  commutes:
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  XX&\topglob{gg}\lift{0}{\cel{TT}}\dropglob{ff}&YY\\
  \dTo<{\alpha}&\lift{-12}{\cel{F}}&\dTo>{\beta}\\
  X&\dropglob{f}&Y
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XX&\topglob{gg}&YY\\
  \dTo<{\alpha}&\lift{12}{\cel{G}}&\dTo>{\beta}\\
  X&\topglob{g}\lift{0}{\cel{T}}\dropglob{f}&Y
\end{diagram}
\vspace{24pt}
$$
\end{blanko}

\begin{lemma}\label{inv}
  Let $f:X \to Y$ be a semi-monoid map.  If $f$ is an equi-arrow (as an arrow in
  $\mathscr{C}$) with quasi-inverse $g:Y\to X$, then there is a canonical $2$-cell
  $\cel{G}$ such that $(g,\cel{G})$ is a semi-monoid map.
\end{lemma}
\begin{dem}
  The $2$-cell $\cel G$ is defined as the mate~\cite{Kelly-Street:2cat} of
  the $2$-cell $\cel F^{\scriptscriptstyle -1}$.  It is routine to check the cube equation in
  \ref{semimonoid-map}.
\end{dem}

\begin{blanko}{Pseudo-idempotents.}\label{idempotent}
  A {\em pseudo-idempotent} is a pair $(I,\alpha)$ where $\alpha:II\to I$ is an
  equi-arrow.  A {\em morphism of pseudo-idempotents} from $(I,\alpha)$ to
  $(J,\beta)$ is a pair $(u,\cel{U})$ consisting of an arrow $u:I\to J$ in $\mathscr{C}$
  and an invertible $2$-cell
  \begin{diagram}
  II & \rTo^{uu}  & JJ  \\
  \dTo<\alpha  &  \cel{U}  & \dTo>\beta  \\
  I  & \rTo_u  & J .
  \end{diagram}
  If $(u,\cel{U})$ and $(v,\cel{V})$ are morphisms of pseudo-idempotents from
  $(I,\alpha)$ to $(J,\beta)$, a {\em $2$-morphism of pseudo-idempotents} from
  $(u,\cel{U})$ to $(v,\cel{V})$ is a $2$-cell $\cel T: u \Rightarrow v$
  satisfying the cylinder equation of \ref{semimonoid-transf}.
\end{blanko}

\begin{blanko}{Cancellable objects.}\label{cancellable}
  An object $I$ in $\mathscr{C}$ is called {\em cancellable} if the two
  $2$-functors $\mathscr{C}\to\mathscr{C}$
  \begin{eqnarray*}
    X & \longmapsto & IX\\
    X & \longmapsto & XI
  \end{eqnarray*}
  are fully faithful.  (Fully faithful means that the induced functors on hom
  categories are equivalences.)  A {\em cancellable morphism} between
  cancellable objects $I$ and $J$ is an equi-arrow $u:I \to J$.  (Equivalently
  it is an arrow such that the functors on hom cats defined by tensoring with
  $u$ on either side are equivalences, cf.~\ref{unitmap}.)  A {\em cancellable
  $2$-morphism} between cancellable arrows is any invertible $2$-cell.
\end{blanko}

We are now ready for the main definition and the main results.

\begin{blanko}{Units.}\label{main-def}
  A {\em unit object} is by definition a cancellable pseudo-idempotent.
  Hence it is a pair $(I,\alpha)$ consisting
  of an object $I$ and an equi-arrow $\alpha : II \to I$, with the
  property that tensoring with $I$ from either side define fully
  faithful $2$-functors $\mathscr{C}\to\mathscr{C}$.

  A {\em morphism} of units is a
  cancellable morphism of
  pseudo-idempotents. In other words, a unit morphism from $(I,\alpha)$ to
  $(J,\beta)$ is a pair $(u,\cel{U})$ where $u: I \to J$ is an equi-arrow
  and $\cel U$ is an invertible $2$-cell
  \begin{diagram}
  II & \rTo^{uu}  & JJ  \\
  \dTo<\alpha  &  \cel{U}  & \dTo>\beta  \\
  I  & \rTo_u  & J .
  \end{diagram}

  A {\em $2$-morphism} of units is a cancellable $2$-morphism of
  pseudo-idempotents.  Hence a $2$-morphism from
  $(u,\cel{U})$ to $(v,\cel{V})$ is a $2$-cell $\cel T: u \Rightarrow v$
  such that
\vspace*{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  II&\topglob{vv}\lift{0}{\cel{TT}}\dropglob{uu}&JJ\\
  \dTo<{\alpha}&\lift{-12}{\cel{U}}&\dTo>{\beta}\\
  I&\dropglob{u}&J
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  II&\topglob{vv}&JJ\\
  \dTo<{\alpha}&\lift{12}{\cel{V}}&\dTo>{\beta}\\
  I&\topglob{v}\lift{0}{\cel{T}}\dropglob{u}&J
\end{diagram}
\vspace{24pt}
$$

  This defines the {\em $2$-category of units}.
\end{blanko}
In the next section we'll see how the notion of unit object induces left and
right constraints familiar from standard notions of monoidal $2$-category.  It
will then turn out (Lemmas~\ref{unitmap} and \ref{unit2map}) that unit morphisms
and $2$-morphisms can be characterised as those morphisms and $2$-morphisms
compatible with the left and right constraints.

\begin{blanko*}{Theorem~\ref{thmA} (Associativity).}
  {\em
  Given a unit object $(I,\alpha)$, there is a canonical invertible
  $2$-cell
  \begin{diagram}[w=6ex,h=4.5ex,tight]
  III & \rTo^{\alpha I}  & II  \\
  \dTo<{I\alpha}  &  \text{\rm \textsf{\AA}}  & \dTo>\alpha  \\
  II  & \rTo_\alpha  & I
  \end{diagram}
  which satisfies the pentagon equation}
\begin{equation}\label{pentaA}
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIII&\rTo^{\alpha II}&III&&&&\\
  \dTo<{II\alpha}&\rdTo>{I\alpha I}&\psr{\text{\rm \textsf{\AA}} I}&\rdTo>{\alpha I}&&&\\
  III&\psr{I\text{\rm \textsf{\AA}}}&III&\rTo^{\alpha I}&II\\
  &\rdTo_{I\alpha}&\dTo<{I\alpha}&\text{\rm \textsf{\AA}}&\dTo>{\alpha}\\
  &&II&\rTo_{\alpha}&I
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIII&\rTo^{\alpha II}&III&&&&\\
  \dTo<{II\alpha}&\copyright&\dTo>{I\alpha}&\rdTo>{\alpha I}&&&\\
  III&\rTo_{\alpha I}&II&\psr{\text{\rm \textsf{\AA}}}&II\\
  &\rdTo_{I\alpha}&\psr{\text{\rm \textsf{\AA}}}&\rdTo<{\alpha}&\dTo>{\alpha}\\
  &&II&\rTo_{\alpha}&I
\end{diagram}
\end{equation}
\end{blanko*}
In other words, a unit object is automatically a semi-monoid.
The $2$-cell $\cel A$ is characterised uniquely in \ref{uniqueA}.

\begin{blanko*}{Theorem~\ref{thmB}.}
  {\em
  A unit morphism $(u,\cel{U}): (I,\alpha) \to (J,\beta)$
  is automatically a semi-monoid map, when $I$ and $J$ are considered
  semi-monoids in virtue of Theorem~A.}
\end{blanko*}

\begin{blanko*}{Theorem~\ref{thmC} (Contractibility).}
  {\em
  The $2$-category of units in $\mathscr{C}$ is contractible, if non-empty.
  }
\end{blanko*}
In other words, between any two units there exists a unit morphism, and
between any two parallel unit morphisms there is a unique unit
$2$-morphism.
Theorem~C shows that units objects are unique up to homotopy, so in
this sense `being unital' is a
property not a structure.

\bigskip

The proofs of these three theorems rely on the auxiliary structure of left and
right constraints which we develop in the next section, and which also displays
the relation with the classical notion of monoidal $2$-category: in
Section~\ref{sec:comparison} we show that the cancellable-idempotent notion of
unit is equivalent to the notion extracted from the definition of tricategory of
Gordon, Power, and Street~\cite{Gordon-Power-Street}.  This is our
Theorem~\ref{thmE}.

\section{Left and right actions, and associativity of the unit
(Theorem~\ref{thmA})}
\label{sec:left-right}

Throughout this section we fix a unit object $(I,\alpha)$.
\begin{lemma}\label{LR}
  For each object $X$ there exists pairs $(\lambda_X, \cel L_X)$ and
  $(\rho_X,  \cel R_X)$,
  \begin{eqnarray*}
    \lambda_X : IX \to X, &  &
    \cel L_X : I\lambda_X \Rightarrow \alpha X  \\
    \rho_X : XI \to X,  &  &
    \cel R_X : X \alpha  \Rightarrow \rho_X I
  \end{eqnarray*}
  where $\lambda_X$ and $\rho_X$ are equi-arrows, and $\cel L_X$ are
  $\cel R_X$ are invertible
  $2$-cells.

  For every such family, there is a unique way to assemble
  the $\lambda_X$ into a natural transformation
  (this involves
  defining $2$-cells $\lambda_f$ for every arrow $f$ in $\mathscr{C}$) in such
  a way that $\cel L$ is a natural modification.  Similarly for the
  $\rho_X$ and $\cel R_X$.
\end{lemma}

The $\lambda_X$ is an action of $I$ on each $X$, and the $2$-cell
$\cel L_X$ expresses an associativity constraint on this action.
Using these structures we will construct the associator for $\alpha$,
and show it satisfies the pentagon equation.
Once that is in place we will see
that the actions $\lambda$ and $\rho$ are coherent too (satisfying
the appropriate pentagon equations).

\bigskip

We shall treat the left action.  The right action is of course
equivalent to establish.

\begin{blanko}{Construction of the left action.}
  Since tensoring with $I$ is a fully faithful $2$-functor, the functor
  $$
  \operatorname{Hom}(IX,X) \to \operatorname{Hom}(IIX,IX)
  $$
  is an equivalence of categories.  In the second category there is
  the canonical object $\alpha  X$.  Hence there is a pseudo
  pre-image which we denote $\lambda_X : I  X \to X$, together
  with an invertible $2$-cell
  $\cel{L}_X : I  \lambda_X \Rightarrow \alpha  X$:
  \vspace{15pt}
  \begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{\alpha X}\lift{-2}{\cel L_X}\dropglob{I\lambda_X}&IX
\end{diagram}
\vspace{15pt}

\noindent
  Since $\alpha$ is an equi-arrow, also $\alpha  X$ is equi,
  and since $\cel{L}_X$ is invertible, we conclude that also $I
  \lambda_X$ is an equi-arrow.  Finally since the $2$-functor `tensoring with
  $I$' is fully faithful, it reflects equi-arrows, so already $\lambda_X$
  is an equi-arrow.
\end{blanko}

\begin{blanko}{Naturality.}\label{naturality2}
  A slight variation in the formulation of the construction gives
  directly a natural
  transformation $\lambda$ and a modification $\cel L$:
  Let $\mathbb{L}:
  \mathscr{C}\to\mathscr{C}$ denote the $2$-functor `tensoring with $I$ on the left'.
  Since $\mathbb{L}$ is fully faithful, there is an equivalence
  of categories
  $$
  \operatorname{Nat}(\mathbb{L},\operatorname{Id}_\mathscr{C}) \to \operatorname{Nat}(\mathbb{L}\circ \mathbb{L}, \mathbb{L}) .
  $$
  Now in the second category we have the canonical natural
  transformation whose $X$-component is $\alpha X$ (and with trivial
  components on arrows).  Hence there is a
  pseudo pre-image natural transformation $\lambda : \mathbb{L} \to
  \operatorname{id}_\mathscr{C}$, together with a modification $\cel L$ whose $X$-component is
  $\cel{L}_X : I \lambda_X \Rightarrow \alpha X$.

  However, we wish to stress the fact that the construction is
  completely
  object-wise.  This fact is of course due to the presence of the
  isomorphism $\cel L_X$: something isomorphic to a natural
  transformation is again natural.  More precisely, to provide the
  $2$-cell data $\lambda_f$ needed to make $\lambda$ into a natural
  transformation, just pull back the $2$-cell data from the natural
  transformation $\alpha X$.
  In detail, we need invertible $2$-cells
    \begin{diagram}[w=6ex,h=4.5ex,tight]
    I  X  & \rTo^{\lambda_X}  & X  \\
    \dTo<{I f}  &  \lambda_f  & \dTo>f  \\
    I  Y   & \rTo_{\lambda_Y}  & Y
    \end{diagram}
To say that the $\cel L_X$ constitute a modification (from $\lambda$
to the identity) is to have this compatibility for every arrow $f:X\to Y$:
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{\alpha X}\lift{0}{\cel{L}_X}\dropglob{I\lambda_X}&IX\\
  \dTo<{IIf}&\lift{-12}{I\lambda_f}&\dTo>{If}\\
  IIY&\dropglob{I\lambda_Y}&IY
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{\alpha X}&IX\\
  \dTo<{IIf}&\lift{12}{\copyright}&\dTo>{If}\\
  IIY&\topglob{\alpha Y}\lift{0}{\cel{L}_Y}\dropglob{I\lambda_Y}&IY
\end{diagram}
\vspace{24pt}
$$
(Here the commutative cell is actually the $2$-cell part of the natural
transformation $\alpha X$.)
Now the point is that each $2$-cell $\lambda_f$ is uniquely defined by
this compatibility: indeed, since the other three $2$-cells in the
diagram are invertible, there is a unique $2$-cell that can fill the
place of $I\lambda_f$, and since $I$ is cancellable this $2$-cell
comes from a unique $2$-cell $\lambda_f$.
The required compatibilities of $\lambda_f$ with composition, identities,
and $2$-cells now follows from its construction: $\lambda_f$ is
just the translation via $\cel L$ of the identity $2$-cell $\alpha X$.
\end{blanko}

\begin{blanko}{Uniqueness of the left constraints.}\label{lambda-lambda}
  There may be many choices for $\lambda_X$, and even for a fixed
  $\lambda_X$, there may be many choices for
  $\cel{L}_X$.  However, between any two pairs $(\lambda_X,\cel{L}_X)$ and
  $(\lambda'_X,\cel{L}'_X)$ there is a unique invertible $2$-cell $\cel{U}^{\text{\tiny \rm{left}}}_X:
  \lambda_X \Rightarrow \lambda'_X$ such that this compatibility
  holds:
$$
  \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  I\lambda_X \ar@{=>}[rr]^{I \cel{U}^{\text{\tiny \rm{left}}}_X} \ar@{=>}[dr]_{\cel L_X} && I \lambda'_X \ar@{=>}[dl]^{\cel L'_X} \\
  & \alpha X &
  }
$$
  Indeed, this diagram defines uniquely an invertible $2$-cell $I\lambda_X
  \Rightarrow I \lambda_X'$, and since $I$ is cancellable, this
  $2$-cell comes from a unique $2$-cell $\lambda_X \Rightarrow
  \lambda_X'$ which we then call $\cel{U}^{\text{\tiny \rm{left}}}_X$.

  There is of course a completely analogous statement for right constraints.
\end{blanko}

\begin{blanko}{Construction of the associator.}
  We define $\cel A : I \alpha \Rightarrow \alpha I$
  as the unique $2$-cell satisfying the equation
  \vspace{24pt}
  \begin{equation}\label{A}
  \begin{diagram}[w=56pt,h=42pt,tight]
  IIII & \thintopglob{I\alpha I}\lift{0}{\cel R_I^{\scriptscriptstyle -1} I}\thindropglob{\rho II}  & III  \\
  \thinleftglob{I\alpha I}\lift{0}{I\cel L_I^{\scriptscriptstyle -1}}\thinrightglob{II\lambda}  &
  \copyright
  & \thinleftglob{I\lambda}\lift{0}{\cel{L}_I}\thinrightglob{\alpha I}  \\
  III  & \thintopglob{\rho I}\lift{0}{\cel{R}_I}\thindropglob{I\alpha}  & II
  \end{diagram}
  \qquad\qquad = \qquad
  \begin{diagram}[w=30pt,h=22.5pt,tight,hug]
  IIII &&&&  \\
  &\rdTo^{I\alpha I} &&&& \\
  && III && \\
  &&&\diagonaltopglob{\alpha I}
  \diagonaldropglob{I\alpha}\NWSElabel{\cel A}   & \\
  &&&& II
  \end{diagram}
  \vspace{24pt}
\end{equation}
This definition is meaningful: since $I\alpha I$ is an equi-arrow,
pre-composing with $I\alpha I$ is a $2$-equivalence, hence gives a bijection on
the level of $2$-cells, so $\cel A$ is
determined by the left-hand side of the equation.
Note that $\cel A$ is invertible since all the $2$-cells in the
  construction are.

  The associator  $\text{\rm \textsf{\AA}}$ is defined as $\cel A \text{-followed-by-}\alpha$:
  $$
  \text{\rm \textsf{\AA}} \ \: {\raisebox{0.255ex}{\normalfont\scriptsize :\!\!}}= \ \cel A \ \underset{II}{\#} \ \alpha    ,
  $$
  but it will be more convenient to work with $\cel A$.
\end{blanko}

\begin{prop}\label{independence}
  The definition of $\cel{A}$ does not depend on the choices of left constraint
  $(\lambda,\cel{L})$ and right constraint $(\rho,\cel{R})$.
\end{prop}

\begin{dem}
  Write down the left-hand side of \eqref{A} in terms of different left and
  right constraints.  Express these cells in terms of the original $\cel L_I$
  and $\cel R_I$, using the comparison $2$-cells $\cel{U}^{\text{\tiny \rm{left}}}_I$ and
  $\cel{U}^{\text{\tiny \rm{right}}}_I$ of \ref{lambda-lambda}.  Finally observe that these
  comparison cells can be moved across the commutative square to cancel each
  other pairwise.
\end{dem}

\begin{blanko}{Uniqueness of $\cel A$.}\label{uniqueA}
  Equation~\eqref{A} may not appear familiar, but it
  is equivalent to the following
  `pentagon' equation (after post-whiskering with $\alpha$):
\begin{equation}\label{penta-LRK}
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIII&\rTo^{\rho II}&III&&&&\\
  \dTo<{II\lambda}&\rdTo>{I\alpha I}&\psr{(\cel R I)\# (\alpha I)}&\rdTo>{\alpha I}&&&\\
  III&\psr{(I\cel L)\#(I\alpha)}&III&\rTo^{\alpha I}&II\\
  &\rdTo_{I\alpha}&\dTo<{I\alpha}&\cel A\#\alpha&\dTo>{\alpha}\\
  &&II&\rTo_{\alpha}&I
\end{diagram}
\quad = \quad
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIII&\rTo^{\rho II}&III&&&&\\
  \dTo<{II\lambda}&\copyright&\dTo>{I\lambda}&\rdTo>{\alpha I}&&&\\
  III&\rTo_{\rho I}&II&\psr{\cel L\#\alpha}&II\\
  &\rdTo_{I\alpha}&\psr{\cel R \#\alpha}&\rdTo<{\alpha}&\dTo>{\alpha}\\
  &&II&\rTo_{\alpha}&I
\end{diagram}
\end{equation}
From this pentagon equation we shall derive the pentagon equation for $\cel A$,
asserted in Theorem~\ref{thmA}.  To this end we need comparison between $\alpha$,
$\lambda_I$, and $\rho_I$, which we now establish, in analogy with Axiom~(1)
of monoidal category: the left and right constraints
coincide on the unit object, up to a canonical $2$-cell:
\end{blanko}

\begin{lemma}\label{lambda-rho}
  There are unique invertible $2$-cells
  $$
  \rho_I \stackrel{\cel{E}}{\Rightarrow}
  \alpha \stackrel{\cel{D}}{\Rightarrow} \lambda_I ,
  $$
  such that
  \vspace{30pt}
\begin{equation}
  \label{SAT}
\begin{diagram}[w=7ex,h=6ex,tight]
  III&
  \bigtopglob{\alpha I}\lift{12}{\cel{L}}\lift{-12}{I\cel{D}}\straighthor{I\lambda}\bigdropglob{I\alpha}
  &II
\end{diagram}
\quad = \quad
\begin{diagram}[w=6ex,h=6ex,tight]
  III&
  \topglob{\alpha I}\lift{0}{\cel A}\dropglob{I\alpha}
  &II
\end{diagram}
\quad = \quad
\begin{diagram}[w=7ex,h=6ex,tight]
  III&
  \bigtopglob{\alpha I}\lift{12}{\cel E I}\lift{-12}{\cel R}\straighthor{\rho I}\bigdropglob{I\alpha}
  &II
\end{diagram}
\vspace{30pt}
\end{equation}
\end{lemma}
\begin{dem}
  The left-hand equation defines uniquely a $2$-cell $I \alpha \Rightarrow
  I\lambda_I$, and since $I$ is cancellable, this cell comes from a unique
  $2$-cell $\alpha \Rightarrow \lambda_I$ which we then call $\cel{D}$.  Same
  argument for $\cel{E}$.
\end{dem}

\begin{satz}[Associativity]\label{thmA}
  Given a unit object $(I,\alpha)$, there is a canonical invertible
  $2$-cell
  \begin{diagram}
  III & \rTo^{\alpha I}  & II  \\
  \dTo<{I\alpha}  &  \text{\rm \textsf{\AA}}  & \dTo>\alpha  \\
  II  & \rTo_\alpha  & I
  \end{diagram}
  which satisfies the pentagon Equation~\eqref{pentaA}.
\end{satz}

\begin{dem}
  On each side of the cube equation \eqref{penta-LRK}, paste the cell $\cel{E}
  II$ on the top, and the cell $II\cel{D}$ on the left.  On the left-hand side
  of the equation we can use Equations~\eqref{SAT} directly, while on the
  right-hand side we first need to move those cells across the commutative
  square before applying \eqref{SAT}.  The result is precisely the pentagon cube
  for $\text{\rm \textsf{\AA}} = \cel A \# \alpha$.
\end{dem}

\begin{blanko}{Coherence of the actions.}
  We have now established that $(I,\alpha,\text{\rm \textsf{\AA}})$ is a semi-monoid, and
  may observe that the left and right constraints are coherent actions,
  i.e.~that their `associators' $\cel L$ and $\cel R$ satisfy the appropriate
  pentagon equations.  For the left action this equation is:
$$
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIIX&\rTo^{\alpha IX}&IIX&&&&\\
  \dTo<{II\lambda}&\rdTo>{I\alpha X}&\psr{\text{\rm \textsf{\AA}} X}&\rdTo>{\alpha X}&&&\\
  IIX&\psr{(I\cel L) \# (I\lambda)}&IIX&\rTo^{\alpha X}&IX\\
  &\rdTo_{I\lambda}&\dTo<{I \lambda}&\cel L \#\lambda&\dTo>{\lambda}\\
  &&IX&\rTo_{\lambda}&X
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=40pt,h=30pt,tight,scriptlabels,objectstyle=\scriptstyle,hug]
  IIIX&\rTo^{\alpha IX}&IIX&&&&\\
  \dTo<{II\lambda}&\copyright&\dTo>{I\lambda}&\rdTo>{\alpha X}&&&\\
  IIX&\rTo_{\alpha X}&IX&\psr{\cel L \#\lambda}&IX\\
  &\rdTo_{I\lambda}&\psr{\cel L \#\lambda}&\rdTo<{\lambda}&\dTo>{\lambda}\\
  &&IX&\rTo_{\lambda}&X
\end{diagram}
$$
Establishing this (and the analogous equation for the right action)
is a routine calculation which we omit since we will not
actually need the result.
We also note that
  the two actions are compatible---i.e.~constitute a two-sided action.
  Precisely this means that there is a canonical invertible $2$-cell
  \begin{diagram}
  I  X  I & \rTo^{\lambda_X  I}  & X  I  \\
  \dTo<{I  \rho_X}  &  \cel{B}  & \dTo>{\rho_X}  \\
  I  X  & \rTo_{\lambda_X}  & X
  \end{diagram}
  This $2$-cell satisfies two pentagon equations, one for $IIXI$ and one for
  $IXII$.
\end{blanko}

\section{Units in the $2$-category of arrows in $\mathscr{C}$, and Theorem~\ref{thmB}}

\label{sec:catArr}

In this section we prove Theorem~\ref{thmB}, which asserts that
a morphism of units $(u,\cel{U}) : (I,\alpha) \to (J,\beta)$
is automatically a semi-monoid map (with respect to the canonical
associators $\cel A$ and $\cel B$ of the two units).
We have to establish the cube equation of \ref{semimonoid-map},
or in fact the reduced version \eqref{shortSemimonoidMap}.
The strategy to establish Equation~\eqref{shortSemimonoidMap} is to interpret
everything in the $2$-category of arrows of $\mathscr{C}$.  The key point is to prove
that a morphism of units is itself a unit in the $2$-category of arrows.  Then
we invoke Theorem~\ref{thmA} to get an associator for this unit, and a pentagon equation,
whose short form \eqref{shortApentagon} will be
the sought equation.

\begin{blanko}{The $2$-category of arrows.}
  The {\em $2$-category of arrows} in $\mathscr{C}$, denoted $\overrightarrow\CC$, is the $2$-category
described as follows.
The objects of $\overrightarrow\CC$ are the
arrows of $\mathscr{C}$,
$$
X_0 \rTo^x X_1 .
$$
The arrows from $(X_0,X_1,x)$ to $(Y_0,Y_1,y)$ are triples $(f_0,f_1,F)$
where $f_0:X_0 \to Y_0$ and $f_1:X_1\to Y_1$ are arrows in $\mathscr{C}$
and $F$ is a $2$-cell
\begin{diagram}
X_0 & \rTo^{f_0}  & Y_0  \\
\dTo<x  &  F  & \dTo>y  \\
X_1  & \rTo_{f_1}  & Y_1
\end{diagram}
If $(g_0,g_1,G)$ is another arrow from $(X_0,X_1,x)$ to $(Y_0,Y_1,y)$,
a $2$-cell from $(f_0,f_1,F)$ to $(g_0,g_1,G)$ is given by a pair $(m_0,m_1)$
where $m_0: f_0\Rightarrow g_0$ and $m_1: f_1 \Rightarrow g_1$ are
$2$-cells in $\mathscr{C}$ compatible with $F$ and $G$ in the sense that
this cylinder commutes:
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  X_0&\topglob{g_0}\lift{0}{m_0}\dropglob{f_0}&Y_0\\
  \dTo<{x}&\lift{-12}{F}&\dTo>{y}\\
  X_1&\dropglob{f_1}&Y_1
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  X_0&\topglob{g_0}&Y_0\\
  \dTo<{x}&\lift{12}{G}&\dTo>{y}\\
  X_1&\topglob{g_1}\lift{0}{m_1}\dropglob{f_1}&Y_1
\end{diagram}
\vspace{24pt}
$$
Composition of arrows in $\overrightarrow\CC$ is just pasting of squares.
Vertical composition of $2$-cells is just vertical composition of the
components (the compatibility is guaranteed by pasting of cylinders along
squares), and horizontal composition of $2$-cells is horizontal
composition of the components (compatibility guaranteed by
pasting along the
straight sides of the cylinders).
Note that
$\overrightarrow\CC$ inherits a tensor product from $\mathscr{C}$: this follows from
functoriality of the tensor product on $\mathscr{C}$.
\end{blanko}

\begin{lemma}\label{map-canc}
  If $I_0$ and $I_1$ are cancellable objects in $\mathscr{C}$ and $i: I_0 \to
  I_1$
  is an equi-arrow, then $i$ is cancellable in $\overrightarrow\CC$.
\end{lemma}

\begin{dem}
  We have to show that for given arrows $x:X_0 \to X_1$ and $y: Y_0\to
  Y_1$, the functor
  $$
  \operatorname{Hom}_{\overrightarrow\CC}(x,y) \to \operatorname{Hom}_{\overrightarrow\CC}(ix,iy)
  $$
  defined by tensoring with $i$ on the left is an equivalence of
  categories (the check for tensoring on the right is analogous).

  Let us first show that this functor is essentially surjective.
  Let
  \begin{diagram}
  I_0 X_0 & \rTo^{s_0}  & I_0 Y_0  \\
  \dTo<{ix}  & S   & \dTo>{iy}  \\
  I_1 X_1  & \rTo_{s_1}  & I_1 Y_1
  \end{diagram}
  be an object in $\operatorname{Hom}_{\overrightarrow\CC}(ix,iy)$.  We need to find a square
  \begin{diagram}
  X_0 & \rTo^{k_0}  & Y_0  \\
  \dTo<{x}  & K   & \dTo>{y}  \\
  X_1  & \rTo_{k_1}  &Y_1
  \end{diagram}
  and an isomorphism $(m_0,m_1)$ from $(s_0,s_1,S)$ to $(I_0 k_0, I_1 k_1, i
  K)$,
  i.e.~a cylinder
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 X_0&\topglob{I_0 k_0}\lift{0}{m_0}\dropglob{s_0}&I_0 Y_0\\
  \dTo<{ix}&\lift{-12}{S}&\dTo>{iy}\\
  I_1 X_1&\dropglob{s_1}&I_1 Y_1
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 X_0&\topglob{I_0 k_0}&I_0 Y_0\\
  \dTo<{ix}&\lift{12}{i K}&\dTo>{iy}\\
  I_1 X_1&\topglob{I_1 k_1}\lift{0}{m_1}\dropglob{s_1}&I_1 Y_1
\end{diagram}
\vspace{24pt}
$$
Since $I_0$ is a cancellable object, the arrow $s_0$ is isomorphic to $I_0 k_0$
for some $k_0: X_0 \to Y_0$.  Let the connecting
  invertible $2$-cell be denoted $m_0: s_0 \Rightarrow I_0 k_0$.
  Similarly we find $k_1$ and $m_1: s_1
  \Rightarrow I_1 k_1$.  Since $m_0$ and $m_1$ are invertible, there is a unique
  $2$-cell
  \begin{diagram}
  I_0 X_0 & \rTo^{I_0 k_0}  & I_0 Y_0  \\
  \dTo<{ix}  & T   & \dTo>{iy}  \\
  I_1 X_1  & \rTo_{I_1 k_1}  & I_1 Y_1
  \end{diagram}
  that can take the place of $iK$ in the cylinder
  equation; it remains to see that $T$ is of the form $iK$ for some $K$.
  But this follows since the map
  \begin{eqnarray}
    {\rm 2Cell}_{\mathscr{C}}(k_0\# y, x\# k_1) & \longrightarrow & {\rm 2Cell}_{\mathscr{C}}(i(k_0\# y),
    i(x\# k_1))  \notag  \\
    K & \longmapsto & iK \label{iK}
  \end{eqnarray}
  is a bijection.  Indeed, the map factors as `tensoring with $I_0$ on the left'
  followed by `post-composing with $i Y_1$'; the first is a bijection since
  $I_0$ is cancellable, the second is a bijection since $i$ (and hence $i Y_1$) is
  an equi-arrow).

  Now for the fully faithfulness of
  $\operatorname{Hom}_{\overrightarrow\CC}(x,y) \to \operatorname{Hom}_{\overrightarrow\CC}(ix,iy)$.
  Fix two objects in the left-hand category, $P$ and $Q$:
  $$
  \begin{diagram}
  X_0 & \rTo^{p_0}  & Y_0  \\
  \dTo<x  & P   & \dTo>y  \\
  X_1  & \rTo_{p_1}  & Y_1
  \end{diagram}
  \qquad
  \begin{diagram}
  X_0 & \rTo^{q_0}  & Y_0  \\
  \dTo<x  & Q   & \dTo>y  \\
  X_1  & \rTo_{q_1}  & Y_1
  \end{diagram}
$$
The arrows from $P$ to $Q$ are pairs $(m_0,m_1)$ consisting of
$$
m_0: p_0 \Rightarrow q_0 \qquad m_1: p_1 \Rightarrow q_1
$$
cylinder-compatible with the $2$-cells $P$ and $Q$.
The image of these two objects are
$$
\begin{diagram}
I_0 X_0 & \rTo^{I_0 p_0}  & I_0 Y_0  \\
\dTo<{ix}  & iP   & \dTo>{iy}  \\
I_1 X_1  & \rTo_{I_1 p_1}  & I_1 Y_1
\end{diagram}
\qquad
\begin{diagram}
I_0 X_0 & \rTo^{I_0 q_0}  & I_0 Y_0  \\
\dTo<{ix}  & iQ   & \dTo>{iy}  \\
I_1 X_1  & \rTo_{I_1 q_1}  & I_1 Y_1
\end{diagram}
$$
The possible $2$-cells from $iP$ to $iQ$ are
pairs $(n_0,n_1)$ consisting of
$$
n_0: I_0 p_0 \Rightarrow I_0 q_0 \qquad n_1: I_1 p_1 \Rightarrow I_1 q_1
$$
cylinder-compatible with the $2$-cells $iP$ and $iQ$.  Now since $I_0$
is cancellable, every $2$-cell $n_0$ like this is uniquely of the form
$I_0 n_0$ for some $n_0$.  Hence there is a bijection between the
possible $m_0$ and the possible $n_0$.  Similarly for $m_1$ and $n_1$.
So there is a bijection between pairs $(m_0, m_1)$ and pairs $(n_0,
n_1)$.  Now by functoriality of tensoring with $i$, all images of
compatible $(m_0,m_1)$ are again compatible.  It remains to rule out
the possibility that
some $(n_0,n_1)$ pair could be compatible without $(m_0, m_1)$ being so,
but this follows again from the argument that `tensoring with $i$ on the left'
is a  bijection on hom sets, just like argued for \eqref{iK}.
\end{dem}

\begin{lemma}\label{f0f1-equi}
  An arrow in $\overrightarrow\CC$,
  \begin{diagram}
  X_0 & \rTo^{f_0}  & Y_0  \\
  \dTo<x  &  F  & \dTo>y  \\
  X_1  & \rTo_{f_1}  & Y_1
  \end{diagram}
  is an equi-arrow in $\overrightarrow\CC$ if the components
  $f_0$ and $f_1$ are equi-arrows in $\mathscr{C}$ and $F$ is invertible.
\end{lemma}

\begin{dem}
  We can construct an explicit quasi-inverse by choosing quasi-inverses
  to the components.%
\end{dem}

\begin{cor}
  If $(I_0,\alpha_0)$ and $(I_1, \alpha_1)$ are units in $\mathscr{C}$, and
  $(u,\cel{U}): I_0 \to I_1$ is a unit map between them, then
  $$
  u: I_0 \to I_1
  $$
  is a unit object in $\overrightarrow\CC$ with structure map
  \begin{diagram}
  I_0 I_0 & \rTo^{\alpha_0}  & I_0  \\
  \dTo<{uu}  & \cel{U}^{\scriptscriptstyle -1}   & \dTo>u \\
  I_1 I_1  & \rTo_{\alpha_1}  & I_1 .
  \end{diagram}
\end{cor}

\begin{dem}
  The object $u$ is cancellable by Lemma~\ref{map-canc}, and the morphism
  $(\alpha_0,\alpha_1,\cel{U}^{\scriptscriptstyle -1})$ from $uu$ to $u$ is an equi-arrow by
  Lemma~\ref{f0f1-equi}.
\end{dem}

\begin{satz}\label{thmB}
  Let $(I_0,\alpha_0)$ and $(I_1,\alpha_1)$ be units, with canonical
  associators $\cel A_0$ and $\cel A_1$, respectively.  If $(u,\cel{U})$ is a unit map
  from $I_0$ to $I_1$ then it is automatically a semi-monoid map.  That is,
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 I_0 I_0&\rTo^{uuu}&I_1 I_1 I_1\\
  \leftglob{I_0\alpha_0}\lift{0}{\cel A_0}\rightglob{\alpha_0 I_0}&\shuft{20}{\cel{U}u}&\rightglob{\alpha_1 I_1}\\
  I_0 I_0&\rTo_{uu}&I_1 I_1
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 I_0 I_0&\rTo^{uuu}&I_1 I_1 I_1\\
  \leftglob{I_0\alpha_0}&\shuft{-20}{u\cel{U}}&\leftglob{I_1\alpha_1}\lift{0}{\cel A_1}\rightglob{\alpha_1 I_1}\\
  I_0 I_0&\rTo_{uu}&I_1 I_1
\end{diagram}
$$
\end{satz}

\begin{dem}
  By the previous Corollary, $(u,\cel{U}^{\scriptscriptstyle -1})$ is a unit object in $\overrightarrow\CC$.
  Hence there is a canonical associator
  $$
  \cel B : u\cel{U}^{\scriptscriptstyle -1} \Leftrightarrow \cel{U}^{\scriptscriptstyle -1} u .
  $$
  By definition of $2$-cells in $\overrightarrow\CC$, this is a pair of $2$-cells in $\mathscr{C}$
  $$
  \cel B_0 : I_0 \alpha_0 \Rightarrow \alpha_0 I_0
  \qquad
  \cel B_1 : I_1 \alpha_1 \Rightarrow \alpha_1 I_1 ,
  $$
  fitting the cylinder equation
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 I_0 I_0&\topglob{\alpha_0 I_0}\lift{0}{\cel B_0}\dropglob{I_0 \alpha_0}&I_0 I_0\\
  \dTo<{uuu}&\lift{-12}{u \cel{U}^{\scriptscriptstyle -1}}&\dTo>{uu}\\
  I_1 I_1 I_1&\dropglob{I_1 \alpha_1}&I_1 I_1
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  I_0 I_0 I_0&\topglob{\alpha_0 I_0}&I_0 I_0\\
  \dTo<{uuu}&\lift{12}{\cel{U}^{\scriptscriptstyle -1} u}&\dTo>{uu}\\
  I_1 I_1 I_1&\topglob{\alpha_1 I_1}\lift{0}{\cel B_1}\dropglob{I_1 \alpha_1}&I_1 I_1
\end{diagram}
\vspace{24pt}
$$
  This is precisely the cylinder diagram we are looking for---provided we can
  show that $\cel B_0 = \cel A_0$ and $\cel B_1 = \cel A_1$.  But this is a
  consequence of the characterising property of the associator of a unit: first
  note that as a unit object in $\overrightarrow\CC$, $u$ induces left and right constraints: for each
  object $x: X_0 \to X_1$ in $\overrightarrow\CC$ there is a left action of the unit $u$, and
  this left action will induce a left action of $(I_0,\alpha_0)$ on $X_0$
  and a left action of $(I_1,\alpha_1)$ on $X_1$ (the ends of the cylinders).
  Similarly there is a right action of $u$ which induces right actions at the
  ends of the cylinder.  Now the unique $\cel B$ that exists as
  associator for the unit object $u$ compatible with the left and right
  constraints induces $\cel B_0$ and $\cel B_1$ at the ends of the cylinder, and
  these will of course be compatible with the induced left and right
  constraints. Hence, by uniqueness of associators compatible with left and
  right constraints, these induced associators $\cel B_0$ and $\cel B_1$
  must coincide with $\cel A_0$ and
  $\cel A_1$.  Note that this does not dependent on choice of left and right
  constraints, cf.~Proposition~\ref{independence}.
\end{dem}

\section{Contractibility of the space of weak units (Theorem~\ref{thmC})}
\label{sec:contractibility}

The goal of this section is to prove Theorem~\ref{thmC}, which asserts that
the $2$-category of units in $\mathscr{C}$ is contractible if non-empty.
First we describe the unit morphisms and unit $2$-morphisms in terms of
compatibility with left and right constraints.  This will show that there
are not too many $2$-cells. Second we use the left
and right constraints to connect any two units.

The following lemma shows that just as the single arrow $\alpha$ induces all the
$\lambda_X$ and $\rho_X$,
the single $2$-cell $\cel{U}$ of a unit
map induces families $\cel{U}^{\text{\tiny \rm{left}}}_X$ and $\cel{U}^{\text{\tiny \rm{right}}}_X$ expressing
compatibility with $\lambda_X$ and $\rho_X$.

\begin{lemma}\label{unitmap}
  Let $(I,\alpha)$ and $(J,\beta)$ be units, and let
  $(u,\cel{U})$ be a morphism of pseudo-idempotents from $(I,\alpha)$ to $(J,\beta)$.
  The following are equivalent.
\begin{punkt-i}
  \item $u$ is an equi-arrow (i.e.~$u$ is a morphism of units).

  \item $u$ is left cancellable,  i.e.~tensoring with $u$ on the left
   is an equivalence of categories $\operatorname{Hom}(X,Y) \to \operatorname{Hom}(IX,JY)$.

   \item[(ii')] $u$ is right cancellable,  i.e.~tensoring with $u$ on the right
   is an equivalence of categories $\operatorname{Hom}(X,Y) \to \operatorname{Hom}(XI,YJ)$.

  \item For fixed left actions $(\lambda_X,\cel L_X)$ for the unit $(I,\alpha)$ and
  $(\ell_X,\cel L'_X)$ for the unit $(J,\beta)$,
  there is a unique invertible $2$-cell $\cel{U}^{\text{\tiny \rm{left}}}_X$, natural in $X$:
  \begin{diagram}
  IX & \rTo^{uX}  & JX  \\
  \dTo<{\lambda_X}  &  \cel{U}^{\text{\tiny \rm{left}}}_X  & \dTo>{\ell_X}  \\
  X  & \rTo_X  & X
  \end{diagram}
such that this compatibility holds:
\begin{equation}\label{P}
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\rTo^{uuX}&JJX\\
  \leftglob{I\lambda_X}\lift{0}{\cel{L}_X}\rightglob{\alpha X}&\shuft{20}{\cel{U}X}&\rightglob{\beta X}\\
  IX&\rTo_{uX}&JX
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\rTo^{uuX}&JJX\\
  \leftglob{I\lambda_X}&\shuft{-20}{u\cel{U}^{\text{\tiny \rm{left}}}_X}&\leftglob{J\ell_X}\lift{0}{\cel{L}'_X}\rightglob{\beta X}\\
  IX&\rTo_{uX}&JX
\end{diagram}
\end{equation}

  \item[(iii')] For fixed right actions $(\rho_X,\cel R_X)$ for the unit $(I,\alpha)$ and
  $(r_X,\cel R'_X)$ for the unit $(J,\beta)$,
  there is a unique invertible $2$-cell $\cel{U}^{\text{\tiny \rm{right}}}_X$, natural in $X$:
  \begin{diagram}
  XI & \rTo^{Xu}  & XJ  \\
  \dTo<{\rho_X}  &  \cel{U}^{\text{\tiny \rm{right}}}_X  & \dTo>{r_X}  \\
  X  & \rTo_X  & X
  \end{diagram}
such that this compatibility holds:
\begin{equation}\label{Q}
\begin{diagram}[w=6ex,h=6ex,tight]
  XII&\rTo^{Xuu}&XJJ\\
  \leftglob{X\alpha}\lift{0}{\cel{R}_X}\rightglob{\rho_X I}&\shuft{20}{\cel{U}^{\text{\tiny \rm{right}}}_X u}&\rightglob{r_X J}\\
  XI&\rTo_{Xu}&XJ
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XII&\rTo^{Xuu}&XJJ\\
  \leftglob{X\alpha}&\shuft{-20}{X\cel{U}}&\leftglob{X\beta}\lift{0}{\cel{R}'_X}\rightglob{r_X J}\\
  XI&\rTo_{Xu}&XJ
\end{diagram}
\end{equation}

\end{punkt-i}
\end{lemma}

\begin{dem}
  (i) implies (ii):   `tensoring with $u$' can be done in two steps:
  given an arrow $X \to Y$, first tensor with $I$ to get $IX \to IY$,
  and then post-compose with $uY$ to get $IX \to JY$.  The first step
  is an equivalence because $I$ is a unit, and the second step is an
  equivalence because $u$ is an equi-arrow.

  (ii) implies (iii):
In Equation~(\ref{P}), the $2$-cell labelled $u\cel{U}^{\text{\tiny \rm{left}}}_X$ is uniquely
defined by the three other cells, and it is invertible since the three other
cells are.  Since tensoring with $u$ on the
left is an equivalence, this cell comes from a unique invertible cell
$\cel{U}^{\text{\tiny \rm{left}}}_X$,
justifying the label $u\cel{U}^{\text{\tiny \rm{left}}}_X$.

(iii) implies (i): The invertible $2$-cell $\cel{U}^{\text{\tiny \rm{left}}}_X$ shows that $uX$ is
  isomorphic to an equi-arrow, and hence is an equi-arrow itself.  Now take $X$
  to be a right cancellable object (like for example $I$) and conclude that
  already $u$ is an equi-arrow.

  Finally, the equivalence
  (i)$\Rightarrow$(ii')$\Rightarrow$(iii')$\Rightarrow$(i) is completely analogous.
\end{dem}

Note that for $(u,\cel U)$ the identity morphism on $(I,\alpha)$, we recover
Observation~\ref{lambda-lambda}.

\begin{lemma}\label{unit2map}
  Let $(I,\alpha)$ and $(J,\beta)$ be units; let $(u,\cel{U})$ and $(v,\cel{V})$
  be morphisms of pseudo-idempotents from $I$ to $J$; and consider a
  $2$-cell $\cel T: u\Rightarrow v$.  Then
  the following are equivalent.
  \begin{punkt-i}
    \item $\cel T$ is an invertible $2$-morphism of pseudo-idempotents.

    \item $\cel T$ is a left cancellable $2$-morphism of pseudo-idempotents
    (i.e., induces a bijection on hom sets (of hom cats) by tensoring with
    $\cel T$ from the left).

    \item[(ii')] $\cel T$ is a right cancellable $2$-morphism of pseudo-idempotents
    (i.e., induces a bijection on hom sets (of hom cats) by tensoring with
    $\cel T$ from the right).

    \item For fixed left actions $(\lambda_X, \cel L_X)$ for $(I,\alpha)$
    and $(\ell_X,\cel L'_X)$ for $(J,\beta)$,
    with induced canonical $2$-cells $\cel{U}^{\text{\tiny \rm{left}}}_X$ and
    $\cel{V}^{\text{\tiny \rm{left}}}_X$ as in \ref{unitmap}, we have:
\vspace{24pt}
\begin{equation}\label{TXP}
\begin{diagram}[w=6ex,h=6ex,tight]
  IX&\topglob{vX}\lift{0}{\cel T X}\dropglob{uX}&JX\\
  \dTo<{\lambda_X}&\lift{-12}{\cel{U}^{\text{\tiny \rm{left}}}_X}&\dTo>{\ell_X}\\
  X&\dropglob{X}&X
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IX&\topglob{vX}&JX\\
  \dTo<{\lambda_X}&\lift{12}{\cel{V}^{\text{\tiny \rm{left}}}_X}&\dTo>{\ell_X}\\
  X&\topglob{X}\lift{0}{\copyright}\dropglob{X}&X
\end{diagram}
\vspace{24pt}
\end{equation}

    \item[(iii')] For fixed right actions $(\rho_X,\cel R_X)$ for $(I,\alpha)$
    and $(r_X,\cel R'_X)$ for $(J,\beta)$, with induced canonical $2$-cells $\cel{U}^{\text{\tiny \rm{right}}}_X$ and
    $\cel{V}^{\text{\tiny \rm{right}}}_X$ as in \ref{unitmap}, we have:
\vspace{24pt}
\begin{equation}\label{TXQ}
\begin{diagram}[w=6ex,h=6ex,tight]
  XI&\topglob{Xv}\lift{0}{X\cel T}\dropglob{Xu}&XJ\\
  \dTo<{\rho_X}&\lift{-12}{\cel{U}^{\text{\tiny \rm{right}}}_X}&\dTo>{r_X}\\
  X&\dropglob{X}&X
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XI&\topglob{Xv}&XJ\\
  \dTo<{\rho_X}&\lift{12}{\cel{V}^{\text{\tiny \rm{right}}}_X}&\dTo>{r_X}\\
  X&\topglob{X}\lift{0}{\copyright}\dropglob{X}&X
\end{diagram}
\vspace{24pt}
\end{equation}
\end{punkt-i}
\end{lemma}

\begin{dem}
  It is obvious that (i) implies (ii).
  Let us prove that (ii) implies (iii), so assume that tensoring with
  $\cel T$ on the left defines a bijection on the level of $2$-cells.
  Start with the cylinder diagram for compatibility of tensor
  $2$-cells (cf.~\ref{semimonoid-transf}).  Tensor this diagram with $X$ on
  the right to get
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{vvX}\lift{0}{\cel{TT}X}\dropglob{uuX}&JJX\\
  \dTo<{\alpha X}&\lift{-12}{\cel{U}X}&\dTo>{\beta X}\\
  IX&\dropglob{uX}&JX
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{vvX}&JJX\\
  \dTo<{\alpha X}&\lift{12}{\cel{V}X}&\dTo>{\beta X}\\
  IX&\topglob{vX}\lift{0}{\cel{T}X}\dropglob{uX}&JX
\end{diagram}
\vspace{24pt}
$$
On each side of this equation, paste an $\cel L_X$ along $\alpha X$,
apply Equation~\eqref{P} on each side, and cancel the $\cel L'_X$
that appear on the other side of the square.
The resulting diagram
\vspace*{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{vvX}\lift{0}{\cel{TT}X}\dropglob{uuX}&JJX\\
  \dTo<{I\lambda_X}&\lift{-12}{u \cel{U}^{\text{\tiny \rm{left}}}_X}&\dTo>{J \ell_X}\\
  IX&\dropglob{uX}&JX
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\topglob{vvX}&JJX\\
  \dTo<{I\lambda_X}&\lift{12}{v\cel{V}^{\text{\tiny \rm{left}}}_X}&\dTo>{J \ell_X}\\
  IX&\topglob{vX}\lift{0}{\cel{T}X}\dropglob{uX}&JX
\end{diagram}
\vspace{24pt}
$$
is the tensor product of $\cel T$
with the promised equation \eqref{TXP}.
Since $\cel T$ is cancellable, we can cancel it away to finish.

(iii) implies (i): the arguments in (ii)$\Rightarrow$(iii) can be
reverted: start with \eqref{TXP}, tensor with $\cel T$ on the left, and apply
\eqref{P} to arrive at the axiom for being a $2$-morphism of pseudo-idempotents.
Since both $\cel{U}^{\text{\tiny \rm{left}}}_X$ and $\cel{V}^{\text{\tiny \rm{left}}}_X$ are invertible, so is $\cel T X$.
Now take $X$ to be a right cancellable object, and cancel it away to conclude
that already $\cel T$ is invertible.

  Finally, the equivalence
  (i)$\Rightarrow$(ii')$\Rightarrow$(iii')$\Rightarrow$(i) is completely analogous.
\end{dem}

\begin{cor}\label{unique-2-cell}
  Given two parallel morphisms of units, there is a unique unit $2$-morphism
  between them.
\end{cor}

\begin{dem}
  The  $2$-cell is determined by the previous lemma.
\end{dem}

Next we aim at proving that there is a unit morphism between any two
units.  The strategy is to use the left and right constraints to
produce a unit morphism
$$
I \rTo IJ \rTo J.
$$
As a first step towards this goal we have:
\begin{lemma}\label{IJunit}
  Let $I$ and $J$ be units, and pick a left constraint $\lambda$ for
  $I$ and a right constraint $r$ for $J$.  Put
  $$
  \gamma \: {\raisebox{0.255ex}{\normalfont\scriptsize :\!\!}}= r_I \lambda_J : IJIJ \to IJ
  $$
Then $(IJ, \gamma)$ is a unit.
\end{lemma}

\begin{dem}
  Since $I$ and $J$ are cancellable, clearly $IJ$ is cancellable too.
  Since $\lambda_J$ and $r_I$ are equi-arrows, $\gamma$ is too.
\end{dem}

\begin{lemma}\label{lambdasemimonoidmap}
  There is a $2$-cell
  \begin{diagram}[w=6ex,h=4.5ex,tight]
  IJIJ & \rTo^{\lambda_J \lambda_J}  & JJ  \\
  \dTo<\gamma  &  \cel{Z}  & \dTo>\beta  \\
  IJ  & \rTo_{\lambda_J}  & J .
  \end{diagram}
Hence $(\lambda_J,\cel{Z})$ is a unit map.  (And there is another
$2$-cell making $r_I$ a unit map.)
\end{lemma}

\begin{dem}
  The $2$-cell $\cel{Z}$ is defined like this:
  \begin{diagram}[w=48pt,h=36pt,tight,hug]
    IJIJ & &  \\
    \dTo<{IJ\lambda_J}  & \diagonaltopglob{\lambda_J \lambda_J} &  \\
    IJJ & \thintopglob{\lambda_J J}\lift{-2}{\cel{K}^\lambda}\thindropglob{\lambda_{JJ}}
  & JJ  \\
    \thinleftglob{r_I J}\lift{0}{\cel R^{\scriptscriptstyle -1}}\thinrightglob{I\beta}  &
    \lambda_\beta  & \dTo>\beta  \\
  IJ  & \rTo_{\lambda_J}  & J
  \end{diagram}
  where the $2$-cell $\cel K^\lambda$ is constructed in Lemma~\ref{lambdaXY}.
\end{dem}

\begin{cor}\label{exist}
  Given two units, there exists a unit morphism between them.
\end{cor}

\begin{dem}
  Continuing the notation from above,
  by Lemma~\ref{IJunit}, $(IJ,\gamma)$ is a unit, and by
  Lemma~\ref{lambdasemimonoidmap}, $\lambda: IJ \to J$ is a morphism of
  units.
  Similarly, $r: IJ \to I$ is a unit morphism, and by Lemma~\ref{inv} any
  chosen pseudo-inverse $r^{\scriptscriptstyle -1} : I \to IJ$ is again a unit morphism.
  Finally we take
  $$
  I \stackrel{r^{\scriptscriptstyle -1}}\rTo IJ \stackrel{\lambda}\rTo J.
  $$
\end{dem}

\begin{satz}[Contractibility]\label{thmC}
  The $2$-category of units in $\mathscr{C}$ is contractible, if non-empty.
In other words, between any two units there exists a unit morphism, and
between any two parallel unit morphisms there is a unique unit
$2$-morphism.
\end{satz}

\begin{dem}
  By Lemma~\ref{exist} there is a unit morphism between any two units
  (an equi-arrow by definition), and by Lemma~\ref{unique-2-cell}
  there is a unique unit $2$-morphism between any two parallel unit morphisms.
\end{dem}

\section{Classical units}

\label{sec:classical}

In this section we review the classical theory of units
in a monoidal $2$-category, as extracted from the definition
of tricategory of Gordon, Power, and Street~\cite{Gordon-Power-Street}.
In the next section we compare this notion with the cancellable-idempotent
approach of this work.  The equivalence is stated explicitly in
Theorem~\ref{thmE}.

\begin{blanko}{Tricategories.}
  The notion of tricategory introduced by Gordon, Power, and
  Street~\cite{Gordon-Power-Street} is is roughly a weak category structure
  enriched over bicategories: this means that the structure maps (composition
  and unit) are weak $2$-functors satisfying weak versions of associativity and
  unit constraints.  For the associativity, the pentagon equation is replaced by
  a specified pentagon $3$-cell (TD7), required to satisfy an equation
  corresponding to the $3$-dimensional associahedron.  This equation (TA1) is
  called the nonabelian $4$-cocycle condition.  For the unit structure, three
  families of $3$-cells are specified (TD8): one corresponding to the Kelly
  axiom, one left variant, and one right variant (those two being the
  higher-dimensional analogues of Axioms (2) and (3) of monoidal category).  Two
  axioms are imposed on these three families of $3$-cells: one (TA2) relating
  the left family with the middle family, and one (TA3) relating the right
  family with the middle family.  These are called left and right normalisation.
  (These two axioms are the higher-dimensional analogues of the first argument
  in Kelly's lemma~\ref{Kelly-lemma}.)  It is pointed out in
  \cite{Gordon-Power-Street} that the middle family together with the axioms
  (TA2) and (TA3) completely determine the left and right families if they
  exist.
\end{blanko}

\begin{blanko}{Monoidal $2$-categories.}
  By specialising the definition of tricategory to the one-object case, and
  requiring everything strict except the units, we arrive at the following
  notion of monoidal $2$-category:
  a {\em monoidal $2$-category} is a semi-monoidal $2$-category
  (cf.~\ref{semimonoidal}) equipped with an object $I$,
two natural transformations $\lambda$ and $\rho$
with equi-arrow components
$$
\lambda_X: IX \to X
$$
$$
\rho_X : XI \to X
$$
and (invertible) $2$-cell data
$$
    \begin{diagram}
    I  X  & \rTo^{\lambda_X}  & X  \\
    \dTo<{I f}  &  \lambda_f  & \dTo>f  \\
    I  Y   & \rTo_{\lambda_Y}  & Y
    \end{diagram}
\qquad\qquad
    \begin{diagram}
    XI  & \rTo^{\rho_X}  & X  \\
    \dTo<{f I}  &  \rho_f  & \dTo>f  \\
    YI   & \rTo_{\rho_Y}  & Y ,
    \end{diagram}
$$
together with three natural modifications $\cel K$, $\cel K^\lambda$,
and $\cel K^\rho$, with invertible components
\begin{align*}
\cel K \; : X \lambda_Y &\Rightarrow \rho_X Y \\
\cel K^\lambda : \lambda_{XY} &\Rightarrow \lambda_X Y \\
\cel K^\rho : X \rho_Y &\Rightarrow \rho_{XY}  .
\end{align*}
We call $\cel K$ the {\em Kelly cell}.

These three families are
subject to the following two equations:
\begin{equation}\label{TA2}
  \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  X \lambda_{YZ} \ar@{=>}[rr]^{X\cel K^\lambda_{Y,Z}} \ar@{=>}[dr]_{\cel K_{X,YZ}} && X\lambda_Y Z \ar@{=>}[dl]^{\cel K_{X,Y} Z} \\
  & \rho_X YZ &
  }
\end{equation}
\begin{equation}\label{TA3}
  \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  X\rho_Y Z \ar@{=>}[rr]^{\cel K^\rho_{X,Y} Z} \ar@{<=}[dr]_{X\cel K_{Y,Z}} &&
  \rho_{XY} Z \ar@{<=}[dl]^{\cel K_{XY,Z}} \\
  & XY\lambda_Z &
  }
\end{equation}
\end{blanko}

\begin{BM}
  We have made one change compared to \cite{Gordon-Power-Street}, namely the
  direction of the arrow $\rho_X$: from the viewpoint of $\alpha$ it seems more
  practical to work with $\rho_X:XI\to X$ rather than with the convention of
  $\rho_X : X \to XI$ chosen in \cite{Gordon-Power-Street}.  Since in any case
  it is an equi-arrow, the difference is not essential.  (Gurski in his
  thesis~\cite{Gurski:PhD} has studied a version of tricategory where all the
  equi-arrows in the definition are equipped with specified pseudo-inverses.
  This has the advantage that the definition becomes completely algebraic, in a
  technical sense.)
\end{BM}

\begin{lemma}\label{Icanc}
  The object $I$ is cancellable
  (independently of the existence of $\cel K$, $\cel K^\lambda$, and $\cel
  K^\rho$.)
\end{lemma}

\begin{dem}
  We need to establish that `tensoring with $I$ on the left',
  $$
  \mathbb{L} : \operatorname{Hom}(X,Y) \to \operatorname{Hom}(IX,IY) ,
  $$
  is an equivalence of categories.  But this follows since the diagram
  \begin{diagram}[w=9ex,h=6ex,tight]
  \operatorname{Hom}(X,Y) & \rTo^{\mathbb{L}}  & \operatorname{Hom}(IX,IY)  \\
  \dTo<\operatorname{Id}  &    & \dTo>{ \_ \;\#\; \lambda_Y}  \\
  \operatorname{Hom}(X,Y)  & \rTo_{\lambda_X \;\#\; \_}  & \operatorname{Hom}(IX,Y)
  \end{diagram}
  is commutative up to isomorphism: the component at $f:X\to Y$ of this
  isomorphism is just the naturality square $\lambda_f$.  Since the functors
  $\lambda_X \,\#\, \_$ and $ \_ \,\#\, \lambda_Y$ are equivalences, it
  follows from this isomorphism that $\mathbb{L}$ is too.
\end{dem}

\begin{blanko}{Coherence of the Kelly cell.}\label{Klambda-from-K}
  As remarked in~\cite{Gordon-Power-Street}, if the $\cel K^\lambda$ and $\cel
  K^\rho$ exist, they are determined uniquely from $\cel K$ and the two axioms.
  Indeed, the two equations
\begin{equation}\label{KKK}
  \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  I \lambda_{YZ} \ar@{=>}[rr]^{I\cel K^\lambda_{Y,Z}} \ar@{=>}[dr]_{\cel K_{I,YZ}} && I\lambda_Y Z \ar@{=>}[dl]^{\cel K_{I,Y} Z} \\
  & \rho_I YZ &
  }
  \qquad\qquad
   \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  X\rho_Y I \ar@{=>}[rr]^{\cel K^\rho_{X,Y} I} \ar@{=>}[dr]_{X\cel K_{Y,I}} && \rho_{XY} I \ar@{=>}[dl]^{\cel K_{XY,I}} \\
  & XY\lambda_I &
  }
\end{equation}
which are just special cases of \eqref{TA2} and \eqref{TA3} uniquely determine
$\cel K^\lambda$ and $\cel K^\rho$, by cancellability of $I$.
But these two special cases of the axioms do not imply the general case.

We shall take the Kelly cell $\cel K$ as the main structure, and say that $\cel
K$ is {\em coherent on the left} (resp.~{\em on the right}) if Axiom~\eqref{TA2}
(resp.~\eqref{TA3}) holds for the induced cell $\cel K^\lambda$ (resp.~$\cel
K^{\rho}$).  We just say {\em coherent} if both hold.  We shall
see (\ref{KLR}) that in fact coherence on the left implies coherence on the
right and vice versa.
\end{blanko}

\begin{blanko}{Naturality.}\label{natK}
  The Kelly cell is a modification.  For future reference we spell out the
  naturality condition satisfied: given arrows
  $f: X \to X'$ and $g: Y \to Y'$, we have
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\topglob{\rho_X Y}\lift{0}{\cel K_{X,Y}}\dropglob{X\lambda_Y}&XY\\
  \dTo<{fIg}&\lift{-12}{f \lambda_g}&\dTo>{fg}\\
  X'IY'&\dropglob{X'\lambda_{Y'}}&X'Y'
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\topglob{\rho_X Y}&XY\\
  \dTo<{fIg}&\lift{12}{\rho_f g}&\dTo>{fg}\\
  X'IY'&\topglob{\rho_{X'}Y'}\lift{0}{\cel K_{X',Y'}}\dropglob{X'\lambda_{Y'}}&X'Y'
\end{diagram}
\vspace{24pt}
$$
\end{blanko}

\begin{BM}
  Particularly useful is naturality of $\lambda$ with respect to $\lambda_X$
  and naturality of $\rho$ with respect to $\rho_X$.
  In these cases, since $\lambda_X$ and $\rho_X$ are equi-arrows, we can
  cancel them and find the following invertible $2$-cells:
  \begin{align*}
    \cel N^\lambda : I \lambda_X &\Rightarrow \lambda_{IX} \\
    \cel N^\rho\,: \,\rho_{XI} &\Rightarrow X\rho_I ,
  \end{align*}
  in analogy with Observation~(5) of monoidal categories.
\end{BM}

The following lemma holds for $\cel K$ independently of Axioms~\eqref{TA2} and
\eqref{TA3}:
\begin{lemma}\label{NK=KN}
  The Kelly cell $\cel K$ satisfies the equation
\vspace{30pt}
$$
\begin{diagram}[w=9ex,h=7ex,tight]
  XIIY&\bigtopglob{\rho_X IY}\lift{15}{\cel{K}_{X,IY}}\lift{-12}{X\cel
  N^\lambda}\straighthor{X\lambda_{IY}}\bigdropglob{XI\lambda_Y}&XIY
\end{diagram}
  \qquad = \qquad
\begin{diagram}[w=9ex,h=7ex,tight]
  XIIY&\bigtopglob{\rho_X IY}\lift{15}{\cel N^\rho Y}\lift{-15}{\cel K_{XI,Y}}
  \straighthor{\rho_{XI}Y}\bigdropglob{XI\lambda_Y}&XIY
\end{diagram}
\vspace{30pt}
$$
\end{lemma}

\begin{dem}
  It is enough to establish this equation after post-whiskering with
  $X\lambda_Y$.  The rest is a routine calculation, using on one side the
  definition of the cell $\cel N^\lambda$, then naturality of $\cel K$ with
  respect to $f=X$ and $g=\lambda_Y$.  On the other side, use the definition of
  $\cel N^\rho$ and then naturality of $\cel K$ with respect to $f=\rho_X$ and
  $g=Y$.  In the end, two $\cel K$-cells cancel.
\end{dem}

Combining the $2$-cells described so far we get
$$
\rho_I I \stackrel{\cel K^{\scriptscriptstyle -1}}{\Rightarrow} I\lambda_I
\stackrel{\cel N^\lambda}{\Rightarrow} \lambda_{II} \stackrel{\cel
K^\lambda}{\Rightarrow} \lambda_I I
$$
and hence, by cancelling $I$ on the right, an invertible $2$-cell
$$
  \cel P : \rho_I \Rightarrow \lambda_I .
$$
Now we could also define $\cel Q : \rho_I \Rightarrow \lambda_I$
in terms of
$$
I\rho_I \stackrel{\cel K^\rho} \Rightarrow
\rho_{II} \stackrel{\cel N^\rho} \Rightarrow
\rho_I I \stackrel{\cel K^{\scriptscriptstyle -1}}\Rightarrow
 I\lambda_I .
$$
Finally,  in analogy with Axiom~(1) for monoidal categories:
\begin{lemma}\label{U=V}
  We have $\cel P = \cel Q$.  (This is true independently of Axioms~\eqref{TA2}
  and \eqref{TA3}.)
\end{lemma}

\begin{dem}
  Since $I$ is cancellable, it is enough to show $I\cel P I = I\cel Q I$.
  To establish this equation, use the constructions of $\cel P$ and $\cel Q$,
  then substitute the characterising Equations~\eqref{KKK} for the auxiliary cells
  $\cel K^\lambda$ and $\cel K^\rho$, and finally use Lemma~\ref{NK=KN}.
\end{dem}

\begin{blanko}{The $2$-category of GPS units.}\label{GPS}
  For short we shall say {\em GPS unit} for the notion of unit just introduced.
  In summary, a GPS unit is a quadruple $(I, \lambda, \rho, \cel K)$ where $I$
  is an object, $\lambda_X$ and $\rho_X$ are natural transformations
  with equi-arrow components, and $\cel K : X\lambda_Y
  \Rightarrow \rho_X Y$ is a good Kelly cell (natural in $X$ and $Y$, of course).

  A {\em morphism of GPS units} from $(I,\lambda,\rho,\cel K)$ to $(J,\ell, r,
  \cel H)$ is an arrow $u: I \to J$ equipped with natural families of invertible
  $2$-cells
$$
\begin{diagram}
  IX & \rTo^{uX}  & JX  \\
  \dTo<{\lambda_X}  & \cel{U}^{\text{\tiny \rm{left}}}_X   & \dTo>{\ell_X}  \\
  X  & \rTo_X  & X
  \end{diagram}
  \qquad\qquad
  \begin{diagram}
  XI & \rTo^{Xu}  & XJ  \\
  \dTo<{\rho_X}  & \cel{U}^{\text{\tiny \rm{right}}}_X   & \dTo>{r_X}  \\
  X  & \rTo_X  & X
  \end{diagram}
$$
satisfying the equation
\begin{equation}\label{PK}
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\rTo^{XuY}&XJY\\
  \leftglob{X\lambda_Y}\lift{0}{\cel K}\rightglob{\rho_X Y}&\shuft{20}{\cel{U}^{\text{\tiny \rm{right}}}_X Y}&\rightglob{r_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\rTo^{XuY}&XJY\\
  \leftglob{X\lambda_Y}&\shuft{-20}{X\cel{U}^{\text{\tiny \rm{left}}}_Y}&\leftglob{X\ell_Y}\lift{0}{\cel H}\rightglob{r_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
\end{equation}

  Finally, a {\em $2$-morphism of GPS unit maps} is a $2$-cell $\cel T: u
  \Rightarrow v$ satisfying the compatibility conditions \eqref{TXP} and
  \eqref{TXQ} of Lemma~\ref{unit2map}.
\end{blanko}

\begin{blanko}{Remarks.}
  Note first that $u$ is automatically an equi-arrow.  Observe also that
  $\cel{U}^{\text{\tiny \rm{left}}}$ and $\cel{U}^{\text{\tiny \rm{right}}}$ completely determine each other by
  Equation~\eqref{PK}, as is easily seen by taking respectively $X$ to be a left
  cancellable object and $Y$ to be a right cancellable object.  Finally note
  that
  there are two further equations, expressing compatibility with $\cel K^\lambda$
  and $\cel K^\rho$, but they can be deduced from Equation~\eqref{PK},
  independently of the coherence Axioms~\eqref{TA2} and \eqref{TA3}.
  Here is the one for $\cel K^\lambda$
  for future reference:
\begin{equation}\label{KP=PH}
\begin{diagram}[w=6ex,h=6ex,tight]
  IXY&\rTo^{uXY}&JXY\\
  \leftglob{\lambda_{XY}}\lift{0}{\cel K^\lambda}\rightglob{\lambda_X Y}&\shuft{20}{\cel{U}^{\text{\tiny \rm{left}}}_X Y}&\rightglob{\ell_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IXY&\rTo^{uXY}&JXY\\
  \leftglob{\lambda_{XY}}&\shuft{-20}{\cel{U}^{\text{\tiny \rm{left}}}_{XY}}&\leftglob{\ell_{XY}}\lift{0}{\cel H^\ell}\rightglob{\ell_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
\end{equation}
\end{blanko}

\section{Comparison with classical theory (Theorem~\ref{thmE})}
\label{sec:comparison}

In this section we prove the equivalence between the two notions of unit.

\begin{blanko}{From cancellable-idempotent units to GPS units.}
  We fix a unit object $(I,\alpha)$.  We also
  assume chosen a left constraint $\lambda_X : IX \to X$ with $\cel L_X:
  I\lambda_X \Rightarrow \alpha X$, and a right constraint $\rho_X : XI \to X$
  with $\cel R_X: X \alpha \Rightarrow \rho_X I$.  First of all, in analogy with
   Axioms (2) and (3) of monoidal categories we have:
\end{blanko}

\begin{lemma}\label{lambdaXY}
  There are unique natural invertible $2$-cells
  \begin{align*}
    \cel{K}^\lambda : \lambda_{XY} &\Rightarrow \lambda_X Y \\
  \cel K^\rho:  X \rho_Y &\Rightarrow \rho_{XY}
  \end{align*}
  satisfying
\vspace{30pt}
\begin{equation}
  \label{IIAB}
\begin{diagram}[w=6ex,h=6ex,tight]
  IIXY&\topglob{I\lambda_X Y}\lift{0}{I\cel{K}^\lambda}\dropglob{I\lambda_{XY}}&IXY
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=8ex,h=6ex,tight]
  IIXY&\bigtopglob{I\lambda_X Y}\lift{12}{\cel{L}^{\scriptscriptstyle -1} Y}\lift{-12}{\cel{L}}\straighthor{\alpha XY}\bigdropglob{I\lambda_{XY}}&IXY
\end{diagram}
\vspace{30pt}
\end{equation}

\bigskip
\bigskip

\begin{equation}
  \label{XYII}
\begin{diagram}[w=6ex,h=6ex,tight]
  XYII&\topglob{\rho_{XY}I}\lift{0}{\cel K^\rho I}\dropglob{X\rho_Y I}&XYI
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=8ex,h=6ex,tight]
  XYII&\bigtopglob{\rho_{XY}I}\lift{12}{\cel R}\lift{-12}{X\cel R^{\scriptscriptstyle -1}}\straighthor{XY\alpha}\bigdropglob{X\rho_Y I}&XYI
\end{diagram}
\vspace{30pt}
\end{equation}
\end{lemma}

\begin{dem}
  The condition precisely defines the $2$-cell, since $I$ is
  cancellable.
\end{dem}

\begin{lemma}
  For fixed left constraint $(\lambda,\cel L)$ and fixed right
  constraint $(\rho,\cel R)$,
  there is a canonical family of invertible $2$-cells  (the Kelly cell)
  $$
  \cel K : X  \lambda_Y \Rightarrow \rho_X  Y ,
  $$
  natural in $X$ and $Y$.
\end{lemma}

\begin{dem}
  This is analogous to the construction of the associator:
  $\cel K$ is defined as the unique $2$-cell $\cel K: X\lambda_Y
  \Rightarrow \rho_X Y$ satisfying the equation
  \vspace{24pt}
  \begin{equation}\label{RYXL}
  \begin{diagram}[w=52pt,h=39pt,tight]
  XIIY & \thintopglob{X\alpha
  Y}\lift{0}{X\cel{L}}\thindropglob{XI\lambda_Y}  &
  XIY  \\
  \thinleftglob{X\alpha Y}\lift{0}{\cel{R}Y}\thinrightglob{\rho_X IY}  &
  \copyright
  & \dTo>{\rho_X Y}  \\
  XIY  & \rTo_{X\lambda_Y}  & XY
  \end{diagram}
  \qquad = \qquad
    \begin{diagram}[w=30pt,h=22.5pt,tight,hug]
  XIIY &&&&  \\
  &\rdTo^{X\alpha Y} &&&& \\
  && XIY && \\
  &&&\diagonaltopglob{\rho_X Y}
  \diagonaldropglob{X\lambda_Y}\NWSElabel{\cel K}   & \\
  &&&& XY
  \end{diagram}
  \vspace{24pt}
\end{equation}
   This makes sense    since $X\alpha Y$ is an equi-arrow, so we can cancel it
   away.  Clearly $\cel K$ is invertible since $\cel L$ and $\cel R$ are.
\end{dem}

We constructed $\cel K^\lambda$ and $\cel K^\rho$ directly from $\cel L$,
and $\cel R$.  Meanwhile we also constructed $\cel K$,
and we know from classical theory (\ref{Klambda-from-K}) that this cell determines the two
others.  The following proposition shows that all these constructions match up,
and in particular that the constructed Kelly cell is coherent on both sides:

\begin{prop}\label{Kcoh}
  The families of $2$-cells constructed, $\cel K$, $\cel K^\lambda$ and $\cel
  K^\rho$ satisfy the GPS unit axioms~\eqref{TA2} and \eqref{TA3}:
$$
  \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  X \lambda_{YZ} \ar@{=>}[rr]^{X\cel K^\lambda_{Y,Z}} \ar@{=>}[dr]_{\cel K_{X,YZ}} && X\lambda_Y Z \ar@{=>}[dl]^{\cel K_{X,Y} Z} \\
  & \rho_X YZ &
  }
  \qquad\qquad
   \xymatrixrowsep{50pt}
  \xymatrixcolsep{42pt}
  \xymatrix @!=0pt {
  X\rho_Y Z \ar@{=>}[rr]^{\cel K^\rho_{X,Y} Z} \ar@{<=}[dr]_{X\cel K_{Y,Z}} &&
  \rho_{XY} Z \ar@{<=}[dl]^{\cel K_{XY,Z}} \\
  & XY\lambda_Z &
  }
$$
\end{prop}

\begin{dem}
  We treat the left constraint (the right constraint being completely
  analogous).
  We need to establish
  \vspace{30pt}
$$
\begin{diagram}[w=10ex,h=6ex,tight]
  XIYZ&\bigtopglob{\rho_X YZ}\lift{15}{\cel K_{X,Y}Z}
  \lift{-17}{X\cel
  K^\lambda_{Y,Z}}\straighthor{X\lambda_Y Z}\bigdropglob{X\lambda_{YZ}}&XYZ
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=8ex,h=6ex,tight]
  XIYZ&\topglob{\rho_X YZ}\lift{-2}{\cel K_{X,YZ}}\dropglob{X\lambda_{YZ}}&XYZ
\end{diagram}
\vspace{30pt}
$$
and it is enough to establish this equation pre-whiskered with $X\alpha Y Z$.
In the diagram resulting from the left-hand side:
  \vspace{30pt}
$$
\begin{diagram}[w=10ex,h=6ex,tight]
  XIIYZ & \rTo^{X\alpha YZ} &
  XIYZ&\bigtopglob{\rho_X YZ}\lift{15}{\cel K_{X,Y}Z}\lift{-17}{X\cel
  K^\lambda_{Y,Z}}\straighthor{X\lambda_Y Z}\bigdropglob{X\lambda_{YZ}}&XYZ
\end{diagram}
\vspace{30pt}
$$
we can replace $(X\alpha YZ) \# (\cel K_{X,Y}Z)$ by the expression that
defined  $\cel
K_{X,Y}Z$ (cf.~\ref{RYXL}), yielding altogether
\begin{diagram}[w=48pt,h=36pt,tight,scriptlabels,hug]
 &   & XIYZ & & \\
  & \NEdiagonaltopglob{X \alpha YZ}
  \NEdiagonaldropglob{XI\lambda_Y Z}\NESWlabel{X \cel L_Y Z}   &  & \rdTo^{\rho_X YZ}  &  \\
XIIYZ  &    & \copyright & & XYZ \\
  & \diagonaltopglob{\rho_X IYZ}
  \diagonaldropglob{X\alpha YZ}\NWSElabel{\cel{R}_X YZ}  & &\NEdiagonaltopglob{X
  \lambda_Y Z}
  \NEdiagonaldropglob{X\lambda_{YZ}}\NESWlabel{X \cel K^\lambda_{Y,Z}} & \\
  && XIYZ
\end{diagram}
Here we can move the cell $X\cel K^\lambda_{Y,Z}$ across the square,
where it becomes $XI \cel K^\lambda_{Y,Z}$ and combines with $X\cel L_Y Z$
to give altogether $X \cel L_{YZ}$ (cf.~\eqref{IIAB}).
The resulting diagram
\begin{diagram}[w=48pt,h=36pt,tight,scriptlabels,hug]
 &   & XIYZ & & \\
  & \NEdiagonaltopglob{X \alpha YZ}
  \NEdiagonaldropglob{XI\lambda_{YZ}}\NESWlabel{X \cel L_{YZ}}   &  & \rdTo^{\rho_X YZ}  &  \\
XIIYZ  &    & \copyright & & XYZ \\
  & \diagonaltopglob{\rho_X IYZ}
  \diagonaldropglob{X\alpha YZ}\NWSElabel{\cel{R}_X YZ}  & &
  \NEdiagonaldropglob{X\lambda_{YZ}} & \\
  && XIYZ
\end{diagram}
is nothing but
  \vspace{30pt}
$$
\begin{diagram}[w=8ex,h=6ex,tight]
  XIIYZ & \rTo^{X\alpha YZ} &
  XIYZ&\topglob{\rho_X YZ}\lift{-2}{\cel
  K_{X,YZ}}\dropglob{X\lambda_{YZ}}&XYZ
\end{diagram}
\vspace{30pt}
$$
(by Equation~\eqref{RYXL} again)
which is what we wanted to establish.
\end{dem}

Hereby we have concluded the construction of a GPS unit from $(I,\alpha)$.
We will also need a result for morphisms:

\begin{prop}\label{Kelly-compatibility}
  Let $(u,\cel U) :(I,\alpha) \to (J,\beta)$ be a morphism of units in the sense
  of \ref{main-def}, and consider the two canonical $2$-cells $\cel{U}^{\text{\tiny \rm{left}}}$ and
  $\cel{U}^{\text{\tiny \rm{right}}}$ constructed in Lemma~\ref{unitmap}.  Then Equation~\eqref{PK}
  holds:
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\rTo^{XuY}&XJY\\
  \leftglob{X\lambda_Y}\lift{0}{\cel K}\rightglob{\rho_X Y}&\shuft{20}{\cel{U}^{\text{\tiny \rm{right}}}_X Y}&\rightglob{r_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XIY&\rTo^{XuY}&XJY\\
  \leftglob{X\lambda_Y}&\shuft{-20}{X\cel{U}^{\text{\tiny \rm{left}}}_Y}&\leftglob{X\ell_Y}\lift{0}{\cel H}\rightglob{r_X Y}\\
  XY&\rTo_{XY}&XY
\end{diagram}
$$
  (Hence $(u,\cel{U}^{\text{\tiny \rm{left}}},\cel{U}^{\text{\tiny \rm{right}}})$ is a morphism of GPS units.)
\end{prop}
\begin{dem}
  It is enough to prove the equation obtained by pasting the $2$-cell $X\cel{U}
  Y$ on top of each side of the equation.  This enables us to use the
  characterising equation for $\cel K$ and $\cel H$.  After this rewriting, we
  are in position to apply Equations~\eqref{P} and \eqref{Q},
  and after cancelling $\cel R$ and $\cel L$ cells, the
  resulting equation amounts to a cube, where it is easy to see that each side
  is just $\cel{U}^{\text{\tiny \rm{right}}}_X \cel{U}^{\text{\tiny \rm{left}}}_Y$.
\end{dem}

\begin{blanko}{From GPS units to cancellable-idempotent units.}
  Given a GPS unit $(I, \lambda, \rho, \cel K)$, just put
  $$
  \alpha \: {\raisebox{0.255ex}{\normalfont\scriptsize :\!\!}}= \lambda_I ,
  $$
  then $(I,\alpha)$ is a unit object in the sense of \ref{main-def}.  Indeed, we
  already observed that $I$ is cancellable (\ref{Icanc}), and from the outset
  $\lambda_I$ is an equi-arrow.  That's all!  To construct it we didn't even
  need the Kelly cell, or any of the auxiliary cells or their axioms.
\end{blanko}

\begin{blanko}{Left and right actions from the Kelly cell.}\label{LRfromK}
  Start with natural left and right constraints $\lambda$ and
  $\rho$ and a Kelly cell $\cel K : X\lambda_Y \Rightarrow \rho_X Y$ (not
  required to be coherent on either side).  Construct $\cel K^\lambda$ as in
  \ref{Klambda-from-K}, put $\alpha \: {\raisebox{0.255ex}{\normalfont\scriptsize :\!\!}}= \lambda_I$, and define left and right
  actions as follows.
We define $\cel L_X$ as
$$
I\lambda_X \stackrel{\cel N^\lambda}{\Rightarrow} \lambda_{IX}
\stackrel{\cel K^\lambda}{\Rightarrow} \lambda_I X = \alpha X ,
$$
while we define $\cel R_X$ simply as
$$
 X\alpha =  X\lambda_I \stackrel{\cel K_{X,I}}{\Rightarrow}   \rho_X I .
$$
\end{blanko}

\begin{prop}\label{KLR}
  For fixed $(I,\lambda,\rho,\cel K)$, the following are equivalent:
  \begin{punkt-i}
    \item The left and right $2$-cells $\cel L$ and $\cel R$ just constructed in
    \ref{LRfromK} are compatible with the Kelly cell in the sense of
    Equation~\eqref{RYXL}.

    \item The Kelly cell $\cel K$ is coherent on the left
    (i.e.~satisfies Axiom~\eqref{TA2}).

    \item[(ii')] The Kelly cell $\cel K$ is coherent on the right
    (i.e.~satisfies Axiom~\eqref{TA3}).
  \end{punkt-i}
\end{prop}

\begin{dem}
  Proposition~\ref{Kcoh} already says that (i) implies both (ii) and (ii').
  To prove (ii)$\Rightarrow$(i),
  we start with an auxiliary observation: by massaging the naturality equation
\vspace{24pt}
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  XIIY&\topglob{\rho_X IY}\lift{0}{\cel{K}_{X,IY}}\dropglob{X\lambda_{IY}}&XIY\\
  \dTo<{XI\lambda_Y}&\lift{-12}{X\lambda_{\lambda_Y}}&\dTo>{X\lambda_Y}\\
  XIY&\dropglob{X\lambda_Y}&XY
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  XIIY&\topglob{\rho_X IY}&XIY\\
  \dTo<{XI\lambda_Y}&\lift{12}{\copyright}&\dTo>{X\lambda_Y}\\
  XIY&\topglob{\rho_X Y}\lift{0}{\cel{K}_{X,Y}}\dropglob{X\lambda_Y}&XY
\end{diagram}
\vspace{24pt}
$$
we find the equation
\vspace{24pt}
\begin{equation}\label{tailored}
\begin{diagram}[w=7ex,h=7ex,tight]
  XIIY&\topglob{X \lambda_{IY}}\lift{0}{X\cel{N}^\lambda}\dropglob{XI\lambda_Y}&XIY\\
  \dTo<{\rho_X IY}&\lift{-12}{\copyright}&\dTo>{\rho_X Y}\\
  XIY&\rTo_{X\lambda_Y}&XY
\end{diagram}
\qquad = \qquad
\begin{diagram}[w=7ex,h=7ex,tight]
  XIIY&\topglob{X \lambda_{IY}}\lift{0}{\cel{K}^{\scriptscriptstyle -1}_{X,IY}}\dropglob{\rho_X IY}&XIY\\
  \dTo<{\rho_X IY}&\lift{-12}{\copyright}&
  \leftglob{X\lambda_Y}\lift{0}{\cel K_{X,Y}}\rightglob{\rho_X Y}\\
  XIY&\rTo_{X\lambda_Y}&XY
\end{diagram}
\vspace{24pt}
\end{equation}
tailor-made to a substitution we shall perform in a moment.

Now for the main computation, assuming first that $\cel K$ is coherent on the
left, i.e.~that Axiom~\eqref{TA2} holds.  Start with the left-hand side of
Equation~\eqref{RYXL}, and insert the definitions we made for $\cel L$ and $\cel
R$ to arrive at
\vspace{32pt}
$$
\begin{diagram}[w=60pt,h=50pt,tight]
  XIIY & \bigtopglob{X\lambda_I Y}
  \lift{15}{X\cel{K}^\lambda}
  \straighthor{X\lambda_{IY}}
  \lift{-15}{X\cel{N}^\lambda}
  \bigdropglob{XI\lambda_Y}  &
  XIY  \\
  \thinleftglob{X\lambda_I Y}\lift{0}{\cel{K}Y}\thinrightglob{\rho_X IY}  &
  \copyright
  & \dTo>{\rho_X Y}  \\
  XIY  & \rTo_{X\lambda_Y}  & XY
  \end{diagram}
  \vspace{24pt}
$$
in which we can now substitute \eqref{tailored} to get
  \vspace{24pt}
$$
\begin{diagram}[w=72pt,h=60pt,tight]
  XIIY & \bigtopglob{X\lambda_I Y}
  \lift{15}{X\cel{K}^\lambda}
  \straighthor{X\lambda_{IY}}
  \lift{-15}{\cel K^{\scriptscriptstyle -1}_{X,IY}}
  \bigdropglob{\rho_X IY}  &
  XIY  \\
  \thinleftglob{X\lambda_I Y}\lift{0}{\cel{K}_{X,I}Y}\thinrightglob{\rho_X IY}  &
  \copyright
  & \leftglob{X\lambda_Y}\lift{0}{\cel K_{X,Y}}\rightglob{\rho_X Y}  \\
  XIY  & \rTo_{X\lambda_Y}  & XY
  \end{diagram}
  \vspace{24pt}
$$
Here finally the three $2$-cells incident to the $XIIY$ vertex cancel each other out, thanks
to Axiom~\eqref{TA2}, and in the end, remembering $\alpha=\lambda_I$, we get
  \vspace{24pt}
$$
\begin{diagram}[w=36pt,h=28pt,tight,hug]
  XIIY &&&&  \\
  &\rdTo^{X\alpha Y} &&&& \\
  && XIY && \\
  &&&\diagonaltopglob{\rho_X Y}
  \diagonaldropglob{X\lambda_Y}\NWSElabel{\cel K}   & \\
  &&&& XY
  \end{diagram}
  \vspace{24pt}
$$
as required to establish that $\cel K$ satisfies
Equation~\eqref{RYXL}.  Hence we have proved (ii)$\Rightarrow$(i), and therefore
altogether (ii)$\Rightarrow$(ii').  The converse, (ii')$\Rightarrow$(ii) follows now by
left-right symmetry of the statements.  (But note that the proof via (i)
is not symmetric, since it relies on the definition $\alpha=\lambda_I$.
To spell out a proof of (ii')$\Rightarrow$(ii), use rather $\alpha=\rho_I$, observing
that the intermediate result (i) would refer to different
 $\cel L$ and $\cel R$.)
\end{dem}

We have now given a construction in each direction, but both constructions
involved choices.  With careful choices, applying one
construction after the other in either way gets us back where we started.
It is clear that this should constitute an equivalence of $2$-categories.
However, the involved choices make it awkward to make the correspondence
functorial directly.  (In technical terms, the constructions are
ana-$2$-functors.)
We circumvent this by introducing an intermediate $2$-category dominating
both.  With this auxiliary $2$-category, the results we already proved
readily imply the equivalence.

\begin{blanko}{A correspondence of $2$-categories of units.}
  Let $\mathscr{U}$ be following $2$-category.  Its objects are septuples
  $$
  (I,\alpha,\lambda,\rho,\cel L, \cel R,\cel K),
  $$
  with equi-arrows
  $$
  \alpha:II\to I, \quad
  \lambda_X: IX \to X , \quad
  \rho_X : XI \to X,
  $$
  (and accompanying naturality $2$-cell data),
  and natural invertible $2$-cells
  $$
  \cel L : I \lambda_X \Rightarrow \alpha X, \quad
  \cel R: X\alpha \Rightarrow \rho_X I, \quad
  \cel K: X\lambda_Y\Rightarrow \rho_X Y .
  $$
  These data
  are required to satisfy Equation~\eqref{RYXL} (compatibility of $\cel K$ with
  $\cel L$ and $\cel R$).

The arrows in $\mathscr{U}$ from $(I,\alpha,\lambda,\rho,\cel L, \cel R,\cel K)$ to
$(J,\beta,\ell,r,\cel L', \cel R',\cel H)$
are quadruples
$$
(u, \cel{U}^{\text{\tiny \rm{left}}}, \cel{U}^{\text{\tiny \rm{right}}}, \cel U) ,
$$
where $u:I \to J$ is an arrow in $\mathscr{C}$, $\cel{U}^{\text{\tiny \rm{left}}}$ and $\cel{U}^{\text{\tiny \rm{right}}}$
are as in \ref{GPS}, and $\cel U$ is a morphism of pseudo-idempotents from
$(I,\alpha)$ to $(J,\beta)$.  These data are required to satisfy
Equation~\eqref{PK} (compatibility with Kelly cells)
as well as  Equations~\eqref{P} and \eqref{Q} in Lemma~\ref{unitmap} (compatibility
with the left and right $2$-cells).

Finally a $2$-cell from $(u, \cel{U}^{\text{\tiny \rm{left}}}, \cel{U}^{\text{\tiny \rm{right}}}, \cel U)$
to $(v, \cel{V}^{\text{\tiny \rm{left}}}, \cel{V}^{\text{\tiny \rm{right}}}, \cel V)$ is a $2$-cell
$$
\cel T : u \Rightarrow v
$$
required to be a $2$-morphism of pseudo-idempotents (compatibility with $\cel{U}$
and $\cel{V}$ as in \ref{semimonoid-transf}), and to satisfy Equation~\eqref{TXP}
(compatibility with $\cel{U}^{\text{\tiny \rm{left}}}$ and $\cel{V}^{\text{\tiny \rm{left}}}$)  as well as
Equation~\eqref{TXQ} (compatibility with $\cel{U}^{\text{\tiny \rm{right}}}$
and $\cel{V}^{\text{\tiny \rm{right}}}$).

Let $\mathscr{E}$ denote the $2$-category of cancellable-idempotent
units introduced in \ref{main-def},
and let $\mathscr{G}$ denote the $2$-category of GPS units of \ref{GPS}.
We have evident forgetful (strict) $2$-functors
\begin{diagram}[w=4.5ex,h=4.5ex,tight]
  && \mathscr{U} \\
  & \ldTo^{\Phi} && \rdTo^{\Psi} \\
\mathscr{E} &&&& \mathscr{G} .
\end{diagram}
\end{blanko}

\stepcounter{satz}
\begin{satz}[Equivalence]\label{thmE}
  The $2$-functors $\Phi$ and $\Psi$ are $2$-equivalences.
  More precisely they are surjective on objects and strongly fully faithful
  (i.e.~isomorphisms on hom categories).
\end{satz}

\begin{dem}
  The $2$-functor $\Phi$ is surjective on objects by Lemma~\ref{LR} and
  Proposition~\ref{Kcoh}.  Given an arrow $(u,\cel{U})$ in $\mathscr{E}$ and overlying
  objects in $\mathscr{U}$, Lemma~\ref{unitmap} says there are unique $\cel{U}^{\text{\tiny \rm{left}}}$ and
  $\cel{U}^{\text{\tiny \rm{right}}}$, and Proposition~\ref{Kelly-compatibility} ensures the
  required compatibility with Kelly cells (Equation~\eqref{PK}).  Hence $\Phi$
  induces a bijection on objects in the hom categories.  Lemma~\ref{unit2map}
  says we also have a bijection on the level of $2$-cells, hence $\Phi$ is an
  isomorphism on hom categories.  On the other hand, $\Psi$ is surjective on
  objects by \ref{LRfromK} and Proposition~\ref{KLR}.  Given an arrow
  $(u,\cel{U}^{\text{\tiny \rm{left}}},\cel{U}^{\text{\tiny \rm{right}}})$ in $\mathscr{G}$, Lemma~\ref{W} below says that for
  fixed overlying objects in $\mathscr{U}$ there is a unique associated $\cel{U}$, hence
  $\Psi$ induces a bijection on objects in the hom categories.  Finally,
  Lemma~\ref{unit2map} gives also a bijection of
  $2$-cells, hence $\Psi$ is strongly fully faithful.
\end{dem}

\begin{lemma}\label{W}
  Given a morphism of GPS units
  \begin{diagram}[w=12ex,tight]
  (I,\lambda,\rho,\cel K) & \rTo^{(u,\cel{U}^{\text{\tiny \rm{left}}},\cel{U}^{\text{\tiny \rm{right}}})}  &
  (J,\ell,r,\cel H)
  \end{diagram}
  fix an equi-arrow $\alpha: II \isopil I$ with natural families
  $\cel L_X: I\lambda_X \Rightarrow \alpha X$ and $\cel R_X: \alpha X
  \Rightarrow \rho_X I$ satisfying Equation~\eqref{RYXL} (compatibility with
  $\cel K$), and fix an equi-arrow $\beta: JJ \isopil J$ with natural families
  $\cel L'_X: I\ell_X \Rightarrow \beta X$ and $\cel R'_X: \beta X
  \Rightarrow r_X I$ also satisfying Equation~\eqref{RYXL} (compatbility with
  $\cel H$).
  Then there is a unique $2$-cell
    \begin{diagram}
  II & \rTo^{uu}  & JJ  \\
  \dTo<\alpha  &  \cel{U}  & \dTo>\beta  \\
  I  & \rTo_u  & J .
  \end{diagram}
  satisfying Equations~\eqref{P} and \eqref{Q}
  (compatibility with $\cel{U}^{\text{\tiny \rm{left}}}$ and the
  left $2$-cells, as well as compatibility with $\cel{U}^{\text{\tiny \rm{right}}}$ and the right
  $2$-cells).
\end{lemma}

\begin{dem}
  Working first with left $2$-cells, define a family $\cel W_X$ by the
equation
$$
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\rTo^{uuX}&JJX\\
  \leftglob{I\lambda_X}\lift{0}{\cel L_X}\rightglob{\alpha X}&\shuft{20}{\cel W_X}&\rightglob{\beta X}\\
  IX&\rTo_{uX}&JX
\end{diagram}
\qquad\qquad = \qquad\qquad
\begin{diagram}[w=6ex,h=6ex,tight]
  IIX&\rTo^{uuX}&JJX\\
  \leftglob{I\lambda_X}&\shuft{-20}{u \cel{U}^{\text{\tiny \rm{left}}}_X}&\leftglob{J\ell_X}\lift{0}{\cel L'_X}\rightglob{\beta X}\\
  IX&\rTo_{uX}&JX
\end{diagram}
$$
It follows readily from Equation~\eqref{KP=PH} that the family has the property
$$
\cel W_{XY} = \cel W_X Y
$$
for all $X, Y$, and it is a standard argument that since a unit object exists,
for example $(I,\lambda_I)$, this implies that
$$
\cel W_X = \cel{U} X
$$
for a unique $2$-cell
  \begin{diagram}
  II & \rTo^{uu}  & JJ  \\
  \dTo<\alpha  &  \cel{U}  & \dTo>\beta  \\
  I  & \rTo_u  & J ,
  \end{diagram}
  and by construction this $2$-cell has the required compatibility with
  $\cel{U}^{\text{\tiny \rm{left}}}$ and the left constraints.
  To see that this $\cel U$ is also compatible with $\cel{U}^{\text{\tiny \rm{right}}}$ and the
  right constraints we reason backwards: $(u,\cel U)$ is now a morphisms of
  units from $(I,\alpha)$ to $(J,\beta)$ to which we apply the right-hand version of
  Lemma~\ref{unitmap} to construct a new $\cel{U}^{\text{\tiny \rm{right}}}$, characterised by
  the compatibility condition.  By Proposition~\ref{Kelly-compatibility}
  this new $\cel{U}^{\text{\tiny \rm{right}}}$ is compatible with $\cel{U}^{\text{\tiny \rm{left}}}$ and the Kelly
  cells $\cel K$ and $\cel H$ (Equation~\eqref{PK}),
  and hence it must in fact be the original
  $\cel{U}^{\text{\tiny \rm{right}}}$ (remembering from \ref{GPS} that $\cel{U}^{\text{\tiny \rm{left}}}$ and
  $\cel{U}^{\text{\tiny \rm{right}}}$ determine each other via \eqref{PK}).  So the $2$-cell
  $\cel U$ does satisfy both the required compatibilities.
\end{dem}

\hyphenation{mathe-matisk}

redpajama_set_name: RedPajamaArXiv