Doctrines, modalities and comonads

Francesco DagninoDIBRIS, Università di Genova,
email<EMAIL_ADDRESS>Giuseppe RosoliniDIMA, Università di Genova,
email<EMAIL_ADDRESS>
Doctrines are categorical structures very apt to study logics of different nature within
a unified environment: the 2-category of doctrines.
Modal operators are characterised as particular adjoints in the 2-category
. We show that they can be constructed from comonads in as well as from
adjunctions in it, and the two constructions compare. Finally we show the amount of
information lost in the passage from a comonad, or from an adjunction, to the modal

The basis for the present work is provided by some seminal work of John Power.

§ INTRODUCTION

The approach to logic proposed by F.W. Lawvere via hyperdoctrines has proved very fruitful
as it provides an extremely suitable environment where to analyse both syntacic aspects of
logic and semantic aspects as well as compare one with the other, see
[19, 20]. The suggestion is to see a logic as a functor
from the opposite of a category to the category of posets and
monotone functions where the category collects the “types” of the logic and terms in
context, a poset $\Doc(c)$ presents the “properties” of the type $c$ with the order
relation describing their “entailments”.
The reader is referred to operanddoc for the precise details,
but may just keep in mind, for the present discussion, that the
contravariant powerset functor Set is an
instance of a doctrine.

One of the main points of Lawvere's structural approach to logic is that all the logical
operators are obtained from adjunctions. That view in itself is very powerful and
contributes to unifying many different aspects in logic. In the present paper, we show
that also a wide class of modal operators, namely, those satisfying axioms T and 4
as in modality, is obtained from adjunctions.

Typically, modalities are unary logical operators, which are quite well-understood
in the context of propositional logic.
However, their meaning is less clear
in a typed logical formalism.
In this setting, there are various semantics which are interrelated,
and we show that many of these are instances of the general situation of an
adjunction between two homomorphisms of doctrines.

Since they are structured categories, doctrines get swiftly organised in a
2-category. And, as we learned also from the works of John Power, in a 2-category one can
develop a very productive theory of monads and comonads, extending the elementary case of
the 2-category Cat of small categories, functors and natural transfomations.

Doctrines are a rather simple categorical framework for logic, but still capable to cover
a large range of examples. We could have considered more general settings such as indexed
preorders (equivalently, faithful fibrations) or even arbitrary fibrations, but we
preferred to keep things at a very simple level as already there one finds many
interesting examples. Yet, after this first step our plan is to extend results to
general fibrations in future work.

We show that an adjunction in the 2-category of doctrines gives rise to a doctrine with a
modal operator.
An adjunction between doctrines is very much like an adjunction between categories: roughly,
it consists of two doctrines  and  and two homomorphisms of doctrines connecting them,
which should be thought of as an interpretation of in (the left adjoint) and an interpretation of in (the right adjoint).
Such a situation can be summarised by a modal logic which uses the logic to describe properties of  types in (the base category of )
and the modal operator to recover (an image of) properties described by .
In a sense, we extend the logic through the adjunction to a richer logic and use a modal operator to keep memory of the original logic.
As we said, many standard approaches to the semantics of modal logic are instances of such construction.

Taking a slightly different perspective,
we show that also a comonad in the 2-category of doctrines determines a doctrine with a modal operator, this time  on
the category of coalgebras for the comonad.
Intuitively, we get a logic where types have a dynamics, given by the coalgebra structure,
and the modal operator specifies when a property is invariant for such dynamics.

These two constructions are tightly related.
Relying on results in
[8], we show that every comonad in the 2-category of doctrines determines an adjunction,
hence, also a modal operator.
In fact, the construction starting from comonads is defined in this way.
On the other hand, every adjunction determins a comonad, hence a modal operator.
However, the two construction starting from an adjunction do not coincide, but we show they can be canonically
compared by a homomorphism of doctrines preserving the modal operator.

We further our analysis measuring in a categorical form how the
passage to a modal operator hides part of the structure that generated it.

In operanddoc
we introduce interior operators on doctrines, which are the class of modal operators we are interested in.
In background
we recall basic notions about comonads and adjunctions in a general 2-category.
In twocatdoc
we define the 2-categories of doctrines and doctrines with interior operators that are at the core of our analysis.
In adjoint
we show how to construct an interior operator starting from an adjunction between doctrines, while
in comonad
we describe the analogous construction starting from a comonad on a doctrine.
Finally, in picture
we compare the two constructions showing they are part of local adjunctions, in the sense
of [7], between the 2-category of doctrines with modal operator and,
respectively, the 2-category of adjunctions and that of comonads in the 2-category of
In Appendix <ref>
we sketch an example on how to use our construction to obtain models
of the bang modality of linear logic.

§ OPERATORS AND DOCTRINES

A simple semantic approach to propositional standard modal logic (satisfying axioms T and 4)
would consider an operator on a poset H,, a monotone
function HH such that, for all $x \in H$,
$\IntOp(x) \order x$ and $\IntOp(x) \order \IntOp(\IntOp(x))$, see
[12]. The intuition is that the elements of the poset are an
interpretation of (some kind of) formulas, the order relation realizes the entailment
between them, and the operator HH acts as a modality on

From a similar semantic point of view, one could consider a many-sorted logic to be a
doctrine , a (contra)variant functor from a category
to the category of posets and monotone functions. Such a functor is often called an
indexed poset in consonancy with the more general notion of indexed category.

The intuition for a doctrine is that the objects of the category provide the interpretations
of the sorts in the logic and the arrows interpret terms between sorts. For an
object $X$ in , the poset $\Doc X$ gives the interpretations for the formulas expressing
the properties of “arbitrary elements” of $X$—although no set-theoretic determination of
$X$ may have been provided, see [19, 20], but also
[17, 22].

Conjoining these two semantic approaches it is quite natural to consider operators on a doctrine as an extension to many-sorted logic, of the propositional
modal logic satisfying axioms T and 4, like the -modality, a.k.a. necessity
modality, of S4 modal logic.

Let  be a doctrine.
An  modal operator on is a natural
transformation  such that,
for each object $X$ in , the following inequalities hold:

*  $\necmod_X \order_X \id{\Doc X}$

*  $\necmod_X \order_X \necmod_X \circ \necmod_X$

Note that standard axioms of the S4 modal operator, see [4], require
further structure. But here we consider the
very simple structure of a poset on the fibres because we want to
focus mainly on the comonadic structure of the modality.

In the following, an element $\alpha\in\Doc X$ of the form
$\alpha=\necmod_X\beta$ for some $\beta\in\Doc X$  will be called
An immediate consequence of modality, obtained combining
the two requirements on $\necmod$, is that
Hence elements are the fixed points of
$\necmod_X$, that is, those elements $\alpha\in\Doc X$ such that

Let HH be an operator on the poset H,, a monotone
function such that, for all $x \in H$,
$\IntOp(x) \order x$ and $\IntOp(x) \order \IntOp(\IntOp(x))$.
Given this, we can consider two examples of doctrines with operator:

* Let Ĥ be the functor defined on the
category with a single object $\star$ and a single arrow $\id{\star}$
as $\hat{H}(\star) = H$. Then $\IntOp$ is operator
on $\hat{H}$.

* The functor H^(),
which maps a set $X$ to $H^X$ with the pointwise order and a function
tXY to the monotone function ∘tH^YH^X,
is a doctrine. The natural transformation
∘H^()H^() given by
postcomposition with $\IntOp$ is an operator on

Note that the example in (a) is obtained from that in (b) by precomposing the doctrine
H^() with the (opposite of the) functor
⋆↦{0} which maps the one object $\star$ to a(ny) singleton

Consider the category $\Topop$ of topological spaces and open
continuous maps. Define $\fun{\Doc}{\Topop\op}{\Pos}$ as
$\Doc\ple{X,\tau}=\pw{X}$, the powerset of the set $X$, and
$\DReIdx{\Doc}{t}=t^{-1}$, the inverse image along the open
continuous function tX,τY,σ
Let X,τ be a topological space, then $\tau$ is the set of
fixed points of the operator
$\fun{\TopInt_\tau}{\pw{X}}{\pw{X}}$, which maps a subset $A\subseteq X$
to its topological interior.
Since $\TopInt_\tau(A)\subseteq A$ and
$\TopInt_\tau(A)\subseteq\TopInt_\tau(\TopInt_\tau(A))$, for each
$A\subseteq X$, to get an operator on $\Doc$ we need to prove that $\TopInt_\tau$ is natural.
Indeed, consider an open continuous map
$\fun{t}{\ple{X,\tau}}{\ple{Y,\sigma}}$, and a subset
$B\subseteq Y$. So
$t^{-1}(\TopInt_\sigma(B))\subseteq\TopInt_\tau(t^{-1}(B))$ by
continuity of $t$. But also $t(\TopInt_\tau(t^{-1}(B)))\subseteq\TopInt_\sigma(B)$
since the set $t(\TopInt_\tau(t^{-1}(B)))\subseteq B$ is open by openness of $t$. So
$t^{-1}(\TopInt_\sigma(B))=\TopInt_\tau(t^{-1}(B))$ which proves that PP.

A Kripke frame is a pair $\KFr = \ple{W,R}$ where $W$ is the set
of possible worlds and $R\subseteq W\times W$ is the
accesibility relation.
On the poset $\pw{W}$ ordered by set inclusion, consider the
monotone function $\fun{\IntOp_R}{\pw{W}}{\pw{W}}$ defined as

\[ \IntOp_R(A) = \set{w \in W}{R(w) \subseteq A} \]

where $R(w) = \set{v \in W}{\ple{w,v} \in R}$.
When $R$ is reflexive and transitive (a preorder on $W$), for any
$w\in W$, we have $w\in R(w)=R(R(w))$. Hence $\IntOp_R$ is operator.

* As a particular instance of into(b), postcomposition with the
endows the doctrine $\fun{\pw{W}^{(\blank)}}{\Set\op}{\Pos}$ with
an operator.
Intuitively, given a “formula” $\alpha\in\pw{W}^D$, for an element
$x$ of $D$, the set $\alpha(x)\subseteq W$ consists of those worlds
where $x$ satisfies $\alpha$. Indeed, one can see the data consisting
of the Kripke frame and the set $D$ as a constant domain skeleton
as in Definition 1 in [9], where the fibres
$\pw{W}^{D^n}$ enlist all possible interpretations for predicates as $n$ varies.

* Another doctrine with operator
built from a Kripke frame $\KFr$ with a reflexive and transitive
accessibility relation can be obtained via $W$-indexed families.
Consider the category W whose

[objects] are $W$-indexed families of sets, that is, pairs
$X=\ple{\overline{X},(X_w)_{w\in W}}$, where
$X_w\subseteq\overline{X}$, for all $w\in W$, and where
[an arrow] tXY is a function
tXY such that,
for each $w \in W$, $X_w \subseteq t^{-1}(Y_w)$.

Consider the subobject functor
$\fun{\Sub[\Fam{W}]{}}{\Fam{W}\op}{\Pos}$ mapping a $W$-indexed
family to the poset
$\Sub[\Fam{W}]{X}$ of its subfamilies, a family $A$
such that $\overline{A}\subseteq\overline{X}$ and $A_w \subseteq X_w$
for each $w \in W$, ordered by pointwise inclusion.
The action on arrows is defined pointwise by inverse image.
For each $W$-indexed family $X$ the function

\[ \left(\necmod_X A\right)_w = \bigcap_{v \in R(w)} A_v \]

is clearly monotone; and it satisfies conditions (<ref>) and
(<ref>) in modality for the same reason as in
the previous example. Moreover, it is natural in $X$ since, for each
function $\fun{t}{Y}{X}$, we have

\[t^{-1}\big(\left(\necmod_X A\right)_w\big)
=t^{-1} \bigg(\bigcap_{v \in R(w)}A_v\bigg)
=\bigcap_{v \in R(w)}t^{-1}(A_v)=(\necmod_Yt^{-1}(A))_w\]

for any $w\in W$. Though surprising, we shall see in sndex that this example is a
universal completion of the previous one in (a).

Intuitively, given a $W$-indexed family $D$, for each $w\in W$, the subset $D_w$ consists
of those elements of $\overline{D}$ which are present at the world $w$, and, given a
“formula” $\alpha\in \Sub[\Fam W]{D}$, for each world $w\in W$, the set $\alpha_w$
consist of those elements $x$ which are present and satisfy $\alpha$ at $w$.
Indeed, one can see the data consisting
of the Kripke frame and the $w$-indexed family $D$ as a varying domain skeleton
as in Definition 7 in [9], with few additional requirements,
where the fibres $\Sub[\Fam{W}]{D^n}$ enlist all possible interpretations for predicates
as $n$ varies.

* Yet another possibility is to consider a doctrine
over the category of presheaves on the preorder $\KFr$; we shall
discuss this in presh, as a particular case of a more
general construction.

§ ADJUNCTIONS AND COMONADS IN A 2-CATEGORY

In this section we recall basic notions which can be introduced in an arbitrary 2-category
with the purpose to use them in the particular case of the 2-category of doctrines.

Given a (strict) 2-category , we denote 0-cells as $A$, $B$, $C,\ldots$, which we shall
refer to also as objects of ; a 1-cell, also referred to as 1-arrow, from $A$
to $B$ will be written as $\oneAr{a}{A}{B}$ while a 2-cell, or 2-arrow, from the
1-cell $a$ to the 1-cell $b$ will be written as $\twoAr{\alpha}{a}{b}$. Composition of
1-cells and horizontal composition of 2-cells is denoted as $\circ$, and often omitted—we
shall use it mainly to emphasise the composition of functions and functors.
The identity 1-cell on the object $A$ is denoted by A and
the identity 2-cell on the 1-cell $a$ is denoted by a.
A horizontal composition with a 2-identity cell a will be written simply as $\alpha
a$. Vertical composition of 2-cells is denoted as $\cdot$. So, for instance, the defining
property of vertical composition of natural transformations would be written as something
like $(\psi\cdot\phi)_C=\psi_C\circ\phi_C$.

Many well-known concepts from standard category theory can be transferred to an arbitrary
2-category $\K$; a basic reference is [29].

Let be a 2-category.

An adjunction in $\K$ consists of the following data: two
objects $C$ and $D$,
two 1-arrows $\oneAr{l}{C}{D}$ and $\oneAr{r}{D}{C}$, and
two 2-arrows $\twoAr{\unit}{\idobj{C}}{rl}$ and
such that the following triangles of 2-arrows commute

\begin{equation}\label{triai}
\xymatrix@C=3em@R=2em{l\ar@{=>}[r]^-{l\unit}\ar@{=>}[rd]_-{\idar{l}}&
lrl\ar@{=>}[d]^-{\counit l}\\&l}\qquad
\xymatrix@C=3em@R=2em{r\ar@{=>}[r]^-{\unit r}\ar@{=>}[rd]_-{\idar{r}}&
rlr\ar@{=>}[d]^-{r\counit }\\&r.}
\end{equation}

A comonad $\mathbb{c}$ in consists of an object $A$, a 1-arrow
$\oneAr{c}{A}{A}$, and two 2-arrows $\twoAr{\cun}{c}{\idobj{A}}$ and
$\twoAr{\cmu}{c}{cc}$, such that the following diagrams of 2-arrows

\begin{equation}\label{dcom}
\xymatrix@C=3em@R=2em{
c&cc\ar@{=>}[l]^-{c\cun}\ar@{=>}[r]_-{\cun c}&c}\qquad
\xymatrix@C=3em@R=2em{c\ar@{=>}[r]^-{\cmu}\ar@{=>}[d]_-{\cmu}&
cc\ar@{=>}[d]^-{c\cmu}\\cc\ar@{=>}[r]^-{\cmu c}&ccc.}
\end{equation}

*  In line with [29, 26], one says that
admits the Eilenberg-Moore construction for the comonad A,c,,
if there is a universal representation of the following 2-problem: given an object $B$ in ,
objects are pairs x,ξ with

\begin{equation}\label{udata}
\vcenter{\xymatrix@C=4em@R=1ex{&A\ar[dd]^-{c}_(.55){}="t"\\
\ar@{=>}"s";"t"^-{\xi}&A}}
\end{equation}

and such that the diagrams of 2-arrows

\begin{equation}\label{1cohe}
\vcenter{\xymatrix{x\ar@{=>}[r]^-{\xi}\ar@{=>}[d]_-{\xi}&
cx\ar@{=>}[d]^-{\cmu x}\\
\vcenter{\xymatrix{x\ar@{=>}[r]^-{\xi}\ar@{=>}[rd]_-{\idar{x}}&
cx\ar@{=>}[d]^-{\cun x}\\&x}}
\end{equation}

commute; an arrow γx,ξy,ζ is a
2-arrow γxy such that the following diagram commutes

\begin{equation}\label{2cohe}
\vcenter{\xymatrix{x\ar@{=>}[d]_{\gamma}\ar@{=>}[r]^-{\xi}&
\end{equation}

Spelling out the data for an Eilenberg-Moore construction for the comonad
$\mathbb{c}=\ple{A,c,\cmu,\cun}$, it requires that there is an object
A𝕔 in together with a 1-arrow and a 2-arrow as in

\[\xymatrix@C=4em@R=1ex{&A\ar[dd]^-{c}_(.55){}="t"\\
\EM{A}{\mathbb{c}}
\ar[ru]^-{u^{\mathbb{c}}}
\ar[rd]_-{u^{\mathbb{c}}}^(.68){}="s"\\
\ar@{=>}"s";"t"^-{\omega^{\mathbb{c}}}&A}\]

which satisfy the commutative diagrams in (<ref>). Moreover, for any
object $B$ in , every pair x,ξ as in (<ref>) satisfying (<ref>) can
be obtained by precomposition

\[\vcenter{\xymatrix@C=4em@R=1ex{&A\ar[dd]^-{c}_(.55){}="t"\\
\ar@{=>}"s";"t"^-{\xi}&A}}=
\vcenter{\xymatrix@C=1.5em@R=1ex{&&&A\ar[dd]^-{c}_(.55){}="t"\\
\ar[rru]^-{u^{\mathbb{c}}}
\ar[rrd]_-{u^{\mathbb{c}}}^(.68){}="s"\\

for a unique 1-arrow x'BA𝕔, and similarly for arrows
γx,ξy,ζ between pairs:

\[\vcenter{\xymatrix@C=4em@R=1ex{B\ar@<1ex>@/^/[r]^-x_{}="s"
\ar@<-1ex>@/_/[r]_-y^{}="t"&A\ar@{=>}"s";"t"^-{\gamma}}}=
\vcenter{\xymatrix@C=1.5em@R=1ex{B\ar@<1ex>@/^/[rr]^-{x'}_{}="s"
\ar@<-1ex>@/_/[rr]_-{y'}^{}="t"&&
\EM{A}{\mathbb{c}}\ar@{=>}"s";"t"^-{\gamma'}\ar[r]^-{u^{\mathbb{c}}}&A}}\]

for a unique 2-arrow γ'x'y' in .

In case the universality condition is verified for each comonad in , it can be restated
in terms of a 2-adjunction after introducing the appropriate[There are many
reasonable 2-categories whose objects are adjunctions in . In this paper, the 2-category
we introduce is the one that gives rise to the 2-adjunction with .]
2-category  of adjunctions in and the 2-category  of comonads in
. Since we can safely refer the reader to [26] for a very clear presentation
of the general setup, we limit ouselves to recapping the main diagram of 2-adjunctions:

\begin{equation}\label{maind}
\vcenter{\xymatrix{
\K \ar@/^8pt/[rr]^{\IncFun} \ar@{}[rr]|{\bot}  &&
\Cmd{\K} \ar@/^8pt/[ll]^{\EMFun} \ar@/_8pt/[rr]_{\EMAFun} \ar@{}[rr]|{\bot} &&
\Adj{\K} \ar@/_8pt/[ll]_{\CmdFun}}}
\end{equation}

where the 2-functor $\IncFun$ sends an object $A$ in to the identity comonad
A,A,A,A on $A$, and the 2-functor $\EMFun$
sends a comonad $\mathbb{c}=\ple{A,c,\cmu,\cun}$ to its Eilenberg-Moore object
A𝕔; while the 2-functor $\CmdFun$ sends an adjunction
$\adj=\ple{C,D,l,r,\unit,\counit}$ to the associated comonad D,lr,lr,,
and the 2-functor $\EMAFun$ sends a comonad $\mathbb{c}$ to the Eilenberg-Moore adjunction
between $A$ and A𝕔.

Although the terminology already suggests clearly the kind of generalization adopted, we
hasten to point out that in the 2-category Cat of (small) categories, functors and
natural transfomations, the definitions in (i) and (ii) instantiate exactly to the usual
notions of (standard) adjunction between categories $l\dashv r$—where $\eta$ and
$\epsilon$ are the unit and the counit of the adjunction—, and to comonads. Clearly,
Cat admits the Eilenberg-Moore construction for every comonad.

In the next sections we shall characterize adjunctions and comonads in the 2-category
of doctrines.

§ THE 2-CATEGORY OF DOCTRINES

The 2-category of doctrines
consists of the following data:

[objects] are doctrines, a functor $\fun{\Doc}{\C\op}{\Pos}$ from the opposite
of a category to the category of posets and monotone functions—in the
nomenclature of indexed categories, the category is named the base of the
doctrine, for $X$ an object in the poset $\Doc(X)$ is the fibre over $X$, and for
tXY an arrow in , the monotone function tYX is called
reindexing along $t$;[In the following, we may sometime refer to a doctrine
as a pair , in order to make the base of the doctrine conspicous.]
[a 1-arrow]
F,f from the doctrine  to the doctrine
is a pair where the first component $\fun{F}{\C}{\D}$ is a
functor and the second component $\TNat{f}{\Doc}{\aDoc F\op}$ is a natural transformation;
[a 2-arrow]
is a natural transformation $\TNat{\theta}{F}{F'}$ such that,
for each object $X$ in ,
$f_X\order_X(\DReIdx{\aDoc}{\theta\op})_X\circ f'_X$.
[Composition of 1-arrows]
G,g,, and
F,f,, is (essentially)
[Composition of 2-arrows]
θF,fF',f' and
ζF',f'F”,f” is the natural transformation
since, for any object $X$ in ,

\[f_X\order_X\DReIdx{\aDoc}{(\theta\op{}_X)}\circ f'_X
\order_X\DReIdx{\aDoc}{(\theta\op{}_X)}\circ\DReIdx{\aDoc}{(\zeta\op{}_X)}\circ f''_X
\order_X\DReIdx{\aDoc}{((\zeta\circ\theta)\op{}_X)}\circ f''_X.\]

There is an obvious forgetful 2-functor Cat to the 2-category of
categories, functors and natural transformations, which maps a doctrine , to
its base category , and acts similarly on the arrows.
Note that such a 2-functor is actually a 2-fibration, in the sense of [16],
where cartesian 1-arrows are “chang of base”, that is, arrows of the form F,𝕀,
while vertical 1-arrows “fibred”, that is, arrows of the form ,f, which act
only on the fibres.[Many notions in this paper can be phrased using the language
of 2-fibrations, but with the hope to keep the presentation more accessible, we shall just
highlight the connection in a few important cases.]

We define also the 2-category of doctrines endowed with operator as follows:

[objects] are pairs , where is a
doctrine and $\necmod$ is operator on ;
[a 1-arrow] from , to
,' is a 1-arrow
$\oneAr{\ple{F,f}}{\Doc}{\aDoc}$ in such that, for each
object $X$ in the base category of $\Doc$, we have
$f_X \circ\necmod_X\order\necmod'_{FX}\circ f_X$;
[a 2-arrow] from F,f to G,g is a 2-arrow
θF,fG,g in .
[Compositions] are inherited from those of the 2-category .

It is easy to verify that the requirement on the component $f$ of a 1-arrow in is
equivalent to the condition that $\necmod'_{FX}\circ f_X\circ\necmod_X=f_X\circ\necmod_X$,
$f_X$ maps elements to elements.

Consider the forgetful functor U, and for a
topological space X,τ let
u_X=𝕀XXX. If P, is as in
topol, then
U,uP,, is a 1-arrow
in .

For a Kripke frame $\KFr=\ple{W,R}$ where $R$ is reflexive and transitive, the pairs
W^(),_R∘ and [W],, introduced
in kripke, are objects of .

Consider the functor CW which maps a
set $S$ the pair S,(S)_w∈W where the second component is
the constant family of value $S$. Also, for $\alpha\in\pw{W}^S$,
consider the $W$-indexed family given by

\[\left(c_S(\alpha)\right)_w\colon=\set{s\in S}{w\in\alpha(s)}.\]

[W], is a 1-arrow in .

One can show that the 1-arrow C,cW^()[W] is the
comprehension completion of the doctrine W^(), and that
the operator is the canonical extension of the other operator
$\IntOp_R\circ\blank$, see [23, 30].

There is a forgetful 2-functor  which deletes the
operator. It has a right 2-adjoint,
which sends a doctrine  to
,𝕀 and is the identity both on 1-arrows and
Indeed, for any object , in the inequality
$\necmod_X\order\id{\Doc X}$ holds; so for
any 1-arrow $\oneAr{\ple{F,f}}{\Doc}{\aDoc}$ in we have
$f_X\circ\necmod_X\order f_X$ by monotonicity of $f_X$.

§ MODALITIES FROM ADJUNCTIONS

The main goal of this section is to connect operators as in
modality and adjunctions in .  First we characterise the general
2-categorical notion of adjunction, as introduced in background, for the
particular case of the 2-category in terms of the functors and natural
transformations involved.

An adjunction in the 2-category in the sense of
adjcom1 is completely determined by an octuple
,,,,,,,, where
and  are
doctrines,  and  are
functors, ,

are natural transformations such that

,,,,, is an adjunction in Cat;

, and
, are 1-arrows in ;

,() and
,𝕀 are 2-arrows in .

If P,Q,l,r,, is an adjunction in
, applying the forgetful functor Cat one
gets immediately <ref> where $L$ and $R$ are the
first components of $l$ and $r$ respectively. The rest of the proof is
plain bookkeeping.

As for any 2-category, one can consider the 2-category  of adjunctions
in . The following proposition is just as straightforward as the
previous one.

The 2-category  of adjunctions in has objects which are adjunctions
\RAdj^\adj,\RAdjLift^\adj,\unit^\adj,\counit^\adj}$
as in idxpos-adj, where ^(^) and

A 1-arrow
in  consists of two 1-arrows
F,f^^ and
and a 2-arrow
^G,(^G)g in such that the triple
F,G,θ is a homomorphism of adjunctions in Cat, and the two natural
transformations (g(^))λ^^^(G^) and
(λ^F)f^^(^F) coincide (note that
$G\LAdj^\adj=\LAdj^\aadj F$ by the first condition).

A 2-arrow
α,βF, f, G, g,θF',f',G',g',θ'
in  consists of two 2-arrows αF,fF',f' and
βG,gG',g' in such that
α,β is a 2-cell from the adjunction homomorphism F, G, θ to the
adjunction homomorphism F',G',θ' in Cat.

To elucidate the conditions in catadj in terms of some diagrams, consider first
that the forgetful 2-functor Cat extends to a 2-functor
Cat. Hence
the condition that the triple F,G,θ is a homomorphism of adjunctions in Cat
requires that the diagram of functors

\[\xymatrix{\C^\adj\ar[r]^-F\ar[d]_-{\LAdj^\adj}&\C^\aadj\ar[d]^-{\LAdj^\aadj}\\
\D^\adj\ar[r]^-G&\D^\aadj}\]

commutes as well as (either of) the diagrams of natural transformations

\[\xymatrix{F\arnta[d]_-{\unit^\aadj F}\arnta[r]^-{F\unit^\adj}&
\RAdj^\aadj\LAdj^\aadj F\ar@{2-2-}[r]&\RAdj^\aadj G\LAdj^\adj}\kern6em
\xymatrix{\LAdj^\aadj F\RAdj^\adj\ar@{2-2-}[d]\arnta[r]^-{\LAdj^\aadj\theta}&
\LAdj^\aadj\RAdj^\aadj G\arntb[d]^-{\counit^\aadj G}\\

as the two commutativity conditions are equivalent. For instance, if we assume the first
commutes, postcomposing it with $\LAdj^\aadj$ and precomposing it with $\RAdj^\adj$,
and using the naturality of $\theta$ and $\counit^\aadj$ and the triangular identities
of adjunctions, we get the second as depicted in the following diagram

\[\xymatrix<EMAIL_ADDRESS>\LAdj^\aadj F\RAdj^\adj\arntb[d]^-{\LAdj^\aadj\unit^\aadj F\RAdj^\adj}
\arnta[r]^-{\LAdj^\aadj F\unit^\adj\RAdj^\adj}
\ar@<-10pt>@/_25pt/[dd]|-*=0[@]{\lstb\tdot}_(.4){\id{}}
\ar@<5pt>@/^25pt/[rr]|-*=0[@]{\lsta\tdot}^(.4){\id{}}&
\LAdj^\aadj F\RAdj^\adj\LAdj^\adj\RAdj^\adj
\arntb[d]^-{\LAdj^\aadj\theta\LAdj^\adj\RAdj^\adj}
\arnta[r]^-{\LAdj^\aadj F\RAdj^\adj\counit^\adj}&
\LAdj^\aadj F\RAdj^\adj\arntb[d]^-{\LAdj^\aadj\theta}\\
\LAdj^\aadj\RAdj^\aadj\LAdj^\aadj F\RAdj^\adj\ar@{2-2-}[r]
\arntb[d]^-{\counit^\aadj\LAdj^\aadj F\RAdj^\adj}&
\LAdj^\aadj\RAdj^\aadj G\LAdj^\adj\RAdj^\adj
\arnta[r]^-{\LAdj^\aadj\RAdj^\aadj G\counit^\adj}&
\LAdj^\aadj\RAdj^\aadj G\arntb[d]^-{\counit^\aadj G}\\
\LAdj^\aadj F\RAdj^\adj\ar@{2-2-}[r]&
\LAdj^\aadj\RAdj^\aadj G}\]

The condition that the pair α,β is a 2-cell from the adjunction
homomorphism F,G,θ to the adjunction homomorphism F',G',θ' in
Cat translates into commutativity of the following diagrams of natural

\[\xymatrix{
\LAdj^\aadj F\arnta[r]^-{\LAdj^\aadj\alpha}\ar@{2-2-}[d]&\LAdj^\aadj F'\ar@{2-2-}[d]\\
\kern6em
\xymatrix{
\RAdj^\aadj G\arnta[r]^-{\RAdj^\aadj\beta}&\RAdj^\aadj G'}\]

From now on, when referring to an adjunction in the 2-category
, we shall take advantage of idxpos-adj and write
it as an octuple

Examples are many as any adjunction between categories with pullbacks gives rise to an
adjunction between the doctrines of subobjects. In details, given a category with
pullbacks , one can define a functor $\fun{\Sub[\C]{}}{\C\op}{\Pos}$
taking advantage of the fact that pulling back preserves monos. The
functor maps an object to the poset of its subobjects and reindexing
along fX'X is as follows:
a subobject $\xymatrix@1{[A\ \ar@<-.2ex>@{^(->}[r]^-{\alpha}&X]}$, determined
by the isomorphism class of the mono $\alpha$, is taken to the subobject
determined by the mono $\alpha'$ obtained as a pullback

\[\xymatrix{A'\ \ar[d]\ar@{^{(}->}[r]^-{\alpha'}
A\ \ar@{^{(}->}[r]_-{\alpha}&X.}\]

Let be also a category with pullbacks, and consider an
adjunction ,,,,, where
preserves pullbacks (as a right adjoint, the
functor R preserves all existing limits).
Between the doctrines $\fun{\Sub[\C]{}}{\C\op}{\Pos}$ and
there are 1-arrows of $\oneAr{\ple{\LAdj,\LAdjLift}}{\Sub[\C]{}}{\Sub[\D]{}}$
where for $X$ in and $Y$ in
\[\LAdjLift_X(\xymatrix@1{[A\ \ar@{^(->}[r]^-{\alpha}&X]})=
\xymatrix@1{[\LAdj A\ \ar@{^(->}[r]^-{\LAdj\alpha}& \LAdj X]}
\qquad
\RAdjLift_X(\xymatrix@1{[B\ \ar@{^(->}[r]^-{\beta}&Y]})=
\xymatrix@1{[\RAdj A\ \ar@{^(->}[r]^-{\RAdj\beta}& \RAdj Y].}\]

The naturality of $\LAdjLift$ and $\RAdjLift$ follows since reindexing
is given by pulling back, and $\LAdj$ and $\RAdj$ preserve pullbacks.
To see that
is an adjunction in there remains to check that
,() and
are 2-arrows of : in other words,
for any $\xymatrix@1{[A\ \ar@<-.2ex>@{^(->}[r]^-{\alpha}&X]}$ and
$\xymatrix@1{[B\ \ar@<-.2ex>@{^(->}[r]^-{\beta}&Y]}$, we have

\[[\alpha]\order\Sub[\C]{\unit_X}[\RAdj\LAdj(\alpha)]
\quad\mbox{and}\quad

But this follows from naturality of and together with the
reindexing pullbacks

\[\xymatrix@C=3em{A\ \ar@{^{(}->}@/^5pt/[drr]^{\alpha}
\ar@/_5pt/[ddr]_{\unit_A}\ar@{-->}[dr]\\
&P\ \ar[d]\ar<EMAIL_ADDRESS>&\RAdj\LAdj A\ \ar@{^{(}->}[r]_{\RAdj\LAdj(\alpha)}&\RAdj\LAdj X}
\qquad\xymatrix@C=3em{\LAdj\RAdj B\ \ar@{-->}[dr]
\ar@{^{(}->}@/^5pt/[drr]^{\LAdj\RAdj(\beta)}\ar@/_5pt/[ddr]_{\counit_B}&& \\
&P\ \ar[d]\ar<EMAIL_ADDRESS>\LAdj\RAdj Y\ar[d]^{\counit_Y}\\
&B\ \ar@{^{(}->}[r]_{\beta}&Y}\]

We now put to use the characterisation in idxpos-adj to construct operator starting from an adjunction of doctrines.
We begin the process performing the construction for a very specific type of adjunctions: adjunctions between vertical 1-arrows.

Let $\fun{\Doc}{\C\op}{\Pos}$ and $\fun{\aDoc}{\C\op}{\Pos}$ be
doctrines, and suppose the octuple
is an adjunction in . Then

* for each object $X$ in , the
following adjunction holds between the fibres

\[\xymatrix{\Doc X \ar@/^8pt/[rr]^{\LAdjLift_X}  \ar@{}[rr]|{\bot} &&
\ar@/^8pt/[ll]^{\RAdjLift_X} \aDoc X,}\quad X\in\C_0;\]

* $\necmod = \LAdjLift \cdot \RAdjLift$ is operator on $\aDoc$.

By idxpos-adj, the hypothesis ensures that
are 2-arrows in . From this, the conclusion follows directly.

Recall from [28] that a commutative quantale is a complete
lattice endowed with further structure
,,,, where ,, is a complete
lattice, ,, is a commutative monoid such that the operation
$\Ltensor$ distributes over sups:

\[x\Ltensor\left(\Lsup\kern-.8ex\strut_{i\in I}\,x_i\right)=
\Lsup\kern-.8ex\strut_{i\in I}(x\Ltensor x_i)\]

for elements $x$ and families $(x_i)_{i\in I}$ in $\Qtl$—note that this yields that
$\Ltensor$ is monotone in its two arguments.

$R_\Qtl = \{x\in\Qtl\mid x\order \Lunit\mbox{ and } x\order x\Ltensor x\} \subseteq \Qtl$.
It is easy to check that $\Lunit\in R_\Qtl$ and $R_\Qtl$ is closed with respect to
$\Ltensor$ and $\Lsup$. Hence R_,,,, is a commutative
quantale. Let $\fun{\iota}{R_\Qtl}{\Qtl}$ be the inclusion function which clearly
preserves sups. Its right adjoint $\fun{r}{\Qtl}{R_\Qtl}$ is determined as
$r(x) = \Lsup \{ y \in R_\Qtl \mid  y\order x\}$.

Consider the doctrine $\fun{\Qtl^{(\blank)}}{\Set\op}{\Pos}$ and
$\fun{R_\Qtl^{(\blank)}}{\Set\op}{\Pos}$ mapping a set $X$ to the sets of functions
$\Qtl^X$ and $R_\Qtl^X$, ordered pointwise, and acting on functions by precomposition.
And the 1-arrow
$\oneAr{\ple{\Id{},\iota\circ\blank}}{R_\Qtl^{(\blank)}}{\Qtl^{(\blank)}}$ has a right
adjoint given by
Hence, by adj-to-modality, there is operator ^()^() given by
$\Lbang_X \alpha = \iota\circ r\circ \alpha$,
for any set $X$ and $\alpha \in \Qtl^X$.

Recall that the doctrine $\Qtl^{(\blank)}$ carries a much richer structure induced
from that of the original quantale $\Qtl$:
for any set $X$, ^X,, _X,_X,_X is a commutative quantale with
the pointwise structure and,
for $\alpha,\beta\in \Qtl^X$, the operation $\alpha\Llimpl_X\beta\colon= \Lsup
\{\zeta\in\Qtl^X\mid \alpha\Ltensor_X\zeta\order_X \beta\}$ determines an adjoint pair
$\blank\Ltensor_X\alpha\dashv\alpha\Llimpl_X\blank$; for every $\gamma\in\Qtl^X$, one
has that
$\alpha\Ltensor_X\gamma\order_X\beta$ if and only if $\gamma\order_X \alpha\Llimpl_X\beta$.
Furthermore, the operator ^()^()
enjoys additional properties:
for any set $X$ and $\alpha,\beta\in\Qtl^X$, we have
$\Lbang_X \alpha \order_X \Lunit_X$ and
$\Lbang_X \alpha\order_X \Lbang_X\alpha \Ltensor_X\Lbang_X\alpha$, and
$\Lunit_X \order_X \Lbang_X \Lunit_X$ and
$\Lbang_X\alpha \Ltensor_X \Lbang_X \beta \order_X \Lbang_X (\alpha \Ltensor_X \beta)$.
Therefore, the indexed poset $\Qtl^{(\blank)}$ provides a model of first order
intuitionistic linear logic, where $\Lbang$ is the linear exponential modality.

Let  be a doctrine.
The propositional connectives are defined in terms of adjunctions
involving and another doctrine defined from it where the
adjoint functors between the base categories are the identity, see
[19], see also
[17, 24].
So adj-to-modality provides operators associated with each connectives.
Two interesting instances are the following:

* Consider the doctrine ^2, defined
by $\Doc^2X = \Doc X \times \Doc X$ and $\DReIdx{\Doc^2}{f} =
\DReIdx{\Doc}{f} \times \DReIdx{\Doc}{f}$. Note that there is a
,Δ^2 where
$\Delta_X=\ple{\id{\Doc X},\id{\Doc X}}$.
Conjunction on is determined by
a right adjoint to ,Δ in ,
that is the octuple
,Δ,,,𝕀C,𝕀C is
an adjunction between and $\Doc^2$.
Hence, by adj-to-modality, there is operator on $\Doc^2$ given by
for $\alpha,\beta\in\Doc X$.

* Assume further that has finite products and consider an
object $X$ in .
Consider the doctrine $\fun{\Doc^X}{\C\op}{\Pos}$, determined as
$\Doc^X(Y)=\Doc(Y\times X)$ and
There is a 1-arrow $\oneAr{\ple{\Id{\C},p^X}}{\Doc}{\Doc^X}$ where
$p^X_Y=\DReIdx{\Doc}{\pi_1}$ and π_1Y×XY is the
first projection.
A universal quantifier  $\Forall X.$ on $\Doc$ over $X$ is a
right adjoint to $\ple{\Id{\C},p^X}$ in , the octuple
,^X,, p^X,,
is an adjunction in .
Hence, by adj-to-modality, there is operator on $\Doc^X$ given as $\alpha\mapsto p^X(\Forall X.\alpha)$
for $\alpha\in\Doc^X(Y)=\Doc(Y\times X)$.

We did not consider the other cases of connectives because the
modality each of those induces is the identity as the next proposition
explains in a more general context.

Let $\fun{\Doc}{\C\op}{\Pos}$ and $\fun{\aDoc}{\C\op}{\Pos}$ be
doctrines on the same base category. Suppose
𝕀,𝕀 is an adjunction.
Then, for each object $X$ in , the following hold:

*  $\LAdjLift_X \cdot \RAdjLift_X
\cdot \LAdjLift_X = \LAdjLift_X$ and $\RAdjLift_X \cdot \LAdjLift_X
\cdot \RAdjLift_X = \RAdjLift_X$;

*  $\LAdjLift_X \cdot \RAdjLift_X =
\id{\aDoc X}$ if and only if $\RAdjLift_X$ is injective if and only
if $\LAdjLift_X$ is surjective;

*  $\RAdjLift_X \cdot \LAdjLift_X =
\id{\Doc X}$  if and only if $\LAdjLift_X$ is injective if and only
if $\RAdjLift_X$ is surjective.

(i) is immediate since the adjunction $\LAdjLift_X\dashv\RAdjLift_X$
involves posetal categories. (ii) and (iii) follow directly from (i).

The next step is an application of a remarkable result by [15] about
fibred adjunctions as it allows to show that any adjunction in can be factored
as the composition of two adjunctions where one is the identity adjunction on the base
For this, recall that $\IdxPos$ has a vertical/cartesian factorisation
system, that is, any 1-arrow $\oneAr{\ple{F,f}}{\Doc}{\aDoc}$ from the
doctrine $\fun{\Doc}{\C\op}{\Pos}$ to the doctrine $\fun{\aDoc}{\D\op}{\Pos}$ can be
factored by “change of base”as $\ple{F,\id{\aDoc F\op}}  \circ \ple{\Id{\C},f}$

\[\xymatrix@C=6em@R=5ex{\C\op\ar@/^/[rd]^(.4)\Doc_(.7){}="f"
\ar[d]_{\Id{\C}\op}\\
\C\op\ar[r]^(.35){\aDoc F\op}^(.6){}="g"_(.6){}="k"
\ar[d]_{F\op}&\Pos\\
\D\op\ar@/_/[ru]_(.4){\aDoc}^(.7){}="h"
\ar"k";"h"_{\id{}}|{\smash{\tdot}}}\]

The factorization of the adjunction follows this decomposition for the left adjoint.
Recall Lemma 3.2 from [15] in the case of doctrines.

Let ,,,,, be an adjunction in Cat. If
is a doctrine, then there is an adjunction
,,,𝕀,,,, in as
depicted in the diagram

<EMAIL_ADDRESS>\aDoc\LAdj\op\ar@/^8pt/[rr]^{\ple{\LAdj,\id{}}}\ar@{}[rr]&&
\aDoc.\ar@/^8pt/[ll]^{\ple{\RAdj,\aDoc\counit\op}}}
\end{equation}

We apply idxpos-adj to show
\aDoc\counit\op,\unit,\counit}$ is an adjunction in .
Since ,,,,, is already an adjunction in
Cat, it remains to check the natural transformations

determine 2-arrows in as follows

\[\begin{array}{l@{\kern2em}l}
\twoAr{\unit}{\ple{\Id{\C},\id{\aDoc\LAdj\op}}}
\twoAr{\counit}{\ple{\LAdj\RAdj,\aDoc\counit\op}}
\end{array}\]

In other words, the inequalities

\[\id{\aDoc\LAdj X}\order
\DReIdx{\aDoc\LAdj}{\unit_X}\circ\DReIdx{\aDoc}{\counit_{\LAdj X}}\qquad
\DReIdx{\aDoc}{\counit_Y}\order\DReIdx{\aDoc}{\counit_Y}\]

hold for each object $X$ in and $Y$ in $\D$.
They are in fact identities: the second is immediate, and the first follows
from the triangular identity (<ref>) for an adjunction

\begin{equation}\label{tadj}
\DReIdx{\aDoc\LAdj}{\unit_X}\circ\DReIdx{\aDoc}{\counit_{\LAdj X}}=
\DReIdx{\aDoc}{(\counit_{\LAdj X}\circ\LAdj\unit_X)}=
\DReIdx{\aDoc}{\id{\LAdj X}} = \id{\aDoc\LAdj X}
\end{equation}

by functoriality of $Q$.

Theorem 3.4 in [15] restricted to the case of doctrines is the

Let  and  be
doctrines, and suppose the octuple
,,,,,,, is an
adjunction in . Then that adjunction factors through the adjunction
in $(\ref{equfx})$ as

<EMAIL_ADDRESS>\Doc\ar@/^8pt/[rr]^{\ple{\Id{\C},\LAdjLift}}\ar@{}[rr]&&
\aDoc\LAdj\op\ar@/^8pt/[ll]^{\ple{\Id{\C},(\Doc\unit\op)(\RAdjLift\LAdj\op)}}
\ar@/^8pt/[rr]^{\ple{\LAdj,\id{}}}\ar@{}[rr]&&
\aDoc.\ar@/^8pt/[ll]^{\ple{\RAdj,\aDoc\counit\op}}}
\end{equation}

where the first one is ,,,,,

We see the ,,,,,
is an adjunction in as another application of idxpos-adj.
Obviously ,,,,𝕀,𝕀 is the identity adjunction
in Cat. To check the natural transformation
determines 2-arrows in
\[\begin{array}{l@{\quad\mbox{and}\quad}l}
\twoAr{\id{\Id{\C}}}{\ple{\Id{\C},\id{\Doc}}}
\twoAr{\id{\Id{\C}}}
\end{array}\]

we must see that the inequalities

\[\id{\Doc X}\order
\DReIdx{\Doc}{\unit_X}\circ\RAdjLift_{\LAdj X}\circ\LAdjLift_X\quad\mbox{and}\quad
\LAdjLift_X\circ\DReIdx{\Doc}{\unit_X}\circ\RAdjLift_{\LAdj X}
\order\id{\aDoc\LAdj X}\]

hold for each object $X$ in .
The first inequality holds since
is a 2-arrow in .
For the second inequality, note that
$\LAdjLift_X\circ\DReIdx{\Doc}{\unit_X}\circ\RAdjLift_{\LAdj X}=
\DReIdx{\aDoc}{\LAdj\unit_X}\circ\LAdjLift_{\RAdj\LAdj X}\circ
\RAdjLift_{\LAdj X}$ since .
Since ,()
,𝕀 is a 2-arrow in , we have that
$\LAdjLift_{\RAdj\LAdj X}\circ\RAdjLift_{\LAdj X}\order
\DReIdx{\aDoc}{\counit_{\LAdj X}}$. Now the result follows from (<ref>).

To see that the composition of the two adjunctions gives the
original adjunction, note that the
top and bottom compositions in (<ref>)
give the top and bottom 1-arrow in

<EMAIL_ADDRESS>\Doc\ar@/^6pt/[r]^{\ple{\LAdj,\LAdjLift}}&
\aDoc.\ar@/^6pt/[l]^{\ple{\RAdj,\RAdjLift}}}\]

It is immediate to see that
\ple{\LAdj,\LAdjLift}$. For the other composition, the first
components coincide trivially, and for the second components
apply the commutativity of the following diagram of natural

\[\xymatrix@=5.5em{\aDoc\ar@/^10pt/[rr]^-{\RAdjLift}
\ar[d]^-{\aDoc\counit\op}\ar[r]_-{\RAdjLift}&
\Doc\RAdj\op\ar[d]_-{\Doc\RAdj\op\counit\op}
\ar[r]_-{P((\RAdj\counit)(\unit\RAdj))\op}&
\Doc\RAdj\op\\
\aDoc\LAdj\op\RAdj\op\ar[r]^-{\RAdjLift\LAdj\op\RAdj\op}&
\Doc\RAdj\op\LAdj\op\RAdj\op\ar[ru]_-{\Doc\unit\op\RAdj\op}}\]

where the square commutes by naturality of , the right-hand
triangle by functoriality of , and the top triangle by one of the
triangular identities for adjunctions (<ref>). Finally one sees
immediately the compositions of the 2-arrows give the 2-arrows of the
original adjunction.

Let  and  be
doctrines, and suppose the octuple
,,,,,,, is an
adjunction in . Then
$\necmod=\LAdjLift\cdot(\Doc\unit\op)\cdot(\RAdjLift\LAdj\op)$ is operator on
the doctrine .

It follows immediately applying adj-to-modality to the
first adjunction in (<ref>).

Let and be category with pullbacks, and let
,,,,, be an adjunction where
preserves pullbacks. As in pb-cat, there
is an adjunction
,,, on the doctrines of subobjects.
By adj-to-modality, there is operator on
the doctrine [],
defined as $\necmod_X\alpha=\LAdj\alpha'$,
where $X \in \C_0$ and $\alpha \in \Sub[\D]{\LAdj X}$ and
$\alpha'\in\Sub[\C]{X}$ is defined by the following pullback diagram

\[\xymatrix@C=3em{P\ \ar[d]\ar@{^{(}->}[r]^{\alpha'}
<EMAIL_ADDRESS>X \ar[d]^{\unit_X}\\
\RAdj A\ \ar@{^{(}->}[r]_{\RAdj \alpha}&\RAdj\LAdj X}\]

The construction is reminiscent of that of a
modal operator from a geometric morphism between elementary toposes,
see the original paper [14], or Section 10.1 in
[9], and also [27, 3, 2].
Indeed, a geometric morphism from the topos to the topos
is an adjunction
,,,,, such that the left
adjoint $\LAdj$ preserves finite limits.

The paradigmatic example of a operator obtained from a geometric morphism is that
offered by presheaves over a category . Recall that the category of presheaves over is the functor category . If we let $\C_0$ be the discrete category of the objects
of and write i_0 the inclusion functor, post-composition with it determines
a functor =∘i_0 which preserves all limits
and colimits as these are computed pointwise—although $\C_0=\C_0\op$ we maintain the
redundant notation $\C_0\op$ just for mental hygiene. Since the functor category
is complete and has a generating set, has a right adjoint
_0. Hence, $\LAdj\dashv\RAdj$ is a geometric morphism, thus
it induces an operator on

\[\xymatrix{\Psh{\C}\op\ar[rr]^{\Sub[\Psh{\C_0}]{}\LAdj\op}\ar[rd]_{\LAdj\op}&&\Pos\\

Finally, note that, if $\KFr = \ple{W,R}$  is a Kripke frame with $R$ reflexive and
transitive, taking $\C = \KFr\op$, the above geometric morphism provides another way to
construct Kripke models categorically.
In detail, a presheaf $D$ over $\KFr\op$ specifies, for each world $w\in W$, a set $D(w)$,
modelling individuals which exist at the world $w$,
and, for each $wRv$, a function D_wvD_wD_v, describing how individuals
existing at the world $w$ “evolve” in the world $v$.
A “formula” $\alpha$ on $D$ is a family of subsets, that is, for each world $w\in W$, $\alpha_w\subseteq D_w$, and
the modal operator identifies those formulas which are subpresheaves of $D$, namely, those $\alpha$ such that, for all $w,v\in W$, if $wRv$ then $\alpha_w \subseteq D_{wv}^{-1}(\alpha_v)$.

We conclude this section showing that the construction in adj-to-modality
extends to a 2-functor .

For an adjunction in write

\[\necmod^\adj\colon=
\LAdjLift^\adj\cdot(\Doc^\adj(\unit^\adj)\op)\cdot(\RAdjLift^\adj(\LAdj^\adj)\op)\]

which is operator by adj-to-modality. Let
For a 1-arrow F,f,G,g,θ, let

\begin{equation}\label{ontf}
\AMFun(\ple{F,f,G,g,\theta})\colon=\ple{F,g(\LAdj^\adj)\op}.
\end{equation}

For a 2-arrow

\begin{equation}\label{twtf}
\AMFun(\ple{\alpha,\beta})\colon=\alpha.
\end{equation}

With the assignments above,  is a 2-functor.

We just have to check that the identities in (<ref>) and (<ref>) determine
arrows in , as the algebraic identities will then follow immediately.
$\TNat{g(\LAdj^\adj)\op}{\aDoc^\adj(\LAdj^\adj)\op}{\aDoc^\aadj (G\LAdj^\adj)\op}$
and $G\LAdj^\adj=\LAdj^\aadj F$ by catadj, in order to see that

\[\oneAr{\ple{F,g(\LAdj^\adj)\op}}

ia a 1-arrow in we are left to check that
for every object $X$ in the base category of $\aDoc(\LAdj^\adj)\op$, we have

\[g_{\LAdj^\adj X}\cdot\necmod^\adj_X\order\necmod^\aadj_{FX}\cdot g_{\LAdj^\adj X}.\]

In the diagram of natural transformations

\[\xymatrix<EMAIL_ADDRESS>\aDoc^\adj(\LAdj^\adj)\op\arnta[r]^-{\RAdjLift^\adj(\LAdj^\adj)\op}
\arntb[dddddd]^-{g(\LAdj^\adj)\op}&
\Doc^\adj(\RAdj^\adj\LAdj^\adj)\op\arnta[r]^-{\Doc^\adj(\unit^\adj)\op}
\arnta[ddd]_{f(\RAdj^\adj\LAdj^\adj)\op}\ar@{{}{}}[rddd]|{*}&
\Doc^\adj\arnta[r]^-{\LAdjLift^\adj\ }\arnta[ddd]_-{f}&
\aDoc^\adj(\LAdj^\adj)\op\arnta[dd]^-{g(\LAdj^\adj)\op}\\&&& \\
\Doc^\aadj(F\RAdj^\adj\LAdj^\adj)\op\arnta[r]^-{\Doc^\aadj(F\unit^\adj)\op}&
\Doc^\aadj F\op\arnta[r]^-{\kern1.3ex\LAdjLift^\aadj F\op}&
\Doc^\aadj(\LAdj^\aadj F)\op\ar@{2-2-}[u]\\ \\ \\
\aDoc^\aadj(\LAdj^\adj)\op\arnta[r]^-{\Doc^\aadj\theta(\LAdj^\adj)\op}
\arnta[rddd]_-{\RAdjLift^\aadj(\LAdj^\aadj F)\op}
\ar@{{}{}}[ruuuuuu]|(.3)*=0[@]{\geq}&
\Doc^\aadj(\RAdj^\aadj G\LAdj^\adj)\op\arntb[uuu]^-{\Doc^\aadj(\theta\LAdj^\adj)\op}
\arnta[uuur]^-{\Doc^\aadj(\theta\LAdj^\adj\cdot F\unit^\adj)\op}\\ \\ \\
&\Doc^\aadj(\RAdj^\aadj\LAdj^\aadj F)\op\arnta[uuuuuur]_-{\Doc^\aadj(\unit^\aadj F)\op}

the marked square commutes by naturality of $f$, the triangle by functoriality of
$\Doc^\aadj$, and all the other paths commutes (possibly up to inequality as shown) by

Given now a 2-arrow
$\twoAr{\ple{\alpha,\beta}}{\ple{F,f,G,g,\theta}}{\ple{F',f',G',g',\theta'}}$ in
to see that
$\twoAr{\alpha}{\ple{F,g\LAdj^\adj}}{\ple{F',g'\LAdj^\adj}}$ is a
2-arrow in , we have to show that, for every object $X$ in the base category
of $\aDoc(\LAdj^\adj)\op$, it is the case that
$g_{\LAdj^\adj X}\order\DReIdx{\aDoc'}{\LAdj^\aadj\alpha_X}\cdot g'_{\LAdj^\adj X}$.
By catadj, the equality $\LAdj^\aadj\alpha=\beta\LAdj^\adj$ holds  and,
since βG,gG',g' in , we obtain that
$g_{\LAdj^\adj X}\order\DReIdx{\aDoc'}{\beta_{\LAdj^\adj X}}\cdot g'_{\LAdj^\adj X}$, as needed.

A particular example of operators is found in the categorical semantics of the
linear exponential modality (a.k.a. bang modality) of propositional linear logic provided by
linear-nonlinear adjunctions.
A linear-nonlinear adjunction is a monoidal adjunction between a symmetric monoidal
category and a cartesian category; the induced comonad on the symmetric monoidal
category interprets the bang modality, see [6].
The categorical notion swiftly extends to doctrines where the construction in
adj-to-modality provides a model of the bang modality in a higher order setting.
The role of the cartesian category is played by a
primary doctrine, see [11]), that is, a doctrine
where has finite products and, for each object $X$ in , the
fiber $\Doc X$ carries an inf-semilattice structure preserved by reindexing.
The role of the symmetric monoidal category is played by a
$($symmetric$)$ monoidal doctrine, which one defines following the work on
monoidal indexed categories of [25]. We give some of the details in
Appendix <ref>, but shall develop fully the particular instance of operators in a subsequent paper.

§ MODALITIES FROM COMONADS

As is well-known, there is a deep connection between comonads and adjunctions in a
2-category: every adjunction determines a comonad.  Viceversa, when the 2-category admits
the Eilenberg-Moore construction for comonads, a comonad generates an adjunction. This
connection is particularly interesting when we consider a left exact comonad on a
topos : the category of coalgebras  is a topos and the
Eilenberg-Moore adjunction between  and is a geometric
morphism, see [21].
As we have seen in presh, geometric morphisms generate operators; hence, combining these two facts, we obtain that a left exact comonads on an
elementary topos determines operator.

In this section, we study the relationship between adjunctions and comonads in the
2-category of doctrines, showing how comonads generate adjunctions, as
expected, and operators from those. We start by determining comonads in

Let  be a doctrine.
A comonad on is completely determined by a quadruple
$\cmd=\ple{\cmdfun,\cmdlift,\comul,\cun}$ where

* ,, is a comonad on ;

, is a 1-arrow in ;

and ,,𝕀 are 2-arrows in .

More explicitly, comonad2 requires that

and comonad3 states that, for each object $X$ in
, the following inequalities hold

\[\cmdlift_X\order\DReIdx{\Doc}{\comul_X}\circ \cmdlift_{\cmdfun X}\circ \cmdlift_X
\qquad\mbox{ and }\qquad
\cmdlift_X\order\DReIdx{\Doc}{\cun_X}.\]

For abstract reasons, a comonad in always admits the Eilenberg-Moore construction,
see [8]. Here we limit ourselves to present the
direct computation of the Eilenberg-Moore object for a comonad
$\cmd=\ple{\cmdfun,\cmdlift,\comul,\cun}$ on the doctrine
The Eilenbeerg-Moore object for can be given on the doctrine
() defined as follows.

The category $\EM{\C}{\cmdfun}$ is the category of coalgebras for the comonad
$\ple{\cmdfun,\comul,\cun}$ on , namely,
objects are pairs $\ple{C,c}$ where $C$ is an object in and $\oneAr{c}{C}{\cmdfun C}$
is an arrow in such that the diagram

\[\xymatrix{&C\ar[d]^-{c}\ar[ld]_{\id{C}}\ar[r]^-{c}&\cmdfun C\ar[d]^{\comul_C}\\
C&\cmdfun C\ar[l]^{\cun_C}\ar[r]_{\cmdfun c}&\cmdfun\cmdfun C}\]

commutes, and an arrow fC,cC',c' is an arrow fCC' in ,
such that

\[\xymatrix{C\ar[d]_-{c}\ar[r]^-{f}&C'\ar[d]^{c'}\\
\cmdfun C\ar[r]^{\cmdfun f}&\cmdfun C'.}\]

With the intention to produce the doctrine
for each coalgebra C,c let C,c be the suborder of
$\Doc C$ on the subset

Given an arrow fC,cC',c' in  and
$\beta\in\EM{\Doc}{\cmd}\ple{C',c'}$, note that
$\beta\order\DReIdx{\Doc}{c'}(\cmdlift_{C'}(\beta))$ by definition of
C',c'. Thus

\[\begin{array}{r@{}l}\DReIdx{\Doc}{f}(\beta)\order
\DReIdx{\Doc}{f}(\DReIdx{\Doc}{c'}(\cmdlift_{C'}(\beta))){}&{}
&{}=\DReIdx{\Doc}{c}(\DReIdx{\Doc}{\cmdfun (f)}(\cmdlift_{C'}(\beta)))
\end{array}\]

So f sends elements of C',c' to elements of C,c: let
f be the restriction of f. It follows immediately
that  is a doctrine.

Note that the inequality $\DReIdx{\Doc}{c}(\cmdlift_C(\alpha)) \order \alpha$ holds
for every $\alpha \in \Doc C$, by properties of $c$ and $\cun_C$.
Hence the elements of $\EM{\Doc}{\cmd}\ple{C,c}$ are the fixpoints of
Furthermore, as we shall see, $\DReIdx{\Doc}{c}\circ\cmdlift_C$ is an idempotent on
$\Doc C$ (it is a consequence of cmd-to-modality).
Thus, as in idempotents split, one gets $\EM{\Doc}{\cmd}\ple{C,c}$ by splitting

Next we introduce the forgetful 1-arrow
, as follows:
the functor $\fun{\Forget}{\EM{\C}{\cmdfun}}{\C}$ is the actual forgetful functor
from the category of coalgebras; the natural transformation
() is given by the inclusion of
$\EM{\Doc}{\cmd}\ple{C,c}$ into $\Doc C$ as C,c varies among the objects of
It is immediate to see the functor $\Forget$ is faithful and, for each object C,c in
$\EM{\C}{\cmdfun}$, the map $\ForgetLift_{\ple{C,c}}$ is injective.

Finally the universal 2-arrow
,, as requested in
(<ref>) is given by the family $\unita$ given by

\[\unita_{\ple{C,c}}\colon=\fun{c}{C}{\cmdfun C},\quad
\mbox{ as }\ple{C,c}\mbox{ varies among the objects in }\EM{\C}{\cmdfun}.\]

One sees immediately that . It determines an
appropriate 2-arrow
in because for any $\alpha\in\EM{\Doc}{\cmd}\ple{C,c}$, by definition of
C,c one has that

\[\alpha\order\DReIdx{\Doc}{c}(\cmdlift_C(\alpha))
=\left(\DReIdx{\Doc}{\unita_{\ple{C,c}}} \circ \cmdlift\big(\Forget\big)\op_{\ple{C,c}}\right)(\alpha)\]

After introducing the dramatis personæ, we are ready to prove the characterization
of the Eilenberg-Moore construction for a comonad in .

Let $\fun{\Doc}{\C\op}{\Pos}$ be a doctrine and $\cmd$ a comonad on $\Doc$.

\[\xymatrix@C=5em@R=1em{&\Doc\ar[dd]^-{\ple{\cmdfun,\cmdlift}}_(.6){}="a"\\
\EM{\Doc}{\cmd}\ar[ru]^{\ple{\Forget,\ForgetLift}}
\ar[rd]_-{\ple{\Forget,\ForgetLift}}^{}="b"\\
\ar@{=>}"b";"a"^-{\unita}&\Doc}\]

is the Eilenberg-Moore construction for $\cmd$ in .

We begin the proof analysing the data for the 2-problem in adjcom3: one
has an arbitrary doctrine  and a diagram of 1-arrows and
2-arrows in
\begin{equation}\label{fcc}
\vcenter{\xymatrix@C=5em@R=1em{&\Doc\ar[dd]^-{\ple{\cmdfun,\cmdlift}}_(.6){}="a"\\
\aDoc\ar[ru]^{\ple{X,x}}
\ar[rd]_-{\ple{X,x}}^{}="b"\\
\ar@{=>}"b";"a"^-{\xi}&\Doc}}
\end{equation}

where the pair X,x,ξ satisfies the two commutativity conditions in
(<ref>). These translate precisely in the commutative diagrams of natural

\begin{equation}\label{transl1}
\vcenter{\xymatrix{X\arnta[r]^-{\xi}\arnta[d]_-{\xi}&
\cmdfun X\arntb[d]^-{\comul X}\\
\cmdfun X\arnta[r]_-{\cmdfun\xi}&\cmdfun\cmdfun X}}\qquad
\vcenter{\xymatrix{X\arnta[r]^-{\xi}\arnta[rd]_-{\id{X}}&
\cmdfun X\arntb[d]^-{\cun X}\\&X}}
\end{equation}

while the condition on the 2-arrow in (<ref>) requires that the natural transformation
ξXX is such that, for every object $D$ in and $\beta\in \aDoc(D)$, we have

\begin{equation}\label{transl2}
x_D(\beta)\order \DReIdx{\Doc}{(\xi_D)}(\cmdlift_{X(D)}(x_D(\beta))).
\end{equation}

In turn, the commutativity of the two diagrams (<ref>) is equivalent to requiring
that, for every object $D$ in , there is a structure of coalgebra X(D),ξ_D for the
comonad ,, on the object $X(D)$ in the category , and that, for every
arrow fDD' in , the arrow X(f)X(D),ξ_DX(D'),ξ_D' is
a homomorphism of coalgebras. At the same
time, condition (<ref>) is equivalent to requiring that the monotone function
x_D(X(D))(X(D)) factors through

\[\xymatrix@R=.8ex@C=2em{\aDoc(X(D))\ar[rrd]_-{x_D}\ar[rrr]^-{x_D}&&&\Doc(X(D))\\

Hence the data for the 2-problem determine precisely a
1-arrow X,ξ,xQ ensuring uniqueness,
and it is immediate to check that the required diagram commutes.

Similarly, for an arrow γX,x,ξY,y,υ of the 2-problem, that is, a 2-arrow γX,xY,y in , the commutative
diagram (<ref>) determines precisely a natural transformation
γX,ξY,υ; the
inequality encoded in the 2-arrow γX,xY,y in is the
same as that encoded in the 2-arrow
Y,υ,y in .

Let  be a doctrine and $\cmd=\ple{\cmdfun,\cmdlift,\comul,\cun}$ be
a comonad on $\Doc$. Then there is an adjunction
\ple{\EM{\Doc}{\cmd},\Doc,\Forget,\ForgetLift,\hat{\cmdfun},\cmdlift,\unit^\cmd,\cun}$
between  and .

It follows from em-obj and general results in [29]. But we make
explicit each component of the adjunction as is obtained from the general case.
Among the data determining the adjunction, only two may need to be described:
the functor  is the free coalgebra functor and
gives, for an object $X$ in , the free coalgebra
$\hat{\cmdfun}X=\ple{\cmdfun X,\comul_X}$. The natural transformation is the canonical
embedding of a coalgebra into the free coalgebra
^ defined as

In fact, in the general 2-adjunction between comonads and adjunctions in a 2-category when admits the Eilenberg-Moore construction, as in diagram (<ref>), we know that
the Eilenberg-Moore construction gives the right 2-adjoint from the 2-category  of
comonads in .
So we briefly collect the
data for the 2-category  in order to apply that result in the present
situation. The 2-category  has

[objects] which are pairs , where is a doctrine and is a
comonad on ;
[1-arrows] from , to ,, with
$\cmd=\ple{\cmdfun,\cmdlift,\comul^\cmd,\cun^\cmd}$ and
$\acmd=\ple{\acmdfun,\acmdlift,\comul^\acmd,\cun^\acmd}$, consist of a 1-arrow
F,f and a 2-arrow
in such that the following diagrams of functors and natural transformations commute:

\[\xymatrix{
F\cmdfun \ar[r]^{\theta} \ar[dr]_{F\cun^\cmd} & \acmdfun F \ar[d]^{\cun^\acmd F} \\
& F
\xymatrix{
F \cmdfun \ar[d]_{F\comul^\cmd} \ar[rr]^{\theta} && \acmdfun F \ar[d]^{\comul^\acmd F} \\
F \cmdfun^2 \ar[r]_{\theta \cmdfun} & \acmdfun F \cmdfun \ar[r]_{\acmdfun \theta} & \acmdfun^2 F

[2-arrows] from F,f,θ to G,g,ζ, which are 1-arrows
from , to ,, with
$\cmd=\ple{\cmdfun,\cmdlift,\comul^\cmd,\cun^\cmd}$ and
$\acmd=\ple{\acmdfun,\acmdlift,\comul^\acmd,\cun^\acmd}$, consist of a 2-arrow
αF,fG,g such that the following diagram of functors and
natural transformations commutes

\[ \xymatrix{
F\cmdfun \ar[r]^{\alpha \cmdfun} \ar[d]_{\theta} & G\cmdfun \ar[d]^{\zeta} \\
\acmdfun F \ar[r]_{\acmdfun \alpha} & \acmdfun G
} \]

The instance of diagram (<ref>) which we have been addressing is the

\[ \xymatrix{
\IdxPos \ar@/^8pt/[rr]^{\IncFun} \ar@{}[rr]|{\bot}  &&
\Cmd{\IdxPos} \ar@/^8pt/[ll]^{\EMFun} \ar@/_8pt/[rr]_{\EMAFun} \ar@{}[rr]|{\bot} &&
\Adj{\IdxPos} \ar@/_8pt/[ll]_{\CmdFun}
} \]

Since by adj-to-modality every adjunction between doctrines induces operator, via one obtains operator also from a comonad.

Let $\fun{\Doc}{\C\op}{\Pos}$ be a doctrine and $\cmd=\ple{\cmdfun,\cmdlift,\comul,\cun}$
a comonad on $\Doc$. Then, the natural transformation
defined, for
each coalgebra X,c in $\EM{\C}{\cmdfun}$, by
is operator on .

By cmd-to-adj, ,,,,^,
is an adjunction between  and .
By adj-to-modality, $\necmod^\cmd= \ForgetLift \cdot (\EM{\Doc}{\cmd}\unit^\cmd)
\cdot (\cmdlift\Forget)$ is operator on
but, for each coalgebra X,c in $\EM{\C}{\cmdfun}$, $\unit^\cmd_{\ple{X,c}} = c$ and
$\Forget\ple{X,c} = X$, $\DReIdx{\EM{\Doc}{\cmd}}{c} = \DReIdx{\Doc}{c}$ by definition, and
$\ForgetLift$ is an inclusion.

An interesting case of cmd-to-modality is that of toposes of presheaves as
models of first order modal logic.
We have already seen in presh how one obtains operator

\[\xymatrix{\Psh{\C}\op\ar[rr]^{\Sub[\Psh{\C_0}]{}\LAdj\op}\ar[rd]_{\LAdj\op}&&\Pos\\

on the category of presheaves  from the adjunction which is the geometric morphism

\begin{equation}\label{geomor}
\xymatrix@=4em{\Psh{\C_0}\ar@<.5ex>@/^/[r]^{\RAdj}\ar@{{}{}}[r]|-{\top}
&\Psh{\C}\ar@<.5ex>@/^/[l]^{\blank\circ i\op}}
\end{equation}

where $\C_0$ denotes the discrete category of the objects of and i_0 is
the inclusion functor. But the category of presheaves is exactly the category of
coalgebras for the comonad determined by the adjunction (<ref>), see
[18]; so cmd-to-modality applies, and the modal
operator obtained on a presheaf model is obtained directly from the subobject doctrine on
_0] and the geometric morphism that determines the presheaves as coalgebras.

§ THE GLOBAL PICTURE

2-fun-adj-modality produces a construction of operator from
adjunctions as a 2-functor $\fun{\AMFun}{\Adj{\IdxPos}}{\NecIdxPos}$. And
cmd-to-modality describes the action of the composition in the diagram

\[\xymatrix@=5em{\Cmd{\IdxPos}\ar@<-.5ex>@/_/[r]_-{\EMAFun}\ar@{{}{}}[r]|-{\bot}
\ar[rd]_-{\CMFun}

The goal of this section is to complete the above diagram, by showing that $\AMFun$ is
part of a local adjunction, see [7]. Hence so is $\CMFun$.

We start by comparing the 2-functor to the composite $\CMFun \circ \CmdFun$, both constructing a doctrine with interior operator from an adjunction in .
They do not coincide, but can be canonically compared by a 2-natural transformation.
Recall that maps a comonad ,, for
to the doctrine with operator (),^ where

Since is a 2-functor, its action on the unit of the 2-adjunction $\CmdFun\dashv\EMAFun$
produces a natural comparison $\AMFun(\adj)\to\CMFun(\CmdFun(\adj))$ for
an adjunction in .

Indeed, let $\cmd\colon=\CmdFun(\adj) =
\ple{\LAdj\RAdj,(\LAdjLift\RAdj\op)\RAdjLift,\LAdj\unit\RAdj,\counit}$ be the induced
comonad on $\aDoc$. The component of the unit of the 2-adjunction on $\adj$ is given
by the 1-arrow K,k,,𝕀,𝕀(), where
K,k is the comparison 1-arrow given by the
Eilenberg-Moore construction. The 1-arrow  K,k is obtained by the universal property
of $\EM{\aDoc}{\cmd}$ applied to the following diagram:

\[\vcenter{\xymatrix@C=4em@R=1ex{
\Doc\ar[ru]^-{\ple{\LAdj,\LAdjLift}}\ar[rd]_-{\ple{\LAdj,\LAdjLift}}^(.68){}="s"\\
\ar@{=>}"s";"t"^-{\LAdj\unit}&\aDoc}}\]

More explicitly,  K,k is defined as follows:
$KX \colon= \ple{\LAdj X,\LAdj\unit_X}$, for each object $X$ in the base category of $\Doc$,
$Kf \colon= \LAdj f$, for each arrow in the base category of $\Doc$, and $k = \LAdjLift$.
This is well-defined thanks to the following chain of inequalities:

\[\LAdjLift_X\order\LAdjLift_X\circ\DReIdx{\Doc}{\unit_X}\circ\RAdjLift_{\LAdj X}\circ\LAdjLift_X
((\LAdjLift\RAdj\op)\cdot\RAdjLift)_{\LAdj X}\circ\LAdjLift_X.\]

Let $\adj=\ple{\Doc,\aDoc,\LAdj,\LAdjLift,\RAdj,\RAdjLift,\unit,\counit}$ be an adjunction
in , and consider
the associated comonad on the doctrine $\aDoc$.
Let $\ple{K,k}$ be the comparison 1-arrow.
is a 1-arrow in and $\necmod^\adj=\necmod^\cmd K$.

It is immediate since, for each object $X$,
$\necmod^\adj_X = \LAdjLift_X \DReIdx{\Doc}{\unit_X} \RAdjLift_{\LAdj X} =
\DReIdx{\aDoc\LAdj}{\unit_X} \LAdjLift_{\RAdj\LAdj X} \RAdjLift_{\LAdj X} =
\necmod^\cmd_{K X}$.

Finally, let us note that this comparison 1-arrow is a component of a 2-natural
transformation, obtained by postcomposition of the unit of the 2-adjunction
$\CmdFun\dashv\EMAFun$ with the 2-functor $\AMFun$.

In order to show that is part of a local adjunction,
We start by constructing a comonad from an object , in .

Let $\fun{\Doc}{\C\op}{\Pos}$ be a doctrine and $\TNat{\necmod}{\Doc}{\Doc}$ be
operator on $\Doc$.
Then, ,,𝕀,𝕀 is a comonad on $\Doc$.

There is only to check that 𝕀,,𝕀
and 𝕀,,· are
well-defined 2-arrows. But, for each object $X$ in , $\necmod_X\order\id{\Doc X}$ and
$\necmod_X\order \necmod_X \cdot \necmod_X$ hold  by modality.

In other words, modality-to-cmd shows that operator on a
doctrine is exactly a vertical comonad on it.

We introduce the 2-functor $\fun{\MCFun}{\NecIdxPos}{\Cmd{\IdxPos}}$ by letting, for
, a doctrine with operator,
$\MCFun(\ple{\Doc,\necmod})\colon= \ple{\Doc,\Id{},\necmod,\id{},\id{}}$, which is a
comonad by modality-to-cmd;
for a 1-arrow F,f,^,^
$\MCFun(\ple{F,f})\colon= \ple{F,f,\id{}}$;
for a 2-arrow θF,fG,g
$\MCFun(\theta)\colon= \theta$.

With the assignments above,   is a 2-functor.

The proof is straightforward.
The only interesting part is checking that it is well-defined on the 1-arrows. Indeed,
for each object $X$ in the base category of the doctrine $\Doc$, we have
$f_X\cdot\necmod^\Doc_X\order\necmod^\aDoc_{FX}\cdot f_X$, by definition of 1-arrow
in . And this ensures that
𝕀F,f·^F,(^F)·f is a
2-arrow in .

It is easy to see that the 2-functor $\MCFun$ is full and faithful.
Hence the 2-category $\NecIdxPos$ is isomorphic to the 2-category of
vertical comonads in $\IdxPos$.

Now let  be the composition
$\xymatrix {\NecIdxPos \ar[r]^{\MCFun} & \Cmd{\IdxPos} \ar[r]^{\EMAFun} & \Adj{\IdxPos}}$
which sends an object , in to the Eilenberg-Moore adjunction
of the associated comonad $\MCFun(\Doc,\necmod)=\ple{\Id{\C},\necmod,\id{},\id{}}$

\[\xymatrix@=5em{
\necmod\Doc\ar@<.5ex>@/^/[r]^{\ple{\Id{\C},\ForgetLift}}\ar@{}[r]|{\bot}
&\Doc \ar@<.5ex>@/^/[l]^{\ple{\Id{\C},\necmod}}}\]

where, from the general construction in (<ref>), the Eilenberg-Moore object
for the comonad induced by $\necmod$ is
$\necmod\Doc X=\set{\alpha \in \Doc X}{\alpha=\necmod_X\alpha}$. Also
$\DReIdx{\necmod\Doc}{f}=\DReIdx{\Doc}{f}$, and $\TNat{\ForgetLift}{\necmod\Doc}{\Doc}$ is
the inclusion.

There is a local adjunction $\MAFun \dashv \AMFun$, where

* the unit $\TNat{\Delta}{\Id{\NecIdxPos}}{\AMFun \cdot \MAFun}$ is the identity lax
2-natural transformation, and

* the counit $\TNat{\nabla}{\MAFun \cdot \AMFun}{\Id{\Adj{\IdxPos}}}$ is given, for
an adjunction $\adj=\ple{\Doc,\aDoc,\LAdj,\LAdjLift,\RAdj,\RAdjLift,\unit,\counit}$
where $\fun{\Doc}{\C\op}{\Pos}$ and $\fun{\aDoc}{\D\op}{\Pos}$, by
$\nabla_\adj=\ple{\Id{\C},(\Doc\unit\op)\cdot(\RAdjLift\LAdj\op),\LAdj,\id{},\unit}$, as
in the following diagram

\[\xymatrix{
\necmod\aDoc\LAdj\op \ar[dd]_{\ple{\Id{\C},(\Doc\unit\op)\cdot(\RAdjLift\LAdj\op)}}
\ar@/^8pt/[rr]^{\ple{\Id{\C},\ForgetLift}} \ar@{}[rr]|{\bot}  &&
\aDoc\LAdj\op \ar@/^8pt/[ll]^{\ple{\Id{\C},\necmod^\adj}} \ar[dd]^{\ple{\LAdj,\id{}}}  \\
&& \\
\Doc  \ar@/^8pt/[rr]^{\ple{\LAdj,\LAdjLift}} \ar@{}[rr]|{\bot}
\xtwocell[rruu]{}<>{_\unit}
&&  \aDoc \ar@/^8pt/[ll]^{\ple{\RAdj,\RAdjLift}}
} \]

and, for each 1-arrow $\oneAr{\phi}{\adj}{\aadj}$,
$\nabla_\phi = \ple{\id{},\id{}}$.

The fact that $\Delta$ is a well-defined lax 2-natural transformation is straightforward, since $\AMFun \cdot \MAFun = \Id{\NecIdxPos}$.
We check that $\nabla_\adj$ is a 1-arrow from $\MAFun(\ple{\aDoc\LAdj\op,\necmod^\adj})$ to $\adj$.
We have $\ple{\LAdj \circ \Id{\C},\LAdjLift \cdot (\Doc\unit\op)\cdot(\RAdjLift\LAdj\op)} = \ple{\LAdj \circ \Id{\C},\id{} \cdot \ForgetLift}$, since, for each object $X$ in and $\alpha \in \necmod\aDoc\LAdj\op X$, we have $\LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) = \necmod^\adj_X \alpha = \alpha$, by definition of $\necmod\aDoc\LAdj\op$.
Then, we have to check that $\twoAr{\unit}{\ple{\Id{\C} \circ \Id{\C},(\Doc\unit\op)\cdot (\RAdjLift\LAdj\op) \cdot \necmod^\adj}}{\ple{\RAdj\LAdj,(\RAdjLift\LAdj\op)\cdot \id{}}}$ is a 2-arrow in ,
but this holds because $\TNat{\unit}{\Id{\C}}{\RAdj\LAdj}$ is a natural transformation and , for each object $X$ in , $\necmod^\adj_X \order \id{\aDoc\LAdj\op X}$, hence we get
$\DReIdx{\Doc}{\unit_X} \circ \RAdjLift_{\LAdj X} \circ \necmod^\adj_X \order \DReIdx{\Doc}{\unit_X} \circ \RAdjLift_{\LAdj X}$.

Now, consider a 1-arrow $\oneAr{\phi = \ple{F, f, G, g, \theta}}{\adj}{\aadj}$ in $\Adj{\IdxPos}$;
hence, we have $\MAFun(\AMFun(\phi)) = \ple{F, g(\LAdj^\adj)\op, F, g(\LAdj^\adj)\op, \id{}}$, and
we have to show that

\[
\twoAr{\nabla_\phi = \ple{\id{},\id{}}}{\ple{F, f, G, g, \theta} \circ \nabla_\adj}{\nabla_\aadj \circ \ple{F, g(\LAdj^\adj)\op, F, g(\LAdj^\adj)\op, \id{}} }
\]

is a 2-arrow in $\Adj{\IdxPos}$.
To this end, it is enough to prove that

\[\twoAr{\id{}}
{\ple{F,(\Doc^\aadj(\unit^\aadj)\op F\op)\cdot
(\RAdjLift^\aadj(\LAdj^\aadj)\op F\op)\cdot(g(\LAdj^\adj)\op)}}\]

\[\twoAr{\id{}}{\ple{G\LAdj^\adj,g(\LAdj^\adj)\op}}{\ple{\LAdj^\aadj F,g(\LAdj^\adj)\op}}\]

are 2-arrows in , since the other conditions are trivially satisfied as the two
components are identities.
The second is a 2-arrow since, by definition of 1-arrow in $\Adj{\IdxPos}$, the equality
$G\LAdj^\adj = \LAdj^\aadj F$ holds.
To see that so is the first, consider the following inequalities for $X$ an object in :

\begin{align*}
f_X \circ \DReIdx{\Doc^\adj}{\unit^\adj_X} \circ \RAdjLift^\adj_{\LAdj^\adj X}
&= \DReIdx{\Doc^\aadj}{F\unit^\adj_X} \circ f_{\RAdj^\adj\LAdj^\adj X} \circ \RAdjLift^\adj_{\LAdj^\adj X}
&& f\text{ is natural} \\
&\order \DReIdx{\Doc^\aadj}{F\unit^\adj_X} \circ \DReIdx{\Doc^\aadj}{\theta_{\LAdj^\adj X}} \circ \RAdjLift^\aadj_{G\LAdj^\adj X} \cdot g_{\LAdj^\adj X}
&& \theta \text{ is a 2-arrow in \IdxPos} \\
&= \DReIdx{\Doc^\aadj}{\unit^\aadj_{FX}} \circ \RAdjLift^\aadj_{\LAdj^\aadj FX} \circ g_{\LAdj^\adj X}
&& (\theta\LAdj^\adj)(F\unit^\adj) = \unit^\aadj F \text{ and } G\LAdj^\adj = \LAdj^\aadj F
\end{align*}

Finally, we have the check the adjunction triangular laws:
$(\AMFun \nabla)(\Delta \AMFun) =
\Id{\AMFun}$ and $(\nabla \MAFun)(\MAFun \Delta) = \Id{\MAFun}$.
The former holds as $\AMFun (\nabla_\adj)$
is the identity on $\AMFun(\adj)$ for any adjunction $\adj$.
The latter holds because, for any object , in ,
$\nabla_{\MAFun(\ple{\Doc,\necmod})}$ is the
identity on $\MAFun(\ple{\Doc,\necmod})$, since
$\MAFun(\ple{\Doc,\necmod})$ is the Eilenberg-Moore adjunction of the comonad
,,𝕀,𝕀 on $\Doc$.

Now recall that, by definition, we have $\MAFun = \EMAFun\cdot\MCFun$ and observe that
$\CmdFun\cdot\EMAFun=\Id{\Cmd{\IdxPos}}$. Hence  $\MCFun = \CmdFun \circ \MAFun$.
Therefore, $\MCFun \dashv \CMFun$ is a local adjunction, as stated in the following

There is a diagram of $($lax$)$ 2-adjunctions

\[\xymatrix@=6em{\Cmd{\IdxPos}\ar@/_/[r]_-{\EMAFun}\ar@{{}{}}[r]|-{\bot}
\ar@/^/[rd]^-{\CMFun}
\ar@/^/[lu]^-{\MCFun} }\]

where the diagonal adjunction is the composite of the other two.

Finally we refine adj-factorization, providing a new factorization through the
doctrine $\necmod\aDoc\LAdj\op$.

Let $\fun{\Doc}{\C\op}{\Pos}$ and $\fun{\aDoc}{\D\op}{\Pos}$ be doctrines and consider an adjunction $\ple{\LAdj, \LAdjLift, \RAdj, \RAdjLift, \unit, \counit}$ between them.
Then, the following diagram (of adjunctions)

\[ \xymatrix@R+15pt@C+5pt{
&&& \ar@/_8pt/[llld]_*=/^8pt/[flip][@]{\ple{\Id{\C},(\Doc\unit\op)(\RAdjLift\LAdj\op)}} \necmod\aDoc\LAdj\op
\ar@/_8pt/[dd]_{\ple{\Id{\C},\ForgetLift}} \ar@{}[dd]|{\dashv}
\ar@/_8pt/[rrrd]_*=/^8pt/[@]{\ple{\LAdj,\ForgetLift}} \ar@{}[rrrd]|*=0[@]{\top} &&& \\
\Doc \ar@/_8pt/[rrru]_*=/^8pt/[@]{\ple{\Id{\C},\LAdjLift}}  \ar@{}[rrru]|*=0[@]{\top}
\ar@/^8pt/[rrrd]^*=/^8pt/[@]{\ple{\Id{\C},\LAdjLift}} \ar@{}[rrrd]|*=0[@]{\bot}   &&&
\aDoc \ar@/_8pt/[lllu]_*=/^8pt/[flip][@]{\ple{\RAdj,\necmod(\aDoc\counit\op)}}
\ar@/^8pt/[llld]^*=/dl8pt/[flip][@]{\ple{\RAdj,\aDoc\counit\op}}   \\
&&& \ar@/^8pt/[lllu]^*=/dr8pt/[flip][@]{\ple{\Id{\C},(\Doc\unit\op)(\RAdjLift\LAdj\op)}}
\aDoc\LAdj\op \ar@/_8pt/[uu]_{\ple{\Id{\C},\necmod}}
\ar@/^8pt/[rrru]^*=/^8pt/[@]{\ple{\LAdj,\id{}}} \ar@{}[rrru]|*=0[@]{\bot}    &&&
} \]

commutes. Moreover $\TNat{\LAdjLift}{\Doc}{\necmod\aDoc\LAdj\op}$ is surjective and
$\TNat{(\Doc\unit\op)(\RAdjLift\LAdj\op)}{\necmod\aDoc\LAdj\op}{\Doc}$ is injective.

The commutativity of the diagram follows immediately from the definition of $\necmod$ and
trivial-modality1 and adj-factorization.
The fact that, for each object $X$, the function
$\fun{\LAdjLift_X}{\Doc X}{\necmod\aDoc\LAdj\op X}$ is
surjective and
$\fun{\DReIdx{\Doc}{\unit_X}\RAdjLift_{\LAdj X}}{\necmod\aDoc\LAdj\op X}{\Doc X}$ is
injective, follows from trivial-modality2, noting that
$\necmod_X = \LAdjLift_X \circ \DReIdx{\Doc}{\unit_X} \circ \RAdjLift_{\LAdj X}$ is the
identity on $\necmod\aDoc\LAdj\op X$ by definition.

[Temporal Logics]
Consider the standard powerset doctrine , sending a set $X$ to
the powerset $\pw{X}$ and a function tXY to the inverse image function
tYX, and a 1-arrow F,f.
Suppose that F is an accessible functor, hence it admits a free comonad
([13]) ^F. We recall the construction in the

* Given a set $A$, let $\cmdfun^F A = \nu X. A\times FX$ be the (underlying set of
the) final coalgebra for the functor

\[\xymatrix<EMAIL_ADDRESS>F}&\ct{Set}\\
X\ar@{|->}[r]&A\times FX}\]

and denote by ζ_A^F AA×F(^F A) the structure map of the
final $A\times F$-coalgebra, which is an iso by the Lambek Lemma.

* Since
𝕀,_2∘ζ_A^FA^FA×F(^FA) is a
$\cmdfun^FA\times F$-coalgebra, there is a unique $\cmdfun^FA\times F$-coalgebra homomorphism
^F_A^FA^F^FA such that the diagram

\[\xymatrix@C=4em@R=3em{\cmdfun^FA\ar[r]^-{\ple{\id{},\proj_2\circ\zeta_A}}\ar[d]_{\cmu^F_A}
&\cmdfun^FA\times F(\cmdfun^FA)\ar[d]^{\cmu^F_A\times\id{}}\\
\cmdfun^F\cmdfun^F A\ar[r]^-{\zeta_A}&\cmdfun^F\cmdfun^F\times F(\cmdfun^F\cmdfun^F A)}\]

* Let ^F_A^FAA be

* Given a function tBA, the function
ζ_B^F BB×F(^F B) is a final $B\times F$-coalgebra; let
^F t^F B^F A be the unique $A\times F$-homomorphism such
that the diagram

\[\xymatrix{\cmdfun^F B\ar[r]^{\zeta_B}\ar[d]_{\cmdfun^F t}
&B\times F(\cmdfun^F B)\ar[r]^{t\times \id{}}&A\times F(\cmdfun^F B)\ar[d]^{\cmdfun^F t}\\
\cmdfun^F A\ar[rr]^{\zeta_A}&&A\times F(\cmdfun^F A)\\}\]

We can also define a natural transformation _f^F as
Consider a set $A$ and a subset $\alpha\in\pw{A}$.
We define a function ϕ_α^F A^F A as
$\phi_\alpha(\beta) = \zeta_A\inv(\alpha \times f_{\cmdfun^FA}(\beta))$, which is monotone
by construction, hence, since ^FA is a complete lattice, by the Knaster-Tarski
theorem, $\phi_\alpha$ has a greatest fixed point,
given by
$\nu\phi_\alpha=\bigcup\set{\beta\in\pw{\cmdfun^F A}}{\beta\subseteq\phi_\alpha(\beta)}$.

Define $\cmdlift^f_A(\alpha)$ as $\nu\phi_\alpha$.
This function is monotone, because, if $\alpha\subseteq\beta$, then $\nu\phi_\alpha =
\zeta_A\inv(\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) \subseteq \zeta_A\inv(\beta\times
f_{\cmdfun^FA}(\nu\phi_\alpha)) = \phi_\beta(\nu\phi_\alpha)$. Thus, by coinduction, we
get $\nu\phi_\alpha\subseteq\nu\phi_\beta$, as needed.
In order to prove that $\cmdlift^f_A$ is natural in $A$, we have to check that, for each
function tBA and $\alpha \in \pw{A}$,
it is the case that $(\cmdfun^F t)\inv(\nu\phi_\alpha) = \nu\phi_{t\inf(\alpha)}$.
First, note that

\[\begin{split}
(\cmdfun^F t)\inv(\nu\phi_\alpha) &= (\cmdfun^F t)\inv(\zeta_A\inv(\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha))) \\
&= (\zeta_A\circ\cmdfun^Ft)\inv (\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) \\
&= ((\id{}\times F\cmdfun^Ft)\circ (t\times \id{}) \circ \zeta_B)\inv (\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) \\
&= \zeta_B\inv (t\inv(\alpha)\times (F\cmdfun^Ft)\inv(f_{\cmdfun^FA}(\nu\phi_\alpha))) \\
&= \zeta_B\inv (t\inv(\alpha)\times f_{\cmdfun^FB}((\cmdfun^Ft)\inv(\nu\phi_\alpha))) \\
&= \phi_{t\inv(\alpha)}((\cmdfun^F t)\inv(\nu\phi_\alpha)).
\end{split}\]

Hence, by coinduction, we get $(\cmdfun^Ft)\inv(\nu\phi_\alpha) \subseteq
\nu\phi_{t\inv(\alpha)}$. To prove the other inclusion,  we just have to prove that
$\cmdfun^Ft[\nu\phi_{t\inv(\alpha)}] \subseteq \nu\phi_\alpha$, where $\cmdfun^Ft[\beta]$
denotes the direct image of $\beta\in\pw{\cmdfun^FB}$ along $\cmdfun^Ft$.
To this end, we note that

\[\begin{split}
\cmdfun^Ft[\nu\phi_{t\inv(\alpha)}] &
\subseteq \cmdfun^Ft[\zeta_B\inv(t\inv(\alpha)\times f_{\cmdfun^FB}(\nu\phi_{t\inv(\alpha)}))] \\
&=\cmdfun^Ft[((t\times\id{})\circ\zeta_B)\inv(\alpha\times f_{\cmdfun^FB}(\nu\phi_{t\inv(\alpha)}))] \\
&\subseteq \zeta_A\inv((\id{}\times F\cmdfun^Ft)[\alpha\times f_{\cmdfun^FB}(\nu\phi_{t\inv(\alpha)})]) \\
&= \zeta_A\inv(\alpha \times F\cmdfun^Ft[f_{\cmdfun^FB}(\nu\phi_{t\inv(\alpha)})]) \\
&\subseteq \zeta_A\inv(\alpha\times f_{\cmdfun^FA}(\cmdfun^Ft[\nu\phi_{t\inv(\alpha)}])) \\
\end{split}\]

To check that $\cmd^F = \ple{\cmdfun^F,\cmdlift^F,\cmu^F,\cun^F}$ is a comonad on , it
is enough to show the following two inequalities:
(1) $\cmdlift^F_A(\alpha) \subseteq (\cun^F_A)\inv(\alpha)$ and
(2) $\cmdlift^F_A(\alpha) \subseteq
(\cmu^F_A)\inv(\cmdlift^F_{\cmdfun^FA}(\cmdlift^F_A(\alpha)))$ for all $\alpha\in\pw{A}$.

Ad (1) note that $\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha) \subseteq
\proj_1\inv(\alpha)$. Hence
$\nu\phi_\alpha = \zeta_A\inv(\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) \subseteq
\zeta_A\inv(\proj_1\inv(\alpha)) = (\cun^F_A)\inv(\alpha)$.

Ad (2) we show $\cmu^F_A[\nu\phi_\alpha] \subseteq \nu\phi_{\nu\phi_\alpha}$.
First of all, since $\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha) \subseteq
\proj_2\inv(f_{\cmdfun^FA}(\nu\phi_\alpha))$, we have
$\nu\phi_\alpha = \zeta_A\inv(\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) \subseteq
Hence $\nu\phi_\alpha \subseteq
\nu\phi_\alpha\cap (\proj_2\circ\zeta_A)\inv(f_{\cmdfun^FA}(\nu\phi_\alpha)) =
\ple{\id{},\proj_2\circ\zeta_A}\inv(\nu\phi_\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha))$.

\[\begin{split}
\cmu^F_A[\nu\phi_\alpha] &\subseteq  \cmu^F_A[ \ple{\id{},\proj_2\circ\zeta_A}\inv(\nu\phi_\alpha\times f_{\cmdfun^FA}(\nu\phi_\alpha)) ] \\
&\subseteq \zeta_{\cmdfun^FA}\inv( (\id{}\times F\cmu^F_A)[ \nu\phi_\alpha \times f_{\cmdfun^FA}(\nu\phi_\alpha) ]) \\
&= \zeta_{\cmdfun^FA}\inv( \nu\phi_\alpha \times F\cmu^F_A[ f_{\cmdfun^FA}(\nu\phi_\alpha) ] ) \\
&\subseteq \zeta_{\cmdfun^FA}\inv( \nu\phi_\alpha\times f_{\cmdfun^F\cmdfun^FA}( \cmu^F_A[\nu\phi_\alpha] ) ) \\
&= \phi_{\nu\phi_\alpha}(\cmu^F_A[\nu\phi_\alpha]).
\end{split}\]

Thus by coinduction we obtain (2).

Applying the construction in cmd-to-modality, we obtain a
comonadic modal operator $\necmod^{\cmd^F}$ on the indexed poset
mapping a coalgebra A,c for the comonad $\cmd^F$ to $\pw{A}$ and a coalgebra
morphism tB,dA,c to the inverse image function
Explicitly, given a coalgebra A,c and an element $\alpha\in\pw{A}$, we have
$\necmod^{\cmd^F}_{\ple{A,c}} \alpha = c\inv(\cmdlift^F_A(\alpha)) = c\inv(\nu\phi_\alpha)$.

This setting has a temporal interpretation:
given the 1-arrow F,f, the functor $F$ represents the “branching type”, namely,
the branching structure of time, and $f$ lifts formulas to branches.
The functor $\cmdfun^F$ models the whole time structure, that is, the present and all
possible futures, generated by the branching type $F$, and $\cmdlift^F$ lifts a formula to
time structures, basically, universally quantifying over time, according to $f$, roughly
saying that the formula holds in all possible future branches.
Given a coalgebra A,c for the comonad $\cmd^F$, for each $x\in A$, $c(x)$ represents
the whole evolution of $x$  along time,
hence, for each $\alpha\in\pw{A}$, we have $x\in \necmod^{\cmd^F}_{\ple{A,c}} \alpha$ if
all future evolutions of $x$ belongs to $\alpha$.
Therefore, roughly, $\necmod^{\cmd^F}$ is a generic kind of “always” modality, typical
of temporal logics. In the following we consider two explicit instances of this situation.

[Linear time]
Consider $\ple{F,f}=\ple{\Id{},\id{}}$, that is, each instant has exactly one possible future.
The free comonad is the stream comonad $\Str A = \nu X. A\times X = A^\omega$, mapping a set $A$ to the set $A^\omega$ of sequences of elements in $A$ indexed over natural numbers.
Given a sequence $a\in A^\omega$, we write $s_i$ to denote the $i$-th element of $s$, and $s[i..]$ to denote the sequence $r\in A^\omega$ such that $r_j = s_{j+i}$ for all $j\in\N$.
Then, the counit maps $s$ to $s_0$ (the first element, namely the present) and the comultiplication maps $s$ to the sequence $(s[i..])_{i\in\N}$, namely the sequence of all suffixes of $s$.

Let $\alpha\in\pw{A}$, we have $\cmdlift^F_A(\alpha) = \{ s\in A^\omega \mid s_i\in\alpha \mbox{ for all } i\in\N\}$, namely, the set of sequences where all elements belongs to/satisfies $\alpha$.
Therefore, if A,c is a coalgebra for , $\necmod^\Str_{\ple{A,c}} \alpha = \{ x \in A \mid c(x)_i \in\alpha\mbox{ for all }i\in\N\}$, that is, it is the set of all elements $x\in A$ such that all its future instances (including the present one) belongs to $\alpha$.

Therefore, $\necmod^\Str_{\ple{A,c}}$ provides a model for the “globally” ($\mathbf{G}$) modality of Linear Temporal Logic (LTL) [5] and, moreover,
the modality on the free coalgebra A, ^_A implements exactly the standard semantics of such a modality on infinite sequences.

[Finitely ordered branching time]
Let  F be the functor $FX = \bigcup_{n\in\N} X^n$.
We can consider several natural transformations fF making
F,f a 1-arrow.
The two paradigmatic examples are the following:
$f^\forall_A(\alpha) = \{ \ple{n,\ple{x_1,\ldots,x_n}} \in FX \mid x_i \in \alpha \mbox{ for all }  i \in 1..n\}$ and
$f^\exists_A(\alpha) = \{ \ple{n,\ple{x_1,\ldots,x_n}} \in FX \mid x_i \in \alpha \mbox{ for some } i \in 1..n\}$.

The free comonad is $\OFTree$, mapping a set $A$ to the set of finitely branching and
ordered trees labelled by $A$.
Formally, such a tree is a partial function t^⋆A with a
non-empty and prefix-closed domain such that, if $\ple{k_1,\ldots,k_n}\in \dom{t}$ and
$k\le k_n$, then $\ple{k_1,\ldots,k}\in \dom{t}$ ([10, 1]).
The counit maps a tree $t$ to the label of its root, that is $t(\varepsilon)$, where
$\varepsilon$ is the empty sequence, and
the comultiplication maps a tree $t$ to $\cmu^F_A(t)$ such that $\dom{\cmu^T_A(t)} =
\dom{t}$ and $\cmu^F_A(t)(u)$ is the subtree of $t$ rooted at $u\in\dom{t}$.
The behaviour of the natural transformation $\cmdlift^F$ of course depends on $f$, for instance,
for $f = f^\forall$, it maps $\alpha\in\pw{A}$ to the set of trees where all nodes have label in $\alpha$, while
for $f = f^\exists$, it maps $\alpha\in\pw{A}$ to the set of trees containing an infinite path starting from the root where all nodes have label in $\alpha$.

Then, given a coalgebra A,c for the comonad and $\alpha\in\pw{A}$, we have
$x\in \necmod^\OFTree_{\ple{A,c}}\alpha$ if all nodes in $c(x)$ have label in $\alpha$,
when $f=f^\forall$, and if there is an infinite path in $c(x)$ where all nodes have label
in $\alpha$, when $f=f^\exists$.
Therefore, $\necmod^\OFTree_{\ple{A,c}}$ provides a model for the modalities
“invariantly” ($\mathbf{AG}$) and “potentially always” ($\mathbf{EG}$) of Computation
Tree Logic (CTL) [5], depending on the choice of $f$.

§ ACKNOWLEDGMENT

The authors would like to thank Jacopo Emmenegger, Fabio Pasquali and Cosimo Perini Brogi
for many helpful discussions on the subject.

[1]
Aczel, P., Adámek, J., Milius, S., and Velebil, J. 2003.
Infinite trees and completely iterative theories: a coalgebraic view.
Theoret. Comput. Sci., 300(1-3):1–45.

[2]
Awodey, S. and Birkedal, L. 2003.
Elementary axioms for local maps of toposes.
J. Pure Appl. Algebra, 177(3):215–230.

[3]
Awodey, S., Birkedal, L., and Scott, D. S. 2002.
Local realizability toposes and a modal logic for computability.
Math. Structures Comput. Sci., 12(3):319–334.

[4]
Awodey, S., Kishida, K., and Kotzsch, H.-C. 2014.
Topos semantics for higher-order modal logic.
Log. Anal. (N.S.), 226:591–636.

[5]
Baier, C. and Katoen, J. 2008.
Principles of model checking.
MIT Press.

[6]
Benton, P. N. 1994.
A mixed linear and non-linear logic: Proofs, terms and models.
In Pacholski, L. and Tiuryn, J., editors, Computer Science Logic, 8th International Workshop, CSL '94, volume 933 of
Lecture Notes in Computer Science, pp. 121–135. Springer.

[7]
Betti, R. and Power, A. J. 1988.
On local adjointness of distributive bicategories.
Bollettino della Unione Matematica Italiana, 2(4):931–947.

[8]
Blackwell, R., Kelly, G. M., and Power, A. J. 1989.
Two-dimensional monad theory.
J. Pure Appl. Algebra, 59(1):1–41.

[9]
Braüner, T. and Ghilardi, S. 2007.
First-order modal logic.
In Blackburn, P., van Benthem, J. F. A. K., and
Wolter, F., editors, Handbook of Modal Logic., volume 3 of Studies in logic and practical reasoning, pp. 549–620. North Holland
Publishing Company.

[10]
Courcelle, B. 1983.
Fundamental properties of infinite trees.
Theoret. Comput. Sci., 25:95–169.

[11]
Emmenegger, J., Pasquali, F., and Rosolini, G. 2020.
Elementary doctrines as coalgebras.
J. Pure Appl. Algebra, 224(12):106445, 16.

[12]
Esakia, L. 2004.
Intuitionistic logic and modality via topology.
Ann. Pure Appl. Logic, 127(1-3):155–170.

[13]
Ghani, N., Lüth, C., Marchi, F. D., and Power, J. 2001.
Algebras, coalgebras, monads and comonads.
Electron. Notes Theor. Comput. Sci., 44(1):128–145.

[14]
Ghilardi, S. and Meloni, G. C. 1988.
Modal and tense predicate logic: models in presheaves and categorical
In Categorical algebra and its applications
(Louvain-La-Neuve, 1987), volume 1348 of Lecture Notes in Math.,
pp. 130–142. Springer, Berlin.

[15]
Hermida, C. 1994.
On fibred adjunctions and completeness for fibred categories.
In Recent trends in data type specification (Caldes de
Malavella, 1992), volume 785 of Lecture Notes in Comput. Sci., pp.
235–251. Springer, Berlin.

[16]
Hermida, C. 1999.
Some properties of fib as a fibred 2-category.
Journal of Pure and Applied Algebra, 134(1):83–109.

[17]
Jacobs, B. 1999.
Categorical Logic and Type Theory.
North Holland Publishing Company.

[18]
Johnstone, P. T. 2002.
Sketches of an elephant: a topos theory compendium. Vol. 1,
volume 43 of Oxford Logic Guides.
The Clarendon Press Oxford University Press.

[19]
Lawvere, F. W. 1969.
Adjointness in foundations.
Dialectica, 23:281–296.
also available as Repr. Theory Appl. Categ., 16 (2006) 1–16.

[20]
Lawvere, F. W. 1970.
Equality in hyperdoctrines and comprehension schema as an adjoint
In Heller, A., editor, Proc. New York Symposium on
Application of Categorical Algebra, pp. 1–14. Amer.Math.Soc.

[21]
Mac Lane, S. and Moerdijk, I. 1992.
Sheaves in Geometry and Logic a First Introduction to Topos
Springer, New York, NY.

[22]
Maietti, M. E. and Rosolini, G. 2013a.
Elementary quotient completion.
Theory Appl. Categ., 27:445–463.

[23]
Maietti, M. E. and Rosolini, G. 2013b.
Quotient completion for the foundation of constructive mathematics.
Log. Univers., 7(3):371–402.

[24]
Maietti, M. E. and Rosolini, G. 2015.
Unifying exact completions.
Appl. Categ. Structures, 23:43–52.

[25]
Moeller, J. and Vasilakopoulou, C. 2020.
Monoidal Grothendieck Construction.
Theory Appl. Categ., 35(31):1159–1207.

[26]
Power, A. J. and Watanabe, H. 2002.
Combining a monad and a comonad.
Theoret. Comput. Sci., 280(1-2):137–162.

[27]
Reyes, G. E. 1991.
A topos-theoretic approach to reference and modality.
Notre Dame J. Form. Log., 32(3):359–391.

[28]
Rosenthal, K. I. 1990.
Quantales and their applications, volume 234 of Pitman
Research Notes in Mathematics Series.
Longman Scientific & Technical, Harlow; copublished in the United
States with John Wiley & Sons, Inc., New York.

[29]
Street, R. 1972.
The formal theory of monads.
J. Pure Appl. Algebra, 2(2):149 – 168.

[30]
Streicher, T. 1991.
Semantics of type theory.
Progress in Theoretical Computer Science. Birkhäuser Boston,
Inc., Boston, MA.
Correctness, completeness and independence results, With a foreword
by Martin Wirsing.

§ OPERATORS FROM LINEAR-NONLINEAR ADJUNCTIONS

A well-known approach to provide categorical semantics to the linear exponential modality
$\Lbang$—read as “bang”—of propositional linear logic is by means of
linear-nonlinear adjunctions as in [6].
A linear-nonlinear adjuction is a monoidal adjunction beween a symmetric monoidal
category and a cartesian category; the induced comonad on the symmetric monoidal
category interprets the bang modality.
This notion is easily extended to doctrines where the construction in
adj-to-modality provides a model of the bang modality in a higher order setting.

In the present context, the role of the cartesian category is played by a
primary doctrine, that is, a doctrine

where has finite products and, for each object $X$ in , the fiber $\Doc X$ carries an
inf-semilattice structure preserved by reindexing, see [11].
The symmetric monoidal category turns into a
$($symmetric$)$ monoidal doctrine, which we define below, following the definition
of monoidal indexed categories in [25]. We shall employ the 2-cartesian
structure of the 2-category . So, in the following, given indexed posets
and , we denote by
×(×) the product doctrine mapping a pair of
objects X,Y to the product (in )
$\Doc X\times\aDoc Y$ and acting similarly on arrows. Furthermore, we denote by $\One$ the
terminal doctrine whose base is the terminal category and mapping its unique object
to the singleton poset. We shall write
λ_P×PP, ρ_P×PP, and
for the usual 1-iso for associativity, left and right identity, and symmetry.

A $($symmetric$)$ monoidal doctrine consists of

* a doctrine ,

* two 1-arrows ⊗,∙× and
I,ι, and

* four invertible 2-arrows

\[\begin{array}{c@{\qquad}c}
\multicolumn2c{\twoAr{a}{\ple{\otimes,\bullet}\circ
\twoAr{l}{\ple{\otimes,\bullet}\circ(\ple{I,\iota}\times\ple{\Id{},\id{}})}
\twoAr{r}{\ple{\otimes,\bullet}\circ(\ple{\Id{},\id{}}\times\ple{I,\iota})}
\multicolumn2c{\twoAr{s}{\ple{\otimes,\bullet}\circ\sigma_{Q,Q}}{\ple{\otimes,\bullet}}}
\end{array}\]

such that ,⊗,I,a,l,r,s is a symmetric monoidal category.
As the 2-arrows $a$, $l$, $r$ and $s$ are invertible, the inequalities they induce on the
fibres are actually equalities, namely, the following diagrams commute

\[\xymatrix@C=5em@R=1em{(\aDoc A \times \aDoc B) \times \aDoc C
\ar[dd]_{\bullet_{A,B} \times \id{}} \ar[r]^{(\alpha_{Q,Q,Q})_{A,B,C}}
&\aDoc A \times (\aDoc B \times \aDoc C) \ar[rd]^{\id{} \times \bullet_{B,C}}\\
&&\aDoc A \times \aDoc (B\otimes C) \ar[dd]^{\bullet_{A,B\otimes C}}\\
\aDoc (A\otimes B) \times \aDoc C \ar[dr]^{\bullet_{A\otimes B,C}} \\
&\aDoc ((A\otimes B)\otimes C) \ar[r]^{\DReIdx{\aDoc}{(a_{A,B,C})}} &
\aDoc (A\otimes (B\otimes C))}\]

\[\xymatrix{
\aDoc 1 \times A \ar[d]_{(\lambda_Q)_A} \ar[r]^{\ple{\iota,\id{}}}
& \aDoc I \times \aDoc A \ar[d]^{\bullet_{I,A}}\\
\aDoc A \ar[r]^-{\DReIdx{\aDoc}{(l_A)}} & \aDoc (I\otimes A)}\qquad
\xymatrix{\aDoc A \times 1 \ar[d]_{(\rho_Q)_A} \ar[r]^{\ple{\id{},\iota}}
& \aDoc A \times \aDoc I \ar[d]^{\bullet_{A,I}}\\
\aDoc A \ar[r]^-{\DReIdx{\aDoc}{(r_A)}}& \aDoc (A\otimes I)}\]

\[\xymatrix{\aDoc A \times \aDoc B \ar[d]_{(\sigma_Q)_{A,B}} \ar[r]^{\bullet_{A,B}}
& \aDoc (A\otimes B) \ar[d]^{\DReIdx{\aDoc}{(s_{A,B})}} \\
\aDoc B \times \aDoc A \ar[r]^{\bullet_{B,A}} & \aDoc(B\otimes A)}\]

Note that a primary doctrine  is a monoidal doctrine with
×,⊓× and 1,⊤_1, where
$1$ is the terminal object and $\top_1$ is the top element in $\Doc 1$,
$\times$ is the binary product in the category and $\sqcap$ is defined, for all objects
$X,Y$ in , by
$\sqcap_{X,Y} = \Land_{X\times Y}\circ(\DReIdx{\Doc}{\pi_1}\times\DReIdx{\Doc}{\pi_2})$,
where π_1X×YX and π_2X×YY are the projections.

Now, consider a primary doctrine and a monoidal doctrine .
An adjunction ,,,,,,, is said to be monoidal if $\LAdj$ and $\RAdj$ are lax monoidal functors and $\unit$ and $\counit$ are monoidal natural trasformations, that is, we have the following additional structure:

* two 2-arrows uI,ι∘1,⊤ and ϕ⊗,∙∘(,×,),∘×,⊓, that is, uI1 and, for all objects $X,Y$ in , ϕ_X,YX ⊗Y(X⊗Y) are arrows in , and

* two 2-arrows v1,⊤,∘I,ι and ψ×,⊓∘(,×,),∘×,⊓, that is, v1I and, for all objects $A,B$ in , ψ_A,BA ×B(A×B) are arrows in , and

* the following diagrams commute

\[\xymatrix{
X\times Y \ar[d]_{\unit_X\times\unit_Y} \ar[rr]^{\id{X\times Y}}&&X\times Y \ar[d]^{\unit_{X\times Y}}\\
\RAdj\LAdj X \times \RAdj\LAdj Y \ar[r]^{\psi_{\LAdj X,\LAdj Y}}
&\RAdj(\LAdj X \otimes \LAdj Y) \ar[r]^{\RAdj\phi_{X,Y}} & \RAdj\LAdj(X\times Y)}\]

\[\xymatrix{\LAdj\RAdj A\otimes\LAdj\RAdj B\ar[d]_{\counit_A\otimes\counit_B}\ar[r]^{\phi_{\RAdj A,\RAdj B}}&
\LAdj(\RAdj A \times \RAdj B) \ar[r]^{\LAdj\psi_{A,B}}
&\LAdj\RAdj(A\otimes B) \ar[d]^{\counit_{A\otimes B}} \\
A\otimes B \ar[rr]^{\id{A\otimes B}} && A\otimes B}\]

\[\xymatrix{
1 \ar[d]_{\unit_1} \ar[r]^{v} & \RAdj I \ar[r]^{\RAdj u}& \RAdj\LAdj 1\\
\RAdj\LAdj 1 \ar[urr]_{\id{\RAdj\LAdj 1}} &&  &}\qquad
\xymatrix{I\ar[drr]_{\id{I}}\ar[r]^{u}&\LAdj1\ar[r]^{\LAdj v}&\LAdj\RAdj I\ar[d]^{\counit_I} \\
& & I}\]

and the following inequalities on the fibres:

\[\xymatrix{
\aDoc A \times \aDoc B \ar@{}[rdd]|{\le} \ar[r]^{\bullet_{A,B}} \ar[d]_{\RAdjLift_A\times\RAdjLift_B} & \aDoc(A\otimes B) \ar[dd]^{\RAdjLift_{A\otimes B}} \\
\Doc\RAdj A\times \Doc\RAdj B  \ar[d]_{\sqcap_{\RAdj A,\RAdj B}} & \\
\Doc (\RAdj A \times \RAdj B)  & \Doc \RAdj (A\otimes B) \ar[l]_{\DReIdx{\Doc}{\psi_{A,B}}} \\
1 \ar@{}[dr]|{\le} \ar[d]_{\top_1} \ar[r]^{\iota} & \aDoc I \ar[d]^{\RAdjLift_I} \\
\Doc 1  &  \Doc \RAdj I  \ar[l]_{\DReIdx{\Doc}{v}}
\qquad
\xymatrix{
\Doc X \times \Doc Y \ar@{}[ddr]|{\le} \ar[r]^{\sqcap_{X,Y}} \ar[d]_{\LAdjLift_X\times\LAdjLift_Y} & \Doc(X\times Y) \ar[dd]^{\LAdjLift_{X\times Y}} \\
\aDoc\LAdj X\times \aDoc\LAdj Y  \ar[d]_{\bullet_{\LAdj X,\LAdj Y}} & \\
\aDoc (\LAdj X \otimes \LAdj Y) & \aDoc \LAdj (X\times Y) \ar[l]_{\DReIdx{\aDoc}{\phi_{X,Y}}} \\
1 \ar@{}[dr]|{\le} \ar[d]_{\iota} \ar[r]^{\top_1} & \Doc 1 \ar[d]^{\LAdjLift_1} \\
\aDoc I & \aDoc \LAdj 1 \ar[l]_{\DReIdx{\aDoc}{u}}
} \]

From general results about monoidal adjunctions between categories, we know that $u$ and
$\phi$ are (natural) isos. Hence the inequalities on the left-hand side are
equalities, that is, those diagrams commute.

Consider now the doctrine .
By adj-to-modality, there is operator
defined as
$\Lbang = \LAdjLift \cdot (\Doc\unit\op) \cdot \RAdjLift\LAdj\op$.
However, in this richer context, $\aDoc\LAdj\op$ has a richer structure.
First of all has finite products, hence, for each object $X$ in , there are arrows
ζX1 and Δ_XXX×X natural in $X$.
Then, we can define a monoid structure on $\aDoc\LAdj\op X$ as the two composite arrows

\[\xymatrix{1\ar@<-1ex>@/_/[rrr]_-{e_X} \ar[r]^{\iota}&\aDoc I \ar[r]^{\DReIdx{\aDoc}{u^{-1}}}
&\aDoc(\LAdj 1) \ar[r]^{\DReIdx{\aDoc}{\LAdj\zeta_X}} &\aDoc(\LAdj X)}\]

\[\xymatrix@C=7ex{\aDoc(\LAdj X)\times\aDoc(\LAdj X)\ar@<-1ex>@/_/[rrr]_-{\ast_X}
\ar[r]^{\bullet_{\LAdj X,\LAdj X}} & \aDoc (\LAdj X\otimes \LAdj X)
\ar[r]^{\DReIdx{\aDoc}{\phi_{X,X}^{-1}}}
& \aDoc(\LAdj(X\times X)) \ar[r]^{\DReIdx{\aDoc}{\LAdj \Delta_X}} & \aDoc(\LAdj X).}\]

It follows that X,∗_X,e_X is a commutative monoid and that such
structure is preserved by reindexing.
This structure interprets the multiplicative conjunction of linear logic and its unit.
To ensure that $\Lbang$ correctly interprets the “bang” modality of linear logic,
four properties, in addition to those of operators, are required to hold:
for each object $X$ in and $\alpha, \beta  \in \aDoc(\LAdj X)$,

\[\begin{array}{ll@{\qquad}ll}
(1)&\Lbang_X\alpha \order e_X&
(2)&\Lbang_X\alpha \order \Lbang_X\alpha \ast_X \Lbang_X\alpha\\[1ex]
(3)&e_X \order \Lbang_X e_X&
(4)&\Lbang_X \alpha \ast_X \Lbang_X \beta \order \Lbang_X (\alpha \ast_X \beta).
\end{array}\]

* Note that $\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \in \Doc X$, which is
an inf-semilattice with top element $\top_X$, hence
$\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \order \top_X=
\DReIdx{\Doc}{\zeta_X}(\top_1)$, because reindexing preserves the inf-semilattice
Therefore, we get
$\Lbang_X \alpha = \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) \order
\LAdjLift_X(\DReIdx{\Doc}{\zeta_X}(\top_1))=
\DReIdx{\aDoc}{\LAdj\zeta_X}(\LAdjLift_1(\top_1)) = e_X$, by naturality of $\LAdjLift$ and
one of the diagrams above.

* Again, note that $\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \in \Doc X$,
which is an inf-semilattice, hence $\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))
\order \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \Land_X
\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))$.
Since $\pi_i \circ \Delta_X = \id{X}$, using naturality of $\Land$, we get

\[\begin{split}
\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))
&\order \DReIdx{\Doc}{\Delta_X}( \DReIdx{\Doc}{\pi_1}(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) \Land_{X\times X} \DReIdx{\Doc}{\pi_2}(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) ) \\
&= \DReIdx{\Doc}{\Delta_X}( \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \sqcap_{X,X} \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) )
\end{split}\]

Therefore, applying $\LAdjLift_X$ and using one of the diagrams above we get

\[\begin{split}
\Lbang_X\alpha &= \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) \\
&\order \LAdjLift_X(\DReIdx{\Doc}{\Delta_X}( \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \sqcap_{X,X} \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) ) \\
&= \DReIdx{\aDoc}{\LAdj\Delta_X}( \LAdjLift_{X\times X}( \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \sqcap_{X,X} \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) ) ) \\
&= \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) \ast_X \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha))) \\
&= \Lbang_X\alpha \ast_X \Lbang_X\alpha
\end{split}\]

* By one of the diagrams above, naturality of $\LAdjLift$ and the fact that reindexing in $\Doc$ preserves the inf-semilattice structure, we have $e_X = \LAdjLift_X(\top_X)$.
Furthermore, since ,𝕀,() is a 2-arrow in , we get

\[ e_X = \LAdjLift_X(\top_X) \order \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\LAdjLift_X(\top_X)))) = \Lbang_X e_X \]

* Using the diagrams above and the definitions of $\ast_X$ and $\Lbang_X$ we get

\[\begin{split}
\Lbang_X \alpha \ast_X \Lbang_X \beta &= (\LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)))) \ast_X (\LAdjLift_X(\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\beta)))) \\
&= \DReIdx{\aDoc}{\LAdj\Delta_X} (\LAdjLift_{X\times X}(
\DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\alpha)) \sqcap_{X,X} \DReIdx{\Doc}{\unit_X}(\RAdjLift_{\LAdj X}(\beta))
)) \\
&= \LAdjLift_X(\DReIdx{\Doc}{\Delta_X}(\DReIdx{\Doc}{(\unit_X\times\unit_X)}(
\RAdjLift_{\LAdj X}(\alpha) \sqcap_{\RAdj\LAdj X,\RAdj\LAdj X} \RAdjLift_{\LAdj X}(\beta)
)))  \\
&\order \LAdjLift_X(\DReIdx{\Doc}{\Delta_X}(\DReIdx{\Doc}{(\unit_X\times\unit_X)}(
\DReIdx{\Doc}{\psi_{\LAdj X,\LAdj X}}(\RAdjLift_{\LAdj X \otimes\LAdj X}(\alpha \bullet_{\LAdj X,\LAdj X} \beta))
\end{split}\]

From one of the diagrams above, we have $\psi_{\LAdj X,\LAdj X} \circ (\unit_X \times\unit_X) = \RAdj\phi_{X,X}^{-1} \circ \unit_{X\times X}$, hence we get

\[\begin{split}
\Lbang_X \alpha \ast_X \Lbang_X \beta
&\order \LAdjLift_X(\DReIdx{\Doc}{\Delta_X}(\DReIdx{\Doc}{(\unit_X\times\unit_X)}(
\DReIdx{\Doc}{\psi_{\LAdj X,\LAdj X}}(\RAdjLift_{\LAdj X \otimes\LAdj X}(\alpha \bullet_{\LAdj X,\LAdj X} \beta))
)))  \\
&= \LAdjLift_X(\DReIdx{\Doc}{\Delta_X}(\DReIdx{\Doc}{\unit_{X\times X}}(
\DReIdx{\Doc}{\RAdj\phi_{X,X}^{-1}}(\RAdjLift_{\LAdj X \otimes\LAdj X}(\alpha \bullet_{\LAdj X,\LAdj X} \beta))
)))  \\
&= \LAdjLift_X(\DReIdx{\Doc}{\unit_X}(
\RAdjLift_{\LAdj X}(\DReIdx{\aDoc}{\LAdj \Delta_X}(\DReIdx{\aDoc}{\phi_{X,X}^{-1}}(\alpha \bullet_{\LAdj X,\LAdj X} \beta)))
))  \\
&= \Lbang_X(\alpha\ast_X\beta)
\end{split}\]