Terminal objects

Work in progress!

<h3> What is a greatest element?</h3>

Here we gather together some basic results about the ubiquitous and highly significant "terminal objects" in categories.

Perhaps most important are several alternative characterizations of (the "terminal object" ${\rightadj\top}_\calC$) in (an arbitrary category $\calC$) see.

The key result can be described as this:

\[  \boxed{  \displaystyle  {\rightcat 0}_\calC \rightadj\limit \cong \top_\calC \cong {\leftcat 1}_\calC \leftadj\colimit  }   \; .\]

This references two functors into $\calC$, the least, ${\rightcat 0}_\calC$, and the greatest, ${\leftcat 1}_\calC$

( this situation should be compared to (the power set $XP$) of (an arbitrary set $X$), which has two extremal elements, (the empty, least, subset $\emptyset$), and (the greatest subset, $X$ itself) ):

\[ \begin{array} {}    &&&&&  \kern16em  &  \rightcat{  \hom {{{\leftadj !}_{\rightcat 0}}\leftcat c} {[0,\black\calC]} {0_\calC}  }  &  \cong  &  1       \\     \rightcat 0  &  \rightcat{ \xrightarrow[\kern8em]{\textstyle 0_\calC \text{    empty functor}} }  &  \calC  && && \llap{ \text{defn. } \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) \; } {\wr\Vert}  &&  {\wr\Vert} \rlap{ \text{ defn. } {\top_\calC} }     \\      \llap{ {\leftadj !}_{\rightcat 0} } \leftadj{\Bigg\downarrow}  &  \rightadj{   \llap\epsilon \Bigg\Uparrow \rlap{  { \textstyle \text{empty} \atop  \textstyle \text{cone} } }  }  &  \Bigg\Vert   &&&&  \hom {\leftcat c} {\leftcat\calC} { \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) }  &&  \hom {\leftcat c} {\leftcat\calC} {\top_\calC}   \\     1  &  \xrightarrow[\smash{\raise2.4ex{\displaystyle \top_\calC}}]{\kern8em}   &  \calC    \\    \rightadj{  \llap{ !_{\leftcat\calC} } \Bigg\uparrow  }  &  \leftadj{ \llap\eta \Bigg\Uparrow \rlap ! }  &  \Bigg\Vert  & &&&  \rightcat{   \hom { \leftadj ( \leftcat{1_\calC} \leftadj\colimit \leftadj ) } \calC c  }     \\      \leftcat\calC  &  \leftcat{ \xrightarrow[\textstyle 1_\calC \text{    identity functor}]{} }   &  \calC  && &&  \llap{ \text{defn. } \leftadj( \leftcat{1_\calC} \leftadj\colimit \leftadj) \; } {\wr\Vert}   \\      &&&&&  &  \leftcat{  \hom {1_\calC}  {[\calC,\black\calC]}  {{{\rightadj !}_\calC}\rightcat c} }   \\   \end{array}  \]

The isomorphism involving $\rightadj\limit$ is proved by the bijections at top right above.

The isomorphism involving $\leftadj\colimit$ is proved in the diagrams below; 

the two on the left show that 

(a terminal, denoted $\rightadj{\top[\leftadj !]}$) is (a colimit of the identity endofunctor $\leftcat{1_\calC}$),  

while the two on the right show that 

(a colimit, denoted $\leftadj{c_\infty[\iota]}$,  of the identity endofunctor $\leftcat{1_\calC}$) is (a terminal in $\calC$).

\[ \boxed{    \begin{array} {ccccccccc|cccc}  &  {} \rlap{  \kern0em \rightadj{   \top[\leftadj !]   } \text{ is initial in } ({\leftcat{1_\calC}} \downarrow \Delta), \text{ thus is } \leftadj{  (\leftcat{1_\calC} \colimit) [\iota]  }   }   &&&&  &&& &&    {} \rlap{  \kern2em  \leftadj{   ( c_\infty =   \leftcat{1_\calC} \colimit) [\iota] }  \text{ is } \rightadj{ \top [\leftadj !] }   }   &&&    \\  \\   \hline    \kern5em  &  \rightadj\top  &  \leftcat{  \xrightarrow[\kern3em]{ \textstyle \lambda_{\rightadj\top}  }  }  &  \rightcat d    & \kern8em &  \rightadj\top  &  \leftcat{  \xrightarrow[\kern3em]{ \textstyle \rightcat f }  }  &  \rightcat d  &  \kern2em  &  \kern4em  & \leftadj{c_\infty}  &  \leftadj{  \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} }  }  &   \leftadj{c_\infty}        &  \kern2em  &  \kern2em  & \leftadj{c_\infty}  &  \leftadj{  \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} = 1_{c_\infty} }  }  &   \leftadj{c_\infty}     \\    &  \leftadj{  \llap{ !_{\leftcat c} } \Big\uparrow  }  \rlap{ \kern.5em \leftcat\lambda_{ \leftadj!_{\leftcat c} }  }  &  \leftcat{  \nearrow \rlap{\lambda_c}  }   &&&  \leftadj{ \llap{  \rightadj{ {\leftadj !}_\top = 1_\top } } \Big\uparrow  } \rlap{ \kern.5em \rightcat f }  &  \leftcat{  \nearrow \rlap{{\leftcat\lambda}_{\rightadj\top}}  }  & &  &&  \leftadj{  \llap{ \iota_{\leftcat c} } \Big\uparrow   \rlap{ \kern.5em \iota_{\iota_{\leftcat c}}  }  }   &  \leftadj{  \nearrow \rlap{ \iota_{\leftcat c} }  }   &&&&  \leftcat{    \llap{ \forall f } \Big\uparrow   \rlap{ \kern.5em {\leftadj\iota}_f  }    }   &  \leftadj{  \nearrow \rlap{ \iota_{\leftcat c} }  }     \\    &  \leftcat c   &&& &   \rightadj\top &&&  &&  \leftcat{ \llap\forall c }     &&&   &&  \leftcat c          \\          \hline   {} \rlap{    \kern-3em { {  \textstyle \text{if } {\leftcat\lambda} :  \leftcat{1_\calC \Rightarrow {\rightcat d}{\black\Delta} \text{ ($\lambda$ is a cocone from $\leftcat{1_\calC}$ to $\rightcat d$)} \, , } \atop \textstyle \text{then, in particular, $\leftcat{\forall c}$ the above ${\leftcat\lambda}_{ {\leftadj !}_{\leftcat c} }$ commutes,} } \atop \textstyle \text{i.e. $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$} }  }  &&&&  {} \rlap{     \kern4em {    {   \textstyle \text{if } \rightcat{  f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}]  }  \atop \textstyle \text{the above commutes;}  }  \atop  \textstyle \text{hence $\rightcat f = {\leftcat\lambda}_{\rightadj\top}$ }  }    }   &&&&&  {} \rlap{    \kern-2em { {  \textstyle \text{because $\leftadj\iota$ is a cocone, $\leftadj{ \iota : \leftcat{1_\calC} \Rightarrow c_\infty {\black\Delta} }$, }  \atop \textstyle \text{$\leftcat{\forall c}$ the above $\leftadj{\iota_{ \iota_{\leftcat c}}}$ commutes;} } \atop \textstyle \text{hence, by the colimit property, $\leftadj{ \iota_{c_\infty} = 1_{c_\infty} }$} }  }  &&&&&  {} \rlap{    \kern0em { {  \textstyle \text{because $\leftadj\iota$ is a cocone,} \atop \textstyle \text{$\leftcat{\forall f}$ the above ${\leftadj\iota}_f$ commutes;}  }  \atop  \textstyle \text{hence $\leftcat{\forall f}$ $\leftcat{ f = {\leftadj\iota}_c }$}  }  }     \\ \end{array}    }    \]

In words:

To  show $\rightadj{\top[{\leftadj !}]}$ is initial in the comma category $({\leftcat{1_\calC}} \downarrow \Delta)$,

let $\leftcat{ (\lambda : {1_\calC} \Rightarrow {\rightcat d} ) }$ be an arbitrary cocone over $\leftcat{1_\calC}$.

Since $\leftcat\lambda$ is a cocone, the triangle at left commutes.

Thus $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$.

Further, recall $\rightadj{ {\leftadj !}_\top = 1_\top }$ by uniqueness in $\hom {\rightadj\top} \calC {\rightadj\top}$.

Thus if $\rightcat{ f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}] }$, taking $\leftcat{ c = {\rightadj\top} }$ yields $\rightcat{ f = {{\leftcat\lambda}_{\rightadj\top}} }$.

That proves the left assertion in the box above.

<hr />

${\rightadj\top}[{\leftadj !}]$ is an <em>absolute colimit</em>.

(This is (the dual of) CWM Exercise III.4.3.)

 This result may be expressed as saying that:

For any (functor $\leftcat{  F: \calC \to {\rightcat\calD}  }$) 

(the reflection adjunction $\leftadj{!_{\leftcat\calC}} \dashv \rightadj{\top_{\leftcat\calC}}$) induces, via pasting composition,

a "mates" bijection between 2-cells 

$\leftcat{ ( \alpha : F \Rightarrow \leftadj{!_{\leftcat\calC}} {\rightcat d} ) }$ and $\rightcat{ ( \delta : \rightadj{\top_{\leftcat\calC}} {\leftcat F} \Rightarrow {\rightcat d} )  }$, 

that is, of types indicated in the 2-diagram below:

\[ \begin{array} {}  &&  \rightcat\calI  &   \rightcat{   {} \rlap{ \kern-1em \xrightarrow[\kern8em]{} }   }  &&&  \rightcat\calI  &   \rightcat{   {} \rlap{ \kern-1em \xrightarrow[\kern8em]{\textstyle d} }   }  &&&  \rightcat\calD       \\        &  \leftadj{ \llap !_{\leftcat\calC} \nearrow }  &  \smash{    \leftadj{ \llap ! \Big\Uparrow \rlap\eta }    }  &  \rightadj{ \searrow \rlap{  \kern-.5em \top_{\leftcat\calC} }  } &  \smash{    \rightadj{ \Big\Vert \rlap\epsilon  }    }   &  \leftadj{ \nearrow \rlap{ \kern-1em !_{\leftcat\calC}}  }  &  \smash{    \leftadj{   \llap ! \Big\Uparrow \rlap{  \eta \kern0em \leftcat{ \Bigg\Uparrow\rlap{\kern-.7em\alpha} }  }   }    }  &  \rightadj{ \searrow \rlap{  \kern-.5em \top_{\leftcat\calC} }  } &  \smash{    \rightcat{ \Big\Uparrow \rlap\delta }    }  &  \leftcat{  \nearrow \rlap F  }     \\     \leftcat\calC & \leftcat{ {} \rlap{ \kern-1em \smash{ \xrightarrow[\kern8em]{\smash{}} } } } &&& \leftcat\calC & \leftcat{ {} \rlap{ \kern-1em \smash{ \xrightarrow[\kern8em]{\smash{}} } } } &&& \leftcat\calC \\\end{array}  \]

The full-up mates bijection involves a morphism between two adjunctions, (one on the left) and (one on the right).

In the case above, 

(the left adjunction is $\leftadj{!_{\leftcat\calC}} \dashv \rightadj{\top_{\leftcat\calC}}$), 

while (the one on the right is the trivial adjunction $1_\calD \dashv 1_\calD$).

From that POV, the mates bijection would be diagrammed as:

\[ \begin{array} {} && \rightcat\calI & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern8em]{} } } &&& \rightcat\calI & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern8em]{\textstyle d} } } &&& \rightcat\calD \\ & \leftadj{ \llap !_{\leftcat\calC} \nearrow } & \smash{ \leftadj{ \llap ! \Big\Uparrow \rlap\eta } } & \rightadj{ \searrow \rlap{ \kern-.5em \top_{\leftcat\calC} } } & \smash{ \rightadj{ \Big\Vert \rlap\epsilon } } & \leftadj{ \nearrow \rlap{ \kern-1em !_{\leftcat\calC}} } & \smash{ \leftadj{ \llap ! \Big\Uparrow \rlap{ \eta \kern0em \leftcat{ \Bigg\Uparrow\rlap{\kern-.7em\alpha} } } } } & \rightadj{ \searrow \rlap{ \kern-.5em \top_{\leftcat\calC} } } &&  \smash{ \rightcat{ \Bigg\Uparrow \rlap\delta } } &  &  \rightadj{ \searrow \rlap{1_\calD} }        \\        \leftcat\calC & \leftcat{ {} \rlap{ \kern-1em \smash{ \xrightarrow[\kern8em]{\smash{}} } } } &&& \leftcat\calC & \leftcat{ {} \rlap{ \kern-1em \smash{ \xrightarrow[\kern8em]{\smash{}} } } } &&& \leftcat\calC  & \leftcat{ {} \rlap{ \kern-1em \xrightarrow[\textstyle F]{\kern8em} } } &&& \leftcat\calD \\   \end{array} \]

<hr />

This situation may be internally diagrammed in $\leftcat\calC$ and $\rightcat\calD$ as follows.

Given a cocone $\leftcat{ ( \alpha : F \Rightarrow \leftadj{ !_{\leftcat\calC} } {\rightcat d} ) }$ in $\rightcat\calD$, 

then, for each $\leftcat c$ in $\leftcat\calC$, we have the following:

\[   \boxed{   \begin{array} {ccc|cccc}  &  \leftcat{  \calC  \rlap{ {} \xrightarrow[\kern6em]{\textstyle F} }  }  & \kern0em  &  \kern0em  &  \rightcat{    {} \rlap{ \kern1em \calD }   }     \\    \hline  & {\rightadj\top}_{\kern-.2em \leftcat\calC}  &&&   {\rightadj\top}_{\kern-.2em \leftcat\calC} \, {\leftcat F}  &  \rightcat{  \xrightarrow{\textstyle {\rightadj\top}_{\kern-.2em \leftcat\calC} \, \leftcat\alpha} }  &  \rightcat d     \\    &   \leftadj{  \llap{ \exists ! \, !_{\leftcat c} } {\Big\uparrow}  }  \rlap{\leftcat\gamma}   &&&    \leftadj{ \llap{!_{\leftcat c} \, {\leftcat F}} {\Big\uparrow} } \rlap{ \kern.5em {\leftadj !}_{\leftcat c} \, {\leftcat\alpha}  }  &  \leftcat{  \nearrow \rlap{ {\leftcat c} \, \alpha }  }     \\     &  \leftcat{ \llap{\forall} c }  &&&   {\leftcat c} \, {\leftcat F}  \\      \end{array}   }   \]

This is in fact a special case of the more general Yoneda situation.

To clarify the relation, I will keep the same notation, but temporarily 

DROP THE ASSUMPTION THAT $\rightadj\top$ IS A TERMINAL OBJECT.

So consider the situation

\[   \boxed{   \begin{array} {ccc|cccc}  &  \leftcat{  \calC  \rlap{ {} \xrightarrow[\kern7.5em]{\textstyle F} }  }  & \kern0em  &  \kern0em  &  \rightcat{    {} \rlap{ \kern2em \calD }   }     \\    \hline  & {\rightadj\top}_{\kern-.2em \leftcat\calC}  &&&   {\rightadj\top}_{\kern-.2em \leftcat\calC} \, {\leftcat F}  &  \rightcat{  \xrightarrow{\textstyle \delta} }  &  \rightcat d   &  \kern1em     \\     &   \leftcat{  \llap{\forall\gamma} {\Big\uparrow}  }   &&&    \leftcat{ \llap{\gamma F} {\Big\uparrow}   }  &  \leftcat{  \nearrow \rlap{ {\leftcat\gamma} \, \rightcat{(\beta = \hat\delta)} }  }     \\     &  \leftcat{ \llap{\forall} c }  &&&   {\leftcat c} \, {\leftcat F}  \\      \end{array}   }   \]

This gives the direction $\rightcat\delta \mapsto \rightcat{(\beta = \hat\delta)}$ of the classic Yoneda bijection:

\[ \begin{array} {}  \rightcat\delta &  \mapsto  & \rightcat{(\beta = \hat\delta)} \\  \rightcat{ \hom {\rightadj\top \leftcat F} \calD d } & \buildrel \text{Yon} \over \cong & \hom { \leftcat{ \hom - \calC {\rightadj\top} } } {[\leftcat{\calC\op},\Set]} { \rightcat{ \hom { \leftcat{- F} } \calD d } } \\   &&  \leftcat\gamma \mapsto \rightcat{ \big( {\leftcat\gamma}\beta =  \leftcat{\gamma F} \cdot \delta \big) }   \\    &&  {} \rlap{  \kern-10em \text{ $\rightcat{(\beta = \hat\delta)}$ may be viewed as the $\leftcat{\calC\op}$-orbit in $\rightcat\calD$ of $\rightcat\delta$. }  }    \\   \end{array} \]

The earlier result comes from reinstating the assumption that $\rightadj\top$ is terminal, 

and noting that in that case, for a given $\leftcat{c \in \calC}$, there is only one choice for $\leftcat{ \gamma : c \to \rightadj\top }$, namely ${\leftadj !}_{\leftcat c}$, hence here $\rightcat{(\beta = \hat\delta)}$ is a function of $\leftcat{c \in \calC}$ alone, which we denote $\alpha$.

This will be further illustrated below.

<hr />

Although not necessary to understand the above situation, 

it is of interest to me at least to compare the above situation 

to that of the Yoneda lemma.

There is a certain external diagram that is often used in proving the Yoneda lemma, which in this case instantiates to:

\[ \begin{array} {}  \rightadj{1_\top}  &  \leftcat\in  &  \hom {\rightadj\top} {\leftcat\calC} {\rightadj\top}  &  {} \rlap{   \kern-1em  \xrightarrow[\kern2em]{ {\rightadj\top} {\beta} }   }  &  \rightcat{   \hom {{\rightadj\top} {\black F}} \calD d   }  &  \rightcat\ni  &   \rightcat{  \rightadj{1_\top}  \,  (  {\rightadj\top} {\beta} )  = \delta }     \\     &&  \leftcat{   \llap{ \hom \gamma \catC {\rightadj\top} } \Big\downarrow   }  &  {\leftcat\gamma} \beta  &  \rightcat{   \Big\downarrow   \rlap{ \hom {{\leftcat\gamma} {\black F}} \calD d }   }  \\  \llap{ {\leftadj !}_{\leftcat c} = {} } \leftcat\gamma  &  \leftcat\in  &  \hom {\leftcat c} {\leftcat\calC} {\rightadj\top}  &  {} \rlap{   \kern-1em  \xrightarrow[ {\leftcat c} {\beta} ]{\kern2em}   }  &   \rightcat{   \hom {{\leftcat c} {\black F}} \calD d   }  &  \rightcat\ni  &    \rightcat{ {\leftcat\gamma} (\leftcat c \beta) =  \leftcat{\gamma F} \cdot \delta  }    \\     \end{array}  \]

Here we consider how several bijections may be composed, 

demonstrating two alternative ways, mates versus Yoneda, of proving that $\leftadj{ !_{\leftcat\calC} }$ is an absolute colimit:

\[  \begin{array} {}   \leftcat\alpha   && \rightcat{ \delta = \check\beta }  &&     \rightcat{ \beta = \hat\delta }     \\      \leftcat{  \hom F { [\leftcat\calC,\rightcat\calD] } { \leftadj{ !_{\leftcat\calC} } {\rightcat d} }  }   &  \buildrel \text{mates} \over \cong  &   \rightcat{   \hom {\rightadj\top \leftcat F} \calD d   }   & \buildrel \text{Yon} \over \cong  &  \hom {  \leftcat{ \hom - \calC {\rightadj\top} }  }  {[\leftcat{\calC\op},\Set]}  {   \rightcat{  \hom { \leftcat{-  F} } \calD d  }   }   \\   {} \rlap{  \kern-4em  \text{cocone from $\leftcat F$ to $\rightcat d$}  }  &&&&  {\wr\Vert} \rlap{ \text{ if } \rightadj\top \text{ is terminal} }    \\    &&&&   \hom { \leftadj{ !_{\leftcat{\calC\op}} } 1 }  {[\leftcat{\calC\op},\Set]}  {   \rightcat{  \hom { \leftcat{-  F} } \calD d  }   }    \\    &&&&  {\wr\Vert} \rlap{ \text{ remark in proof of CWM Thm. V.4.1} }    \\    &&&&      \hom { \leftcat F }  {[\leftcat\calC,\rightcat\calD]}  {  \leftadj{ !_{\leftcat\calC} } \rightcat d  }     \\   &&&&  \leftcat\alpha     \end{array}    \]

Adjoint triples

Work in progress!

To be expanded.

$\newcommand\inclusion{{\text{inclusion}}}$

First, we give a categorical definition for $\rightadj{ \text{the floor, the right adjoint}}$ to $\leftadj{ \text{the inclusion} }$ of $\leftcat\Z$  in $\rightcat\R$.

\[   \boxed{ \begin{array}  {}   & &&  \rightcat 1 &&  \rightcat{  {}  \rlap{ \kern-4em \xrightarrow[\kern11em] {\lower4ex{\textstyle x}} }  }   && \rightcat{ \R = (\calR \text{ for } \rightadj{\text{floor} =  \left\lfloor \rightcat x \right\rfloor} ) } = \leftcat{ (\calL \text{ for } \leftadj{\text{ceiling} = \left\lceil \leftcat x \right\rceil} ) }     \\    \text{2-categorical diagram in $\Cat$ for } \rightadj{\text{floor} \left\lfloor \rightcat x \right\rfloor}   &  &   \rightcat{ \llap ! \nearrow } &   \smash{ \leftadj{ \llap \lambda \Bigg\Uparrow } }  &  \leftadj{ \searrow \rlap{ \kern-2em \scriptstyle { {\leftcat l} \colimit \atop {} = \rightadj{\left\lfloor {\rightcat x} \right\rfloor} } }  }  & \smash{  \rightadj{\Bigg\Uparrow} \rlap{ \rightcat x \rightadj\epsilon } }   {} \rlap{ \kern-3em \rightcat{ \smash{ \raise.5ex{\Bigg\Uparrow} } \rlap\rho } }  &   \leftadj{ \nearrow \rlap {\inclusion =L} }    \\     &  \rightcat{  ( \leftadj{ (\inclusion = L) }  {} \downarrow x  )  }  &&  \leftcat{  {} \rlap{ \kern-3em \xrightarrow [\textstyle i = l] {\kern8em} } }  &&  \leftcat{ \Z =\calL  }    \end{array} }  \]

(The above 2-categorical diagram in $\Cat$) should be compared to 

the definition of floor in Graham, Knuth, and Patashnik's <i>Concrete Mathematicics</i> (3.1):

⌊x⌋ = the greatest integer less than or equal to x

Note how (the 2-categorical diagram in $\Cat$) makes explicit 

( many entities and relations (arrows) )

which are implicit in (the GKP definition), 

e.g., 

( (the set of objects of) $\rightcat{  ( \leftadj{ (\inclusion = L) }  {} \downarrow x  )  }$ ) 

is

(the collection of $\leftcat{\text{integers}} \rightcat{\text{ less than or equal to } x}$.

<hr />

The following section on terminal objects will be replaced by a reference to a stand-alone, dedicated post in that subject, expanding on what is below.

<hr />

<h3> What is a greatest element?</h3>

Here we drop back to recall and emphasize a key basic result in category theory:

Some alternative characterizations of (the "terminal object" ${\rightadj\top}_\calC$) in (an arbitrary category $\calC$).

The key result can be described as this:

\[  \boxed{  \displaystyle  {\rightcat 0}_\calC \rightadj\limit \cong \top_\calC \cong {\leftcat 1}_\calC \leftadj\colimit  }   \; .\]

This references two functors into $\calC$, the least, ${\rightcat 0}_\calC$, and the greatest, ${\leftcat 1}_\calC$

( this situation should be compared to (the power set $XP$) of (an arbitrary set $X$), which has two extremal elements, (the empty, least, subset $\emptyset$), and (the greatest subset, $X$ itself) ):

\[ \begin{array} {}    &&&&&  \kern16em  &  \rightcat{  \hom {{{\leftadj !}_{\rightcat 0}}\leftcat c} {[0,\black\calC]} {0_\calC}  }  &  \cong  &  1       \\     \rightcat 0  &  \rightcat{ \xrightarrow[\kern8em]{\textstyle 0_\calC \text{    empty functor}} }  &  \calC  && && \llap{ \text{defn. } \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) \; } {\wr\Vert}  &&  {\wr\Vert} \rlap{ \text{ defn. } {\top_\calC} }     \\      \llap{ {\leftadj !}_{\rightcat 0} } \leftadj{\Bigg\downarrow}  &  \rightadj{   \llap\epsilon \Bigg\Uparrow \rlap{  { \textstyle \text{empty} \atop  \textstyle \text{cone} } }  }  &  \Bigg\Vert   &&&&  \hom {\leftcat c} {\leftcat\calC} { \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) }  &&  \hom {\leftcat c} {\leftcat\calC} {\top_\calC}   \\     1  &  \xrightarrow[\smash{\raise2.4ex{\displaystyle \top_\calC}}]{\kern8em}   &  \calC    \\    \rightadj{  \llap{ !_{\leftcat\calC} } \Bigg\uparrow  }  &  \leftadj{ \llap\eta \Bigg\Uparrow \rlap ! }  &  \Bigg\Vert  & &&&  \rightcat{   \hom { \leftadj ( \leftcat{1_\calC} \leftadj\colimit \leftadj ) } \calC c  }     \\      \leftcat\calC  &  \leftcat{ \xrightarrow[\textstyle 1_\calC \text{    identity functor}]{} }   &  \calC  && &&  \llap{ \text{defn. } \leftadj( \leftcat{1_\calC} \leftadj\colimit \leftadj) \; } {\wr\Vert}   \\      &&&&&  &  \leftcat{  \hom {1_\calC}  {[\calC,\black\calC]}  {{{\rightadj !}_\calC}\rightcat c} }   \\   \end{array}  \]

The isomorphism involving $\rightadj\limit$ is proved by the bijections at top right above.

The isomorphism involving $\leftadj\colimit$ is proved in the diagrams below; 

the two on the left show that 

(a terminal, denoted $\rightadj{\top[\leftadj !]}$) is (a colimit of the identity endofunctor $\leftcat{1_\calC}$),  

while the two on the right show that 

(a colimit, denoted $\leftadj{c_\infty[\iota]}$,  of the identity endofunctor $\leftcat{1_\calC}$) is (a terminal in $\calC$).

\[ \boxed{    \begin{array} {ccccccccc|cccc}  &  {} \rlap{  \kern0em \rightadj{   \top[\leftadj !]   } \text{ is initial in } ({\leftcat{1_\calC}} \downarrow \Delta), \text{ thus is } \leftadj{  (\leftcat{1_\calC} \colimit) [\iota]  }   }   &&&&  &&& &&    {} \rlap{  \kern2em  \leftadj{   ( c_\infty =   \leftcat{1_\calC} \colimit) [\iota] }  \text{ is } \rightadj{ \top [\leftadj !] }   }   &&&    \\  \\   \hline    \kern5em  &  \rightadj\top  &  \leftcat{  \xrightarrow[\kern3em]{ \textstyle \lambda_{\rightadj\top}  }  }  &  \rightcat d    & \kern8em &  \rightadj\top  &  \leftcat{  \xrightarrow[\kern3em]{ \textstyle \rightcat f }  }  &  \rightcat d  &  \kern2em  &  \kern4em  & \leftadj{c_\infty}  &  \leftadj{  \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} }  }  &   \leftadj{c_\infty}        &  \kern2em  &  \kern2em  & \leftadj{c_\infty}  &  \leftadj{  \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} = 1_{c_\infty} }  }  &   \leftadj{c_\infty}     \\    &  \leftadj{  \llap{ !_{\leftcat c} } \Big\uparrow  }  \rlap{ \kern.5em \leftcat\lambda_{ \leftadj!_{\leftcat c} }  }  &  \leftcat{  \nearrow \rlap{\lambda_c}  }   &&&  \leftadj{ \llap{  \rightadj{ {\leftadj !}_\top = 1_\top } } \Big\uparrow  } \rlap{ \kern.5em \rightcat f }  &  \leftcat{  \nearrow \rlap{{\leftcat\lambda}_{\rightadj\top}}  }  & &  &&  \leftadj{  \llap{ \iota_{\leftcat c} } \Big\uparrow   \rlap{ \kern.5em \iota_{\iota_{\leftcat c}}  }  }   &  \leftadj{  \nearrow \rlap{ \iota_{\leftcat c} }  }   &&&&  \leftcat{    \llap{ \forall f } \Big\uparrow   \rlap{ \kern.5em {\leftadj\iota}_f  }    }   &  \leftadj{  \nearrow \rlap{ \iota_{\leftcat c} }  }     \\    &  \leftcat c   &&& &   \rightadj\top &&&  &&  \leftcat{ \llap\forall c }     &&&   &&  \leftcat c          \\          \hline   {} \rlap{    \kern-3em { {  \textstyle \text{if } {\leftcat\lambda} :  \leftcat{1_\calC \Rightarrow {\rightcat d}{\black\Delta} \text{ ($\lambda$ is a cocone from $\leftcat{1_\calC}$ to $\rightcat d$)} \, , } \atop \textstyle \text{then, in particular, $\leftcat{\forall c}$ the above ${\leftcat\lambda}_{ {\leftadj !}_{\leftcat c} }$ commutes,} } \atop \textstyle \text{i.e. $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$} }  }  &&&&  {} \rlap{     \kern4em {    {   \textstyle \text{if } \rightcat{  f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}]  }  \atop \textstyle \text{the above commutes;}  }  \atop  \textstyle \text{hence $\rightcat f = {\leftcat\lambda}_{\rightadj\top}$ }  }    }   &&&&&  {} \rlap{    \kern-2em { {  \textstyle \text{because $\leftadj\iota$ is a cocone, $\leftadj{ \iota : \leftcat{1_\calC} \Rightarrow c_\infty {\black\Delta} }$, }  \atop \textstyle \text{$\leftcat{\forall c}$ the above $\leftadj{\iota_{ \iota_{\leftcat c}}}$ commutes;} } \atop \textstyle \text{hence, by the colimit property, $\leftadj{ \iota_{c_\infty} = 1_{c_\infty} }$} }  }  &&&&&  {} \rlap{    \kern0em { {  \textstyle \text{because $\leftadj\iota$ is a cocone,} \atop \textstyle \text{$\leftcat{\forall f}$ the above ${\leftadj\iota}_f$ commutes;}  }  \atop  \textstyle \text{hence $\leftcat{\forall f}$ $\leftcat{ f = {\leftadj\iota}_c }$}  }  }     \\ \end{array}    }    \]

In words:

To  show $\rightadj{\top[{\leftadj !}]}$ is initial in the comma category $({\leftcat{1_\calC}} \downarrow \Delta)$,

let $\leftcat{ (\lambda : {1_\calC} \Rightarrow {\rightcat d} ) }$ be an arbitrary cocone over $\leftcat{1_\calC}$.

Since $\leftcat\lambda$ is a cocone, the triangle at left commutes.

Thus $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$.

Further, recall $\rightadj{ {\leftadj !}_\top = 1_\top }$ by uniqueness in $\hom {\rightadj\top} \calC {\rightadj\top}$.

Thus if $\rightcat{ f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}] }$, taking $\leftcat{ c = {\rightadj\top} }$ yields $\rightcat{ f = {{\leftcat\lambda}_{\rightadj\top}} }$.

That proves the left assertion in the box above.

<hr />

\[ \boxed{ \begin{array} {}    & \leftcat{ ( x \downarrow \rightadj{ (\inclusion = R) }  ) } && \rightcat{ {} \rlap{ \kern-3em \xrightarrow [\kern8em] {\textstyle j = r} } } && \rightcat{ \Z =\calR }    \\      \text{2-categorical diagram in $\Cat$ for } \leftadj{\text{ceiling} \left\lceil \leftcat x \right\rceil} & & \leftcat{ \llap ! \searrow } & \smash{ \raise.5ex{ \rightadj{ \llap \rho \Bigg\Uparrow } } } & \rightadj{ \nearrow \rlap{ \kern-2em \scriptstyle { {\rightcat r} \limit \atop {} = \leftadj{\left\lceil {\leftcat x} \right\rceil} } } } & \smash{ \leftadj{\Bigg\Uparrow} \rlap{ \leftcat x \leftadj\eta } } {} \rlap{ \kern-3em \leftcat{ \smash{ \raise0ex{\Bigg\Uparrow} } \rlap\lambda } } & \rightadj{ \searrow \rlap {\inclusion = R} }    \\    & && \leftcat 1 && \leftcat{ {} \rlap{ \kern-4em \xrightarrow[\textstyle x] {\kern11em} } } && \leftcat{ \R = (\calR \text{ for } \rightadj{\text{floor} = \left\lfloor \rightcat x \right\rfloor} ) } = \leftcat{ (\calL \text{ for } \leftadj{\text{ceiling} = \left\lceil \leftcat x \right\rceil} ) } \\   \end{array} } \]