# Two-dimensional Kripke Semantics I: Presheaves

G. A. Kavvos

(February 2024)

###### Abstract

The study of modal logic has witnessed tremendous development following the
introduction of Kripke semantics. However, recent developments in programming
languages and type theory have led to a second way of studying modalities,
namely through their categorical semantics. We show how the two correspond.

##  1 Introduction

The development of modal logic has undergone many phases [23, 15, 46, 98]. It
is widely accepted that one of the most important developments was the
relational semantics of Kripke [68, 69, 70] [15, §1] [46, §4.8]. Kripke
semantics has proven time and again that it is intuitive and technically
malleable, thereby exerting sustained influence over Computer Science.

However, over the last 30 years another way of studying modalities has
evolved: looking at modal logic through the prism of the _Curry-Howard-Lambek
correspondence_ [72, 93, 99] yields new computational intuitions, often with
surprising applications in both programming languages and formal proof. The
tools of the trade here are type theory and category theory.

Up to now these two ways of looking at modalities have been discussed in
isolation. The purpose of this paper is to establish a connection: I will show
that the Kripke and categorical semantics of modal logic are part of a
_duality_. It is well-known that dualities between Kripke and algebraic
semantics exist: the _Jónsson-Tarski duality_ is one of the cornerstones of
classical modal logic [15, §5]. The main contribution of this paper is to show
that such dualities can be elevated to the level of _proofs_. The punchline is
that a _profunctor_
$R:\mathcal{C}^{\mathsf{op}}\times\mathcal{C}\to\mathbf{Set}$, considered as a
_proof-relevant relation_ on a category $\mathcal{C}$, uniquely corresponds to
a categorical model of modal logic on the category of presheaves on
$\mathcal{C}$.

There are two obstacles to overcome to get to that result. The first is that
we must work over an _intuitionistic_ substrate: most research on types and
categories is forced to do so, for unavoidable reasons [72, §8]. We must
therefore first develop a duality for _intuitionistic modal logic_. However,
there is no consensus on what intuitionistic modal logic is! The problem is
particularly acute in the presence of $\lozenge$ [27]. I will avoid this
problem by making canonical choices at each step. First, I will formulate a
Kripke semantics based on _bimodules_ , i.e. relations that are canonically
compatible with a poset. Then, I will show how _Kan extension_ uniquely
determines two adjoint modalities, $\blacklozenge$ and $\Box$, from any
bimodule. The fact these arise automatically is evidence that they are the
canonical choice of intuitionistic modalities.

The second obstacle stems from considering proofs. The jump from algebraic to
categorical semantics involves adding an extra ‘dimension’ of proofs.
Consequently, in order to re-establish a duality, an additional dimension must
be added to Kripke semantics as well. I call the result a _two-dimensional
Kripke semantics_. Category theorists will find it anticlimactic: it amounts
to the folklore observation that a proof-relevant Kripke semantics is
essentially a semantics in a presheaf category.

Indeed, a sizeable proportion of this paper consists of folklore results that
are well-known to experts. However, many of them are drawn from related but
distinct areas: logic, order theory, category theory, and topos theory. As a
result, it does not appear that all of them are well-known by a _single_
expert. Thus, the synthesis presented here appears to be new.

The results I present in this paper show that there are deep connections
between modal logic and presheaf categories. This is important, as the latter
are ubiquitous in logic and related fields: presheaf models are used in fields
as disparate as categorical homotopy theory [87, 24], type theory [57],
concurrency [65, 21, 22], memory allocation [81, 82], synthetic guarded domain
theory [14], second-order syntax and algebraic theories [34, 53, 35, 36, 37],
higher-order abstract syntax [58], and so on. As a result, the connections
presented here may enable synthetic reasoning _via_ modalities in a variety of
logical settings.

In § 2 I recall the Kripke and algebraic semantics of intuitionistic logic,
and outline the duality between Kripke semantics and certain complete Heyting
algebras, the _prime algebraic lattices_. Then I extend this duality to
intuitionistic modal logic in § 3 by showing how a relation that is
compatible with the intuitionistic order—a bimodule—gives rise to modalities
through Kan extension. In § 4 I add proofs to intuitionistic logic, and
elevate the duality to one between ‘two-dimensional frames’ and presheaf
categories. I then repeat this exercise for intuitionistic modal logic in §
5 by promoting bimodules to profunctors on the relational side, and adding an
adjunction on the categorical side.

For general background in orders please refer to the book by Davey and
Priestley [28]. Given a poset $(D,\sqsubseteq_{D})$ let the _opposite_ poset
$D^{\mathsf{op}}$ be given by reversing the partial order; that is,
$x\sqsubseteq_{D^{\mathsf{op}}}y$ iff $y\sqsubseteq_{D}x$. A _lattice_ has all
finite meets and joins. A _complete lattice_ has arbitrary ones. A complete
lattice is _infinitely distributive_ just if the law
$a\land\bigvee_{i}b_{i}=\bigvee_{i}a\land b_{i}$ holds. Such lattices are
variously called _frames_ , _locales_ , or _complete Heyting algebras_ [61,
76, 84].

##  2 Intuitionistic Logic I

There are many types of semantics for intuitionistic logic, including Kripke,
Beth, topological, and algebraic semantics. Bezhanishvili and Holliday [11]
argue that these form a strict hierarchy, with Kripke being the least general,
and algebraic the most general. I will briefly review the elements of these
extreme points of the spectrum.

The Kripke semantics of intuitionistic logic are given by _Kripke frames_ ,
i.e. partially-ordered sets $(W,\sqsubseteq)$ [23, §2.2]. $W$ is referred to
as the set of _possible worlds_ , and $\sqsubseteq$ as the _information
order_. A world $w\in W$ is a ‘state of knowledge,’ and $w\sqsubseteq v$ means
that moving from $w$ to $v$ potentially entails an increase in the amount of
information.

Let $\textsf{Up}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W$}\mathclose{}{)}}$ be the set of _upper sets_ of $W$, i.e. the subsets
$S\subseteq W$ such that $w\in S$ and $w\sqsubseteq v$ implies $v\in S$. A
_Kripke model_ $\mathfrak{M}=(W,\sqsubseteq,V)$ consists of a Kripke frame
$(W,\sqsubseteq)$ as well as a function
$V:\textsf{Var}\to\textsf{Up}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W$}\mathclose{}{)}}$. The _valuation_ $V$ assigns to each propositional
variable $p\in\textsf{Var}$ an upper set $V(p)\subseteq W$, which is the set
of worlds in which $p$ is true. The idea is that, once a proposition becomes
true, it must remain true as information increases.

We are now able to inductively define a relation $\mathfrak{M},w\vDash\varphi$
with the meaning that $\varphi$ is true in world $w$ of model $\mathfrak{M}$.
The only interesting clause is that for implication:

$\mathfrak{M},w\vDash\varphi\to\psi\
\stackrel{{\scriptstyle\mathclap{\mbox{\tiny def}}}}{{\equiv}}\ \forall
w\sqsubseteq v.\ \mathfrak{M},v\vDash\varphi\text{ implies
}\mathfrak{M},v\vDash\psi$

This definition is famously monotonic: if $\mathfrak{M},w\vDash\varphi$ and
$w\sqsubseteq v$ then $\mathfrak{M},v\vDash\varphi$. Kripke semantics is sound
and complete for intuitionistic logic [23, 15].

The algebraic semantics of intuitionistic logic consist of _Heyting algebras_.
These are lattices such that every map $-\land x:L\to L$ has a right adjoint,
i.e. for $x,y\in L$ there is an element $x\Rightarrow y\in L$ such that
$c\land x\sqsubseteq y$ iff $c\sqsubseteq x\Rightarrow y$. Such lattices are
always distributive. Assuming that one has an interpretation
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle
p$}\mathclose{}{\rrbracket}}\in L$ of each proposition $p$, each formula
$\varphi$ of intuitionistic logic is inductively mapped to an element
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}\in
L$ using the corresponding algebraic structure. I will not expound further on
Heyting algebras; see [23, §7.3] [16, §1.1] [76, §I.8]. But I note that they
are sound and complete for intuitionistic logic.

###  2.1 Prime algebraic lattices

Let $(W,\sqsubseteq)$ be any Kripke frame, and let
$\mathbb{2}{}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\\{0\sqsubseteq 1\\}$. Consider the poset
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ of monotonic functions from $W$ to
$\mathbb{2}$, ordered pointwise. This poset has a number of curious
properties.

First, the monotonicity of $p:W\to\mathbb{2}$ means that if $p(w)=1$ and
$w\sqsubseteq v$, then $p(v)=1$. Hence, the subset
$U\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}p^{-1}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
1$}\mathclose{}{)}}$ of $W$ is an upper set. Conversely, every upper set
$U\subseteq W$ gives rise to a monotonic $p_{U}:W\to\mathbb{2}$ by setting
$p_{U}(w)=1$ if $w\in U$, and $0$ otherwise. Consequently, there is an _order
bijection_

$\textsf{Up}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W$}\mathclose{}{)}}\cong\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$

with the order on $\textsf{Up}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W$}\mathclose{}{)}}$ being inclusion. I will liberally treat upper sets and
elements of $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ as the same, but prefer the latter notation
for reasons that will become clear later.

Second, given any $w\in W$, consider its _principal upper set_
$\mathop{\uparrow}w\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle v\in
W$}\mathrel{{|}}\hbox{$\displaystyle w\sqsubseteq
v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle v\in
W$}\mathrel{{|}}\hbox{$\textstyle w\sqsubseteq
v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle v\in
W$}\mathrel{{|}}\hbox{$\scriptstyle w\sqsubseteq
v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle v\in
W$}\mathrel{{|}}\hbox{$\scriptscriptstyle w\sqsubseteq
v$}\mathclose{}{\\}}}\in\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$. This set consists of worlds with potentially
more information than that found in world $w$. A simple argument shows that
$w\sqsubseteq v$ iff $\mathop{\uparrow}v\subseteq\mathop{\uparrow}w$.111This
is an order-theoretic consequence of the Yoneda lemma. Thus, this gives an
_order embedding_

$\mathop{\uparrow}:W^{\mathsf{op}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$

which can be shown to preserve meets and exponentials.

Third, the poset $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ is a _complete lattice_ : arbitrary joins and
meets are given pointwise. Viewing the elements of
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ as upper sets, these joins and meets
correspond to arbitrary unions and intersections of upper sets, which are also
upper. Moreover, this lattice satisfies the infinite distributive law, so it
is a _complete Heyting algebra_ —synonymously a _frame_ or _locale_ [61, 84].
Given two upper sets $X,Y\subseteq W$ their exponential is given by [29, §1.9]

$X\Rightarrow Y\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle w\in
W$}\mathrel{{|}}\hbox{$\displaystyle\forall w\sqsubseteq v.\ v\in X\text{
implies }v\in Y$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle w\in
W$}\mathrel{{|}}\hbox{$\textstyle\forall w\sqsubseteq v.\ v\in X\text{ implies
}v\in Y$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle w\in
W$}\mathrel{{|}}\hbox{$\scriptstyle\forall w\sqsubseteq v.\ v\in X\text{
implies }v\in Y$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle
w\in W$}\mathrel{{|}}\hbox{$\scriptscriptstyle\forall w\sqsubseteq v.\ v\in
X\text{ implies }v\in Y$}\mathclose{}{\\}}}$

Fourth, the principal upper sets $\mathop{\uparrow}w$ are special, in that
they are _prime_.222Such elements are variously called _completely join-
irreducible_ [86], _supercompact_ [8] [84, §VII.8], _completely (join-)prime_
[100], or simply _join-prime_ [41, §1.3]. An element $d$ of a complete lattice
$L$ is _prime_ just if

$d\sqsubseteq\mathop{\bigsqcup}X\ \text{ implies }\ \exists x\in X.\
d\sqsubseteq x$

This says that $d$ contains a tiny, indivisible fragment of information: as
soon as it approximates a supremum, it must approximate something in the set
that is being upper-bounded. The prime elements of
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ are exactly the principal upper sets
$\mathop{\uparrow}w$ for some $w\in W$.

Fifth, the complete lattice $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ is _prime algebraic_. This means that all its
elements can be reconstructed by ‘multiplying’ or ‘sticking together’ prime
elements. In symbols, a complete lattice $L$ is prime algebraic whenever for
every element $d\in L$ we have

$d=\mathop{\bigsqcup}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle p\in
L$}\mathrel{{|}}\hbox{$\displaystyle p\sqsubseteq d,p\text{ prime
}$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle p\in
L$}\mathrel{{|}}\hbox{$\textstyle p\sqsubseteq d,p\text{ prime
}$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle p\in
L$}\mathrel{{|}}\hbox{$\scriptstyle p\sqsubseteq d,p\text{ prime
}$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle p\in
L$}\mathrel{{|}}\hbox{$\scriptscriptstyle p\sqsubseteq d,p\text{ prime
}$}\mathclose{}{\\}}}$

Such lattices are variously called _completely distributive, algebraic
lattices_ [28, §10.29] or _superalgebraic lattices_ [84, §VII.8]. In fact, it
can be shown that any such lattice is essentially of the form
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$, i.e. a lattice of upper sets; this was shown
by Raney in the 1950s [86], and independently by Nielsen, Plotkin and Winskel
in the 1980s [80]. See the paper by Winskel for the use of prime algebraic
lattices in semantics [100].

Finally, the fact every element can be reconstructed as a supremum of primes
means that it is possible to canonically extend any monotonic $f:W\to
W^{\prime}$ to a monotonic $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}\to W^{\prime}$, as long as
$W^{\prime}$ is a complete lattice. Diagrammatically, in the situation

$W$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}$$W^{\prime}$$\mathop{\uparrow}$$f$$f_{{!}}$$\dashv$${f}^{{\star}}$
(1)

there exists a unique $f_{{!}}$ which preserves all joins and satisfies
$f_{{!}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathop{\uparrow}w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathop{\uparrow}w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathop{\uparrow}w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathop{\uparrow}w$}\mathclose{}{)}}=f(w)$.
It is given by

$f_{{!}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
S$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
S$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
S$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
S$}\mathclose{}{)}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathop{\bigsqcup}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle
f(w)$}\mathrel{{|}}\hbox{$\displaystyle w\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle
f(w)$}\mathrel{{|}}\hbox{$\textstyle w\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle
f(w)$}\mathrel{{|}}\hbox{$\scriptstyle w\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle
f(w)$}\mathrel{{|}}\hbox{$\scriptscriptstyle w\in S$}\mathclose{}{\\}}}$

$f_{{!}}$ is called the _(left) Kan extension_ of $f$ along
$\mathop{\uparrow}$. As $f_{{!}}$ preserves all joins and
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ is complete it has a right adjoint
${f}^{{\star}}$, by the adjoint functor theorem [28, §7.34] [61, §I.4.2]. For
any complete lattice $W^{\prime}$ this situation amounts to a bijection

$\mathrm{Hom}_{\textbf{Pos}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W,W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W,W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W,W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W,W^{\prime}$}\mathclose{}{)}}\cong\mathrm{Hom}_{\textbf{CSLatt}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}},W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}},W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}},W^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}},W^{\prime}$}\mathclose{}{)}}$

where CSLatt is the category of complete lattices and join-preserving maps.

Suppose then that we have a Kripke model $(W,\sqsubseteq,V)$. The construction
given above induces a Heyting algebra
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$. Defining
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle
p$}\mathclose{}{\rrbracket}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}V(p)$ we obtain an algebraic model of intuitionistic logic, which
interprets every formula $\varphi$ as an upper set
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}\in\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$. This is the upper set of worlds in which a
formula is true [23, Theorem 7.20]:

######  Theorem 2.1.

$w\vDash\varphi$ if and only if
$w\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$.

Thus, every Kripke semantics corresponds to a prime algebraic lattice.

######  Remark 2.2.

This shows that a Kripke semantics is a particular kind of algebraic
semantics. Thus, we can deduce the completeness of the latter from the
completeness of the former: if a formula is valid in all Heyting algebras, it
must be valid in all prime algebraic lattices, and hence valid in all Kripke
semantics. If the Kripke semantics is complete, then the formula must be
provable. Therefore, the algebraic semantics is then complete as well.

The opposite direction—viz. proving the completeness of Kripke semantics from
completeness of the algebraic semantics—cannot be shown constructively. The
reason is that it requires the construction of _prime filters_ , which is a
weak form of choice. I will investigate the details of this mismatch in a
sequel paper.

###  2.2 Morphisms

The simplest kind of morphism between Kripke frames is a _monotonic_ map
$f:W\to W^{\prime}$. Frames and monotonic maps form the category Pos of
posets. Given a monotonic $f:W\to W^{\prime}$ we can define a monotonic
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ by taking $p:W^{\prime}\to\mathbb{2}$ to
$p\circ f:W\to\mathbb{2}$. Viewing the elements of
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}$ as upper sets, $f^{*}$ maps the upper
set $S\subseteq W^{\prime}$ to the set
$\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle v\in
W^{\prime}$}\mathrel{{|}}\hbox{$\displaystyle f(v)\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle v\in
W^{\prime}$}\mathrel{{|}}\hbox{$\textstyle f(v)\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle v\in
W^{\prime}$}\mathrel{{|}}\hbox{$\scriptstyle f(v)\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle v\in
W^{\prime}$}\mathrel{{|}}\hbox{$\scriptscriptstyle f(v)\in
S$}\mathclose{}{\\}}}\subseteq W$, which is upper by the monotonicity of $f$.
$f^{*}$ preserves arbitrary joins and meets. It is thus the morphism part of a
functor
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-,\mathbb{2}$}\mathclose{}{]}}:\textbf{Pos}^{\mathsf{op}}\longrightarrow\textbf{PrAlgLatt}$
to the category PrAlgLatt of prime algebraic lattices and complete lattice
homomorphisms.

Moreover, the functor
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-,\mathbb{2}$}\mathclose{}{]}}$
is an equivalence! By the adjoint functor theorem any complete lattice
homomorphism $f^{*}:L^{\prime}\to L$ has a left and right adjoint:

$L$$L^{\prime}$$f^{*}$$f_{{*}}$$f_{{!}}$

$\dashv$

$\dashv$

(2)

Given a prime algebraic lattice $L$, let
$\textsf{Prm}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
L$}\mathclose{}{)}}\subseteq L$ be the sub-poset of prime elements. It can be
shown that the left adjoint $f_{{!}}$ maps primes to primes [41, Lemma 1.23].
We can thus restrict it to a function
$\textsf{Prm}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
L$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
L$}\mathclose{}{)}}\to\textsf{Prm}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
L^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
L^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
L^{\prime}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
L^{\prime}$}\mathclose{}{)}}$. This defines a functor
$\textsf{Prm}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle-$}\mathclose{}{)}}:\textbf{PrAlgLatt}\longrightarrow\textbf{Pos}^{\mathsf{op}}$
with the property that
$\textsf{Prm}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$}\mathclose{}{)}}\cong W$. All in all, this
amounts to a _duality_

$\textbf{Pos}^{\mathsf{op}}\simeq\textbf{PrAlgLatt}$ (3)

However, monotonic maps are not particularly well-behaved from the perspective
of logic, as they do not preserve nor reflect ‘local’ truth. This is the
privilege of _open maps_.

######  Definition 2.3.

Let $i_{0}:\mathbb{1}\to\mathbb{2}$ map the unique point of
$\mathbb{1}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\\{\ast\\}$ to $0\in\mathbb{2}$. A monotonic map $f:W\to
W^{\prime}$ of Kripke frames is _open_ just when it has the right lifting
property with respect to $i_{0}:\mathbb{1}\to\mathbb{2}$, i.e. when every
commuting diagram of the form

$\mathbb{1}$$\mathbb{2}$$i_{0}$$W$$W^{\prime}$$f$

in Pos has a diagonal filler (dashed) that makes it commute.

In other words, $f$ is open if whenever $f(w)\sqsubseteq v^{\prime}$ there
exists a $w^{\prime}\in W$ with $w\sqsubseteq w^{\prime}$ and
$f(w^{\prime})=v^{\prime}$.333Such morphisms are often called _p-morphisms_
[23, §2.3] or _bounded morphisms_ [15, §2.1]. According to Goldblatt [46] open
maps were introduced by de Jongh and Troelstra [29] in intuitionistic logic,
and by Segerberg [91] in modal logic. More rarely they are called _functional
simulations_ , and led us to bisimulations [90, §3.2]. The name is chosen
because such maps are open with respect to the _Alexandrov topology_ on a
poset, whose open sets are the upper sets [61, §1.8]. Open maps send upper
sets to upper sets [23, Prop. 2.13]. Thus

######  Lemma 2.4.

Let $\mathfrak{M}=(W,\sqsubseteq,V)$ and
$\mathfrak{N}=(W^{\prime},\sqsubseteq,V^{\prime})$ be Kripke models, and
$f:W\to W^{\prime}$ be open. Suppose $V=f^{-1}\circ V^{\prime}$, i.e. $w\in
V(p)$ iff $f(w)\in V^{\prime}(p)$. Then $\mathfrak{M},w\vDash\varphi$ iff
$\mathfrak{N},f(w)\vDash\varphi$.

Write $W\vDash\varphi$ to mean that $(W,\sqsubseteq,V),w\vDash\varphi$ for any
valuation $V$ and $w\in W$. Then

######  Lemma 2.5.

If $f:W\to W^{\prime}$ is open and surjective, then $W\vDash\varphi$ implies
$W^{\prime}\vDash\varphi$.

Recall now the induced map
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ for a monotonic $f:W\to W^{\prime}$. The
following lemma allows us to characterise the openness and surjectivity of $f$
in terms of $f^{*}$.

######  Lemma 2.6.

  1. 1.

$f:W\to W^{\prime}$ is open iff
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ preserves exponentials.

  2. 2.

$f:W\to W^{\prime}$ is surjective iff
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ is injective.

Consequently, the duality (3) may be restricted to two wide subcategories:

$\displaystyle\textbf{Pos}^{\mathsf{op}}_{\text{open}}\simeq\textbf{PrAlgLatt}_{\Rightarrow}$
$\displaystyle\textbf{Pos}^{\mathsf{op}}_{\text{open,surj}}\simeq\textbf{PrAlgLatt}_{\Rightarrow,\text{inj}}$
(4)

The morphisms of the categories to the left of $\simeq$ are open (resp. and
surjective) maps, and the morphisms of the categories to its right are
_complete Heyting homomorphisms_ , i.e. complete lattice homomorphisms that
preserve exponentials (resp. and are injective).

Finally, let us consider the classical case—as a sanity-check. This amounts to
restricting Pos to its subcategory of discrete orders, i.e. $\mathbf{Set}$. In
this case every map is open. The corresponding restriction on the other side
is to the category CABA of _complete atomic Boolean algebras_ , yielding the
usual _Tarski duality_ $\mathbf{Set}^{\mathsf{op}}\simeq\textbf{CABA}$ [67].

###  2.3 Related work

The origins of the construction of a Heyting algebra from a Kripke frame seems
to be lost in the mists of time. The earliest occurrence I have located is in
the book by Fitting [39, §1.6], where it is attributed to an exercise in the
book by Beth [10].

The duality (3) appears to be folklore—folklore enough to be included as an
exercise in new textbooks [41, Ex. 1.3.10]; see also Erné [31]. However, I
have not been able to find any mention of the dualities of (4) in the
literature.

Both the dualities (3) and (4) involve just prime algebraic lattices, which is
a far cry from encompassing all Heyting algebras. It is possible to do so, by
enlarging the category Pos to a class of ordered topological spaces called
_descriptive frames_ [23, §8.4]. The resulting duality is called _Esakia
duality_ [32] [41, §4.6] [12, §2.3].

A survey on dualities for classical modal logic is given by Kishida [67].

##  3 Modal Logic I

The task now is to extend the results of § 2 to _intuitionistic modal
logic_.

There is disagreement on what a minimal intuitionistic modal logic is. This
arises no matter the methodology we choose—be it relational, algebraic, or
proof-theoretic. The situation becomes even more complex if we include a
diamond modality ($\lozenge$): see Das and Marin [27] and Wolter and
Zakharyaschev [103] for a discussion.

In this paper I will adopt the _intuitionistic propositional logic with Galois
connections_ of Dzik, Järvinen, and Kondo [30], for reasons that will become
clear in a moment. This extends intuitionistic logic with modalities
$\blacklozenge$ and $\Box$, and the two inference rules

$\displaystyle\displaystyle{\hbox{\hskip
15.13885pt\vbox{\hbox{\hskip-15.13885pt\hbox{\hbox{$\displaystyle\displaystyle\blacklozenge\varphi\to\psi$}}}\vbox{}}}\over\hbox{\hskip
15.69441pt\vbox{\vbox{}\hbox{\hskip-15.69441pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\to\Box\psi$}}}}}}$
and $\displaystyle\displaystyle{\hbox{\hskip
15.69441pt\vbox{\hbox{\hskip-15.69441pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\to\Box\psi$}}}\vbox{}}}\over\hbox{\hskip
15.13885pt\vbox{\vbox{}\hbox{\hskip-15.13885pt\hbox{\hbox{$\displaystyle\displaystyle\blacklozenge\varphi\to\psi$}}}}}}$

These rules correspond to a _Galois connection_ [28, §7.23], i.e. an
adjunction $\blacklozenge\dashv\Box$ between posets. They imply the
derivability of the following rules, amongst others [30, Prop. 2.1].

$\displaystyle\displaystyle{\hbox{\hskip
11.80551pt\vbox{\hbox{\hskip-11.80551pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\to\psi$}}}\vbox{}}}\over\hbox{\hskip
19.58331pt\vbox{\vbox{}\hbox{\hskip-19.58331pt\hbox{\hbox{$\displaystyle\displaystyle\Box\varphi\to\Box\psi$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
3.27084pt\vbox{\hbox{\hskip-3.27083pt\hbox{\hbox{$\displaystyle\displaystyle\varphi$}}}\vbox{}}}\over\hbox{\hskip
7.15974pt\vbox{\vbox{}\hbox{\hskip-7.15973pt\hbox{\hbox{$\displaystyle\displaystyle\Box\varphi$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
8.88889pt\vbox{\vbox{}\hbox{\hskip-8.88889pt\hbox{\hbox{$\displaystyle\displaystyle\Box\top$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
8.33333pt\vbox{\hbox{\hskip-8.33333pt\hbox{\hbox{$\displaystyle\displaystyle\blacklozenge\bot$}}}\vbox{}}}\over\hbox{\hskip
4.99998pt\vbox{\vbox{}\hbox{\hskip-4.99998pt\hbox{\hbox{$\displaystyle\displaystyle\bot$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
11.80551pt\vbox{\hbox{\hskip-11.80551pt\hbox{\hbox{$\displaystyle\displaystyle\varphi\to\psi$}}}\vbox{}}}\over\hbox{\hskip
18.4722pt\vbox{\vbox{}\hbox{\hskip-18.4722pt\hbox{\hbox{$\displaystyle\displaystyle\blacklozenge\varphi\to\blacklozenge\psi$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
45.83327pt\vbox{\vbox{}\hbox{\hskip-45.83325pt\hbox{\hbox{$\displaystyle\displaystyle\blacklozenge(\varphi\lor\psi)\leftrightarrow\blacklozenge\varphi\lor\blacklozenge\psi$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
47.49994pt\vbox{\vbox{}\hbox{\hskip-47.49992pt\hbox{\hbox{$\displaystyle\displaystyle\Box(\varphi\land\psi)\leftrightarrow\Box\varphi\land\Box\psi$}}}}}}$

The notation of the ‘black diamond’ modality $\blacklozenge$ may appear
unusual. However, I will argue that this logic is, in a way, the canonical
intuitionistic modal logic.

The Kripke semantics of classical modal logic is given by a _modal frame_
$(W,R)$, which consists of a set $W$ and an arbitrary _accessibility relation_
$R\subseteq W\times W$ [15, §1]. If the same set of worlds $W$ is already part
of an intuitionistic Kripke frame $(W,\sqsubseteq)$ we must take care to
ensure that $\sqsubseteq$ and $R$ are _compatible_. There are many
compatibility conditions that one can consider [85] [92, §3.3]. However, I
will take a hint from the category theory literature, and seek a canonical
definition of what it means for a relation to be compatible with a poset.

Recall that relations can be presented as functions $R:W\times W\to\mathbb{2}$
which map a pair of worlds $(w,v)$ to $1$ iff $w\mathbin{R}v$. I will ask that
$R$ is such function, but with a twist:

######  Definition 3.1.

A _bimodule_ $R:W_{1}\relbar\joinrel\mapstochar\joinrel\rightarrow W_{2}$ is a
monotonic map $R:W_{1}^{\mathsf{op}}\times W_{2}\to\mathbb{2}$.

Thus, a relation $R\subseteq W_{1}\times W_{2}$ is a bimodule just if
$w^{\prime}\sqsubseteq w\mathbin{R}v\sqsubseteq v^{\prime}$ implies
$w^{\prime}\mathbin{R}v^{\prime}$. This means that $R$ can absorb changes in
information on either side: contravariantly on the first component, and
covariantly on the second. This is a standard, minimal way to define what it
means to be ‘a relation in Pos.’ It is strongly reminiscent of bimodules in
abstract algebra.

We can then define a _modal Kripke frame_ $(W,\sqsubseteq,R)$ to be a Kripke
frame $(W,\sqsubseteq)$ equipped with a bimodule
$R:W\relbar\joinrel\mapstochar\joinrel\rightarrow W$. A _modal Kripke model_
$\mathfrak{M}=(W,\sqsubseteq,R,V)$ adds to this a function
$V:\textsf{Var}\to\textsf{Up}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
W$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
W$}\mathclose{}{)}}$. We extend $\mathfrak{M},w\vDash\varphi$ to modal
formulae:

$\displaystyle\mathfrak{M},w\vDash\blacklozenge\varphi\ $
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{\tiny def}}}}{{\equiv}}\
\exists v.\ v\mathbin{R}w\text{ and }\mathfrak{M},v\vDash\varphi$
$\displaystyle\mathfrak{M},w\vDash\Box\varphi\ $
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{\tiny def}}}}{{\equiv}}\
\forall v.\ w\mathbin{R}v\text{ implies }\mathfrak{M},v\vDash\varphi$

There are a number of things to note about this definition. First, there is a
deep duality between the clauses: not only do we exchange $\forall$ for
$\exists$, but we also flip the variance of $R$. As a result, $\blacklozenge$
uses the relation in the _opposite variance_ to the more traditional
$\lozenge$ modality (hence the change in notation). Second, the clause for the
$\Box$ modality is the traditional one; some streams of work on intuitionistic
modal logic adopt a slightly different one [85, 92], which is equivalent to
this in the presence of the bimodule condition. Finally, this definition is
monotonic: the bimodule conditions on $R$ suffice to show that if
$\mathfrak{M},w\vDash\varphi$ and $w\sqsubseteq v$ then
$\mathfrak{M},v\vDash\varphi$. Dzik et al. [30, §5] prove that this semantics
is sound and complete.

The algebraic semantics of this logic is given by a Heyting algebra $H$
equipped with two monotonic maps $\blacklozenge,\Box:H\to H$ which form an
adjunction $\blacklozenge\dashv\Box$, i.e. a Galois connection. Dzik et al.
[30, §4] prove that this semantics is also sound and complete.

We are now in a position to relate the Kripke and algebraic semantics of this
intuitionistic modal logic. Let $(W,\sqsubseteq,R)$ be a modal Kripke frame,
and consider the map $\lambda
R:W^{\mathsf{op}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ obtained by cartesian closure of Pos. This map
takes $w\in W$ to the upper set
$\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle v\in
W$}\mathrel{{|}}\hbox{$\displaystyle
w\mathbin{R}v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle v\in
W$}\mathrel{{|}}\hbox{$\textstyle
w\mathbin{R}v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle v\in
W$}\mathrel{{|}}\hbox{$\scriptstyle
w\mathbin{R}v$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle
v\in W$}\mathrel{{|}}\hbox{$\scriptscriptstyle
w\mathbin{R}v$}\mathclose{}{\\}}}$ of worlds accessible from $w$. Putting
$\lambda R$ in (1) we obtain through Kan extension the diagram

$W^{\mathsf{op}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$$\mathop{\uparrow}$$\lambda
R$$\blacklozenge_{R}$$\dashv$$\Box_{R}$ (5)

where we write $\blacklozenge_{R}$ for $\lambda R_{{!}}$ and $\Box_{R}$ for
${\lambda R}^{{\star}}$. It can be shown that these maps are given by

$\displaystyle\blacklozenge_{R}(S)$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle w\in
W$}\mathrel{{|}}\hbox{$\displaystyle\exists v.\ v\mathbin{R}w\text{ and }v\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle w\in
W$}\mathrel{{|}}\hbox{$\textstyle\exists v.\ v\mathbin{R}w\text{ and }v\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle w\in
W$}\mathrel{{|}}\hbox{$\scriptstyle\exists v.\ v\mathbin{R}w\text{ and }v\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle w\in
W$}\mathrel{{|}}\hbox{$\scriptscriptstyle\exists v.\ v\mathbin{R}w\text{ and
}v\in S$}\mathclose{}{\\}}}$ $\displaystyle\Box_{R}(S)$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle w\in
W$}\mathrel{{|}}\hbox{$\displaystyle\forall v.\ w\mathbin{R}v\text{ implies
}v\in S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle w\in
W$}\mathrel{{|}}\hbox{$\textstyle\forall v.\ w\mathbin{R}v\text{ implies }v\in
S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle w\in
W$}\mathrel{{|}}\hbox{$\scriptstyle\forall v.\ w\mathbin{R}v\text{ implies
}v\in S$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle w\in
W$}\mathrel{{|}}\hbox{$\scriptscriptstyle\forall v.\ w\mathbin{R}v\text{
implies }v\in S$}\mathclose{}{\\}}}$

Thus, any bimodule $R$ defines an adjunction $\blacklozenge_{R}\dashv\Box_{R}$
on $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$. Correspondingly, any adjunction
$\blacklozenge\dashv\Box$ on $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ yields a monotonic map
$\blacklozenge\circ\mathop{\uparrow}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle-$}\mathclose{}{)}}:W^{\mathsf{op}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$, which uniquely corresponds to a bimodule
$W^{\mathsf{op}}\times W\to\mathbb{2}$ by the cartesian closure of Pos.

Thus, starting from a bimodule, i.e. a relation that is compatible with the
information order, we have canonically obtained a model of intuitionistic
modal logic on $\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ through Kan extension:
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$ is a complete Heyting algebra, and we define
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}=\blacklozenge_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$
and
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}=\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$.
We immediately obtain a modal analogue to Theorem 2.1:

######  Theorem 3.2.

For any modal formula $\varphi$, $w\vDash\varphi$ if and only if
$w\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$.

###  3.1 Morphisms

We define a category Bimod with bimodules
$R:W_{1}\relbar\joinrel\mapstochar\joinrel\rightarrow W_{2}$ as objects. A
_bimodule morphism_ from $R:W_{1}\relbar\joinrel\mapstochar\joinrel\rightarrow
W_{2}$ to
$R^{\prime}:W^{\prime}_{1}\relbar\joinrel\mapstochar\joinrel\rightarrow
W^{\prime}_{2}$ is a pair $(f,g)$ of monotonic maps $f:W_{1}\to
W^{\prime}_{1}$ and $g:W_{2}\to W^{\prime}_{2}$ such that $R(w,v)\sqsubseteq
R^{\prime}(f(w),g(v))$. Stated in terms of relations, it must be that
$w\mathbin{R}v$ implies $f(w)\mathbin{R^{\prime}}g(v)$.

We define the subcategory EBimod to consist of (endo)bimodules
$R:W\relbar\joinrel\mapstochar\joinrel\rightarrow W$ and pairs of maps
$(f,f)$. Thus, objects are bimodules on a single poset $W$, and morphisms are
monotonic maps $f:W\to W^{\prime}$ that preserve the relation, i.e.
$w\mathbin{R}v$ implies $f(w)\mathbin{R}f(v)$. In other words, the objects of
EBimod are modal Kripke frames, and the morphisms are monotonic, relation-
preserving maps.

Recall the adjunctions and modalities induced by a monotonic $f:W\to
W^{\prime}$:

$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W,\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W,\mathbb{2}$}\mathclose{}{]}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
W^{\prime},\mathbb{2}$}\mathclose{}{]}}$$f^{*}$$f_{{*}}$$f_{{!}}$

$\dashv$

$\dashv$

$\Box_{R}$$\Box_{R^{\prime}}$ (6)

######  Lemma 3.3.

$f:W\to W^{\prime}$ is a morphism of bimodules $f:R\to R^{\prime}$ iff
$f^{*}\Box_{R^{\prime}}\subseteq\Box_{R}f^{*}$.

This constitutes a duality

$\textbf{EBimod}^{\mathsf{op}}\simeq\textbf{PrAlgLattO}$ (7)

where PrAlgLattO is the category with objects $(L,\Box_{L})$, where $L$ is a
prime algebraic lattice and $\Box_{L}:L\to L$ is an operator that preserves
all meets. By the adjoint functor theorem, such operators always have a left
adjoint $\blacklozenge_{L}:L\to L$. Thus, this category contains algebraic
models of intuitionistic modal logic (but not all of them). By the preceding
section each such adjunction corresponds uniquely to a bimodule. The morphisms
of PrAlgLattO are complete lattice homomorphisms $h:L\to L^{\prime}$ such that
$h\Box_{L}\sqsubseteq\Box_{L^{\prime}}h$. By the preceding lemma they
correspond precisely to morphisms of bimodules.

However, as with monotone maps, morphisms of bimodules do not preserve local
truth; for that we need a notion of _modally open_ maps.

######  Definition 3.4.

Let $(W,\sqsubseteq,R)$ and $(W^{\prime},\sqsubseteq,R^{\prime})$ be modal
Kripke frames. A bimodule morphism $f:R\to R^{\prime}$ is _modally open_ just
if whenever $f(w)\mathbin{R^{\prime}}v$ then there exists a $w^{\prime}\in W$
with $w\mathbin{R}w^{\prime}$ and $f(w^{\prime})\sqsubseteq v$.

This is similar to Definition 2.3, but ever so slightly weaker: instead of
requiring $f(w^{\prime})=v^{\prime}$, it requires that the information in
$f(w^{\prime})$ can be increased to $v^{\prime}$. Like Definition 2.3, it can
also be written homotopy-theoretically, but that requires some ideas from
double categories that are beyond the scope of this paper. We have the
analogous result about preservation of truth:

######  Lemma 3.5.

Let $\mathfrak{M}=(W,\sqsubseteq,R,V)$ and
$\mathfrak{N}=(W^{\prime},\sqsubseteq,R^{\prime},V^{\prime})$ be modal Kripke
models, $f:W\to W^{\prime}$ be open and modally open, and $V=f^{-1}\circ
V^{\prime}$. Then $\mathfrak{M},w\vDash\varphi$ iff
$\mathfrak{N},f(w)\vDash\varphi$.

######  Lemma 3.6.

Let $f:W\to W^{\prime}$ be open, modally open, and surjective. If
$W\vDash\varphi$ then $W^{\prime}\vDash\varphi$.

The following result relates the modal openness of $f$ to $f^{*}$.

######  Lemma 3.7.

$f:R\to R^{\prime}$ is modally open iff $\Box_{R}f^{*}=f^{*}\Box_{R^{\prime}}$
iff $f_{{!}}\blacklozenge_{R}=\blacklozenge_{R^{\prime}}f_{{!}}$.

Thus, the duality (7) may be restricted to dualities between wide
subcategories:

$\displaystyle\textbf{EBimod}^{\text{op}}_{\text{moo}}\simeq\textbf{PrAlgLattO}_{\Rightarrow{}o}$
$\displaystyle\textbf{EBimod}^{\text{op}}_{\text{moo,
surj}}\simeq\textbf{PrAlgLattO}_{\Rightarrow{}o,\text{inj}}$ (8)

The morphisms to the left of $\simeq$ are open and modally open (resp. and
surjective); and the to the right of it preserve exponentials and commute with
operators (resp. and are injective).

Let us consider the restriction of this duality to the classical setting—as a
sanity check. A bimodule on a discrete poset is just a relation on a set. The
corresponding restriction on the right is to CABAs with operators, and
complete homomorphisms which commute with operators. We thus obtain the
_Thomason duality_
$\textbf{MFrm}^{\text{op}}_{\text{open}}\simeq\textbf{CABAO}$ between Kripke
frames and modally open maps on the left, and CABAs with operators to the
right [96, 67].

###  3.2 Related work

Many works have presented a Kripke semantics for intuitionistic modal logic.
All such semantics assume two accessibility relations: a preorder for the
intuitionistic dimension, and a second relation for the modal dimension. What
varies is their _compatibility conditions_.

The first work to present such a semantics appears to be that of Fischer Servi
[38]. One of the required compatibility conditions is $(\sqsubseteq)\circ
R\subseteq R\circ(\sqsubseteq)$. This is weaker than having a bimodule, but
sufficient to prove soundness.

The first work to recognise the importance of bimodules was Sotirov’s 1979
thesis. His results are summarised in a conference abstract [94, §4]: they
include the completeness of a minimal intuitionistic modal logic with a
$\Box$, the K axiom, and the necessitation rule. Božić and Došen [19] repeat
the study for the same logic, but for a semantics based on the Fischer Servi
compatibility conditions. However, they note that their completeness proof
actually constructs half a bimodule (a ‘condensed’ relation). They also point
out that bimodules, which they call ‘strictly condensed’ relations, are sound
and complete for their logic. Wolter and Zakharyaschev [101, §2] argue that
bimodule and Fischer Servi semantics are equi-expressive.

Plotkin and Stirling [85] attempt to systematise the Kripke semantics of
intuitionistic modal logic. Their frame conditions allow ‘transporting a modal
relation upwards’ along any potential increases of information on either side.
This paper and all its descendants—notably the thesis of Simpson [92,
§3.3]—adopt a different satisfaction clause for $\Box$ which uses both
$\sqsubseteq$ and $R$. In the presence of the bimodule conditions this
satisfaction clause is equivalent to the classical one, which I use here.

The bimodule condition and the _complex algebra_ construction (or fragments
thereof) have made scattered appearances in the literature: in the early work
of Sotirov [94] and Božić and Došen [19]; in the work of Wolter and
Zakharyaschev [102, 101, 103], Hasimoto [54, §4], and Orłowska and Rewitzky
[83]; and of course in Dzik et al. [30, §7]. With the exception of the last
one, none of these references discuss the $\blacklozenge$ modality. Moreover,
in none of these references are the categorical aspects of this construction
discussed.

As mentioned before, dualities between frames and algebras have played a
significant role in modal logic. Thomason [96] and Goldblatt [45] also
considered morphisms of frames, respectively obtaining _Thomason duality_ and
(categorical) _Jónsson-Tarski duality_ between descriptive frames and Boolean
Algebras with Operators (BAOs) [46, §6.5]. Kishida [67] surveys a number of
dualities for classical modal logic.

The duality (7) is stated by Gehrke [40, Thm. 2.5] who attributes it to
Jónnson [64], even though no such theorem appears in that paper.

The dualities of (8) are the direct intuitionistic analogues to that of
Thomason. I have not been able to find them anywhere in the literature.

According to the extensive survey of Menni and Smith [78], the idea that the
commonly-used modalities $\Box$ and $\lozenge$ are often part of adjunctions
$\blacklozenge\dashv\Box$ and $\lozenge\dashv\blacksquare$ is implicitly
present throughout the development of modal logic. However, these were not
made explicit in a logic until the 2010s, when they appeared in the work of
Dzik et al. [30] and Sadrzadeh and Dyckhoff [89]. The same perspective plays a
central rôle in the exposition of Kishida [67].

The $\blacklozenge$ modality has appeared before in _tense logics_ as a ‘past’
modality [33, 47].

##  4 Intuitionistic Logic II

In the rest of this paper we will _categorify_ [7] the notion of Kripke
semantics. The main idea is to replace posets by categories, so that the order
$w\sqsubseteq v$ is replaced by a morphism $w\to v$. As there might be
multiple morphisms $w\to v$, this allows the recording of not just the fact
$v$ may signify more information than $w$, but also the _manner_ in which it
does so. The reflexivity and transitivity of the poset are then replaced by
the identity and composition laws of the category. This adds a dimension of
_proof-relevance_ to Kripke semantics.

A corresponding change in our algebraic viewpoint will be that of replacing
the set $\mathbb{2}$ of truth values with the category $\mathbf{Set}$. This is
a classic Lawverean move [73]. Notice that this is lopsided, as is usual in
intuitionistic logic: while the falsity $0$ is only represented by one value,
viz. the empty set, the truth $1$ can be represented by any non-empty set $X$.
The elements of $X$ can be thought of as a _proofs_ of a true statement.

Let us then trade the frame $(W,\sqsubseteq)$ for an arbitrary category
$\mathcal{C}$. It remains to define what it means to have a _proof_ that the
formula $\varphi$ holds at a world $w\in\mathcal{C}$. We denote the set of all
such proofs by
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}$.
Assuming we are given a set
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle
p$}\mathclose{}{\rrbracket}}_{w}$ for each proposition $p$ and world $w$, here
is a first attempt:

$\displaystyle\begin{aligned}
\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\bot$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\bot$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\bot$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\bot$}\mathclose{}{\rrbracket}}_{w}&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\emptyset&\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\top$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\top$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\top$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\top$}\mathclose{}{\rrbracket}}_{w}&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\\{\ast\\}&\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}_{w}&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}\times\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\psi$}\mathclose{}{\rrbracket}}_{w}&\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\lor\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\lor\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\lor\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\lor\psi$}\mathclose{}{\rrbracket}}_{w}&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}+\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\psi$}\mathclose{}{\rrbracket}}_{w}\end{aligned}$
$\displaystyle\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}_{w}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v:\mathcal{C}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v:\mathcal{C}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v:\mathcal{C}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v:\mathcal{C}$}\mathclose{}{)}}\to\mathrm{Hom}_{\mathcal{C}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w,v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w,v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w,v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w,v$}\mathclose{}{)}}\to\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}\to\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\psi$}\mathclose{}{\rrbracket}}_{v}$

where for a family of sets $\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B_{a}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B_{a}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B_{a}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B_{a}$}\mathclose{}{)}}_{a\in A}$ we let

$\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
a:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
a:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
a:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
a:A$}\mathclose{}{)}}\to B_{a}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\{}\hbox{$\displaystyle
f:A\to\bigcup_{a\in
A}B_{a}$}\mathrel{{\mathchoice{\bigg{|}}{\bigg{|}}{\big{|}}{|}}}\hbox{$\displaystyle\forall
a\in A.f(a)\in
B_{a}$}\mathclose{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\}}}{\mathopen{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\{}\hbox{$\textstyle
f:A\to\bigcup_{a\in
A}B_{a}$}\mathrel{{\mathchoice{\bigg{|}}{\bigg{|}}{\big{|}}{|}}}\hbox{$\textstyle\forall
a\in A.f(a)\in
B_{a}$}\mathclose{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\}}}{\mathopen{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\{}\hbox{$\scriptstyle
f:A\to\bigcup_{a\in
A}B_{a}$}\mathrel{{\mathchoice{\bigg{|}}{\bigg{|}}{\big{|}}{|}}}\hbox{$\scriptstyle\forall
a\in A.f(a)\in
B_{a}$}\mathclose{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\}}}{\mathopen{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\{}\hbox{$\scriptscriptstyle
f:A\to\bigcup_{a\in
A}B_{a}$}\mathrel{{\mathchoice{\bigg{|}}{\bigg{|}}{\big{|}}{|}}}\hbox{$\scriptscriptstyle\forall
a\in A.f(a)\in
B_{a}$}\mathclose{{\mathchoice{\bigg{missing}}{\bigg{missing}}{\big{missing}}{missing}}}{\\}}}$

This closely follows the usual Kripke semantics, but adds proofs. For example,
a proof in
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi_{1}\land\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi_{1}\land\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi_{1}\land\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi_{1}\land\varphi_{2}$}\mathclose{}{\rrbracket}}_{w}$
is a pair $(x,y)$ of a proof
$x\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi_{1}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi_{1}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi_{1}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi_{1}$}\mathclose{}{\rrbracket}}_{w}$
and a proof
$y\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi_{2}$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi_{2}$}\mathclose{}{\rrbracket}}_{w}$.
Similarly, a proof
$F\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}_{w}$
is a function which maps a proof of ‘increase in information’ $f:w\to v$ to a
function
$F(v)(f):\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}\to\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\psi$}\mathclose{}{\rrbracket}}_{v}$.
In turn, this function maps proofs in
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}$
to proofs in
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\psi$}\mathclose{}{\rrbracket}}_{v}$.

To show that this definition is monotonic we have to demonstrate it on proofs:
given a proof
$x\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}$
and a morphism $f:w\to v$ we have to define a proof $f\cdot
x\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}$.
Assuming that we are given this operation for propositions, we can extend it
by induction; e.g.

$\begin{array}[]{lllll}f\cdot(x,y)&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}&(f\cdot x,f\cdot
y)&\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\land\psi$}\mathclose{}{\rrbracket}}_{v}\\\
f\cdot F&\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}&(z:\mathcal{C})\mapsto(g:\mathrm{Hom}_{\mathcal{C}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v,z$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v,z$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v,z$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v,z$}\mathclose{}{)}})\mapsto(x:\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{z})\mapsto
F(z)(g\circ
f)(x)&\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}_{v}\end{array}$

Moreover, this definition is compatible with $\mathcal{C}$, in the sense that
$g\cdot(f\cdot x)=(g\circ f)\cdot x$ and $\textsf{id}_{w}\cdot x=x$. We thus
obtain a (covariant) _presheaf_
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}:\mathcal{C}\longrightarrow\mathbf{Set}$
for each formula $\varphi$.

It is well-known that the proofs of intuitionistic logic form a _bicartesian
closed category_ (biCCC), i.e. a category with finite (co)products and
exponentials [71]. A biCCC can be seen as a categorification of a Heyting
algebra: formulae are objects of the category, and proofs are morphisms. We
will not expound on this further; see [72, 26, 4].

It should therefore be the case that the semantics described above form a
biCCC. Indeed, it is a well-known fact of topos theory that the _category of
presheaves_
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
is a biCCC. In fact, the construction of exponentials [76, §I.6] reveals that
our definition above is deficient: we should restrict
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi\to\psi$}\mathclose{}{\rrbracket}}_{w}$
to contain only those functions $F$ that satisfy a _naturality condition_ ,
i.e. those which for any $f:w\to v_{1}$, $g:v_{1}\to v_{2}$, and
$x\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v_{1}}$
satisfy

$g\cdot F(v_{1})(f)(x)=F(v_{2})(g\circ f)(g\cdot x)$

From this point onwards I will identify two-dimensional Kripke semantics with
categorical semantics in a category of presheaves
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$.

###  4.1 Presheaf categories

The category
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
of covariant presheaves is eerily similar to prime algebraic lattices. In a
sense they are just the same; but, having traded $\mathbb{2}$ for
$\mathbf{Set}$, they have become proof-relevant.

First, letting
$P\in\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$,
an element $x\in P(w)$ is a proof that $P$ holds at a ‘world’
$w\in\mathcal{C}$. A morphism $f:w\to v$ of $\mathcal{C}$ then leads to a
proof $f\cdot x\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}P(f)(x)\in P(v)$ that $P$ holds at $v$. Thus, the presheaf $P$ is
very much like an upper set.

Second, the _representable presheaves_
$\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathrm{Hom}_{\mathcal{C}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w,-$}\mathclose{}{)}}:\mathcal{C}\to\mathbf{Set}$ are the proof-relevant
analogues of the principal upper set. By the Yoneda lemma they constitute an
_embedding_

$\mathbf{y}:\mathcal{C}^{\mathsf{op}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$

which moreover preserves limits and exponentials [4].

Third, the category
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
is both complete and cocomplete, with limits and colimits computed pointwise
[76, §I]. It is also ‘distributive’ in an appropriate sense [3, §3.3], which
makes it into a _Grothendieck topos_. It is thus a cartesian closed category,
with exponential

$(P\Rightarrow Q)(w)\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
P\times\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}},Q$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
P\times\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}},Q$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
P\times\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}},Q$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
P\times\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}},Q$}\mathclose{}{)}}$

which is essentially the two-dimensional semantics of implication I gave
above.

Fourth, the representables
$\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$ are special, in that they are _tiny_ [104].

######  Definition 4.1.

An object $d\in\mathcal{D}$ is _tiny_ just if
$\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
d,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
d,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
d,-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
d,-$}\mathclose{}{)}}:\mathcal{D}\to\mathbf{Set}$ preserves colimits.444In the
literature this property is often referred to as _external tininess_ (cf.
internal tininess).

Tininess is a proof-relevant version of primality: it implies that for any
$f:w\to{\varinjlim}_{i}\,v_{i}$ there exists an $i$ such that $f$ is equal to
the composition of a morphism $w\to v_{i}$ with the injection
$v_{i}\to{\varinjlim}_{i}\,v_{i}$. By the Yoneda lemma it follows that all
representables $\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$ are tiny, as they satisfy the above definition for
$\mathcal{D}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
and $d\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$.

Fifth, the so-called _co-Yoneda lemma_ [75, §III.7] shows that every
$P\in\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
is a colimit of representables. This means that it can be reconstructed by
sticking together tiny elements:

$P\cong{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$

Like with prime algebraic lattices, there is a converse to this result: every
category which is generated by sticking together tiny elements is in fact a
presheaf category:

######  Theorem 4.2 (Bunge [20]).

A category which is cocomplete and strongly generated by a small set of tiny
objects is equivalent to
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
for some small category $\mathcal{C}$.

A textbook presentation of this result can be found in the book by Kelly [66,
§5.5].

Finally, the fact every element can be reconstructed as a colimit of
representables means that it is possible to uniquely extend any functor
$f:\mathcal{C}\longrightarrow\mathcal{D}$ to a cocontinuous functor
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbb{2}$}\mathclose{}{]}}\longrightarrow\mathcal{D}$,
as long as $\mathcal{D}$ is cocomplete. Diagrammatically, in the situation

$\mathcal{C}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}$$\mathcal{D}$$\mathbf{y}$$f$$f_{{!}}$$\dashv$${f}^{{\star}}$
(9)

there exists an essentially unique cocontinuous $f_{{!}}$ with
$f_{{!}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{}{)}}=f(w)$. It is given by

$f_{{!}}\mathchoice{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\displaystyle{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\textstyle{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\scriptstyle{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\scriptscriptstyle{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
w$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
w$}\mathclose{}{)}}$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}{\varinjlim}_{(w,x)\in\mathop{\textsf{el}}P}\,f(w)$

$f_{{!}}$ is called the _left Kan extension_ of $f$ along $\mathbf{y}$. It has
a right adjoint ${f}^{{\star}}$ which is explicitly given by
${f}^{{\star}}(d)\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
f(-),d$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
f(-),d$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
f(-),d$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
f(-),d$}\mathclose{}{)}}$. This amounts to an isomorphism

$\mathrm{Hom}_{\mathbf{Cat}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathcal{C},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathcal{C},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathcal{C},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathcal{C},\mathcal{D}$}\mathclose{}{)}}\cong\mathrm{Hom}_{\textbf{Cocont}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}},\mathcal{D}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C}^{\mathsf{op}},\mathbf{Set}$}\mathclose{}{]}},\mathcal{D}$}\mathclose{}{)}}$

where $\mathbf{Cat}$ is the category of categories, and Cocont is the category
of cocomplete categories and cocontinuous functors: see [4, Prop. 9.16] [88,
Cor. 6.2.6, Rem. 6.5.9] and [75, § X.3, Cor. 2] [66, Th. 4.51].

Table 1: Categorification of Kripke semantics poset | category
---|---
monotonic map | functor
upper sets | presheaves
principal upper set | representable presheaf
prime element | tiny object
prime algebraic lattice | presheaf category
bimodule | profunctor

All in all, presheaf categories are the categorification of prime algebraic
lattices.

###  4.2 Cauchy-complete and spacelike categories

Replacing posets with categories does not come for free: the extra dimension
of morphisms leads to situations that have no analogues in poset. Some of
these are problematic when thinking of $\mathcal{C}$ as a two-dimensional
Kripke frame. Perhaps the most bizarre is the presence of _idempotents_ , i.e.
morphisms $e:w\to w$ with the property that $e\circ e=e$. Such morphisms
represent a non-trivial increase in information which confusingly leaves us in
the same world.

The presence of idempotents causes issues. For example, recall that, in prime
algebraic lattices, primes and principal upper sets coincide. The astute
reader will have noticed we did _not_ claim the analogous result in presheaf
categories: tiny objects are not necessarily representable in
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$.
For that, we need $\mathcal{C}$ to be _Cauchy-complete_ [18, 17].

######  Definition 4.3.

A category is _Cauchy-complete_ just if every idempotent splits, i.e. if every
idempotent is equal to $s\circ r$ for a section-retraction pair $s$ and $r$.

Note that every complete category is Cauchy-complete, including $\mathbf{Set}$
and
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$.

This leads us to another troublesome situation, namely that of having section-
retraction pairs, i.e. $s:w\to v$ and $r:v\to w$ with $r\circ
s=\textsf{id}_{w}$. In this case $w$ and $v$ contain no more information than
each other, but are not isomorphic. We may ask that this does not arise.

######  Definition 4.4.

A category satisfies the _Hemelaer condition_ [55, Prop. 5.8] just if every
section-retraction pair is an isomorphism.

Combining these two conditions is equivalent to the following definition.

######  Definition 4.5.

A category is _spacelike_ if every idempotent is an identity.

Lawvere has identified this condition as having particular importance in
recognising petit toposes [77]. We will not use it much, as it restricts the
dualities we wish to develop.

In the rest of this paper we will assume that our base categories
$\mathcal{C}$ are Cauchy-complete, so that tiny objects coincide with
representables.

###  4.3 Morphisms

The simplest kind of morphism between categories is a functor. Given a
$f:\mathcal{C}\longrightarrow\mathcal{D}$ we can define a functor
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
that takes $P:\mathcal{D}\longrightarrow\mathbf{Set}$ to $P\circ
f:\mathcal{C}\longrightarrow\mathbf{Set}$. This functor has left and right
adjoints, which are given by Kan extension [62, A4.1.4]:

$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}$$f^{*}$$f_{{*}}$$f_{{!}}$

$\dashv$

$\dashv$

(10)

Therefore $f^{*}$ preserves all limits and colimits, i.e. it is
(co)continuous. In short, the presheaf construction gives a functor
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-,\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-,\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-,\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-,\mathbf{Set}$}\mathclose{}{]}}:\textbf{Cat}_{\text{cc}}^{\mathsf{op}}\longrightarrow\textbf{PshCat}$,
where $\textbf{Cat}_{\text{cc}}$ is the category of small Cauchy-complete
categories and functors; and PshCat is the category of presheaf categories
(over Cauchy-complete base categories) and (co)continuous functors.

Moreover, this functor is an equivalence. Given a presheaf category we can
obtain its base as the subcategory of tiny objects [62, A1.1.10]. But how can
we extract $f:\mathcal{C}\longrightarrow\mathcal{D}$ from any (co)continuous
functor
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$?
First, as presheaf categories are locally presentable, the adjoint functor
theorem implies that $f^{*}$ has left and right adjoints, as in (10) [1,
§1.66]. This gives what topos theorists call an _essential geometric
morphism_. Johnstone [62, §A4.1.5] shows that every such morphism is induced
by a $f:\mathcal{C}\longrightarrow\mathcal{D}$, as $f_{{!}}$ preserves
representables (when $\mathcal{D}$ is Cauchy-complete). We thus obtain a
duality

$\textbf{Cat}^{\text{op}}_{\text{cc}}\simeq\textbf{PshCat}$ (11)

As with posets, functors here fail to preserve truth; for that we need a
notion of openness.

######  Definition 4.6.

$f:\mathcal{C}\longrightarrow\mathcal{D}$ is _open_ just if
$f^{*}:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
preserves exponentials.

######  Lemma 4.7.

If $f:\mathcal{C}\longrightarrow\mathcal{D}$ is open then there is a natural
isomorphism
$\theta_{w}:\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}\cong\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{f(w)}$.

Definition 4.6 is somewhat underwhelming, as it does not give explicit
conditions that one can check—unlike Definition 2.3. However, obtaining such a
description appears difficult.

Some information may be gleaned by considering
$(f^{*},f_{{*}}):\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{D},\mathbf{Set}$}\mathclose{}{]}}$
as a _geometric morphism_. Such a morphism is _open_ [60] [63, C3.1] just if
both the canonical maps $f^{*}(c\Rightarrow d)\to f^{*}(c)\Rightarrow
f^{*}(d)$ and $f^{*}(\Omega)\to\Omega$ are monic. Johnstone [63, C3.1] proves
that $(f^{*},f_{{*}})$ is open iff for any $\beta:f(w)\to v^{\prime}$ in
$\mathcal{D}$ there exists an $\alpha:w\to w^{\prime}$ in $\mathcal{C}$ and a
section-retraction pair $s:v^{\prime}\to f(w^{\prime})$ and
$r:f(w^{\prime})\to v^{\prime}$ with $s\circ\beta=f(\alpha)$. This
superficially seems like a categorification of Definition 2.3. However, it
only guarantees that $f^{*}$ is _sub-cartesian-closed_ , whereas we need an
isomorphism for Lemma 4.7 to hold.

A stronger condition is to ask that $(f^{*},f_{{*}})$ be _locally connected_ ,
i.e. that $f^{*}$ commute with dependent products [63, C3.3]. All such
morphisms are open geometric morphisms. This is stronger than what we need,
but sufficient conditions on $f$ can be given [63, C3.3.8].

Finally, an even stronger condition is to ask that $(f^{*},f_{{*}})$ be
_atomic_ , i.e. that $f^{*}$ is a _logical_ functor. This means it preserves
exponentials and the subobject classifier [63, A2.1, C3.5]. All atomic
geometric morphisms are locally connected. This is again stronger than what we
need, and a characterisation in terms of $f$ is elusive: see MathOverflow
[95].

It is easier to characterise when $(f^{*},f_{{*}})$ is a _surjective geometric
morphism_ , i.e. when $f^{*}$ is faithful [62, A2.4.6]. This happens exactly
when $f$ is _retractionally surjective_ , i.e. whenever every
$d\in\mathcal{D}$ is the retract of $f(c)$ for some $c\in\mathcal{C}$ [62,
A2.4.7]. If $\mathcal{D}$ satisfies the Hemelaer condition this reduces to $f$
being essentially surjective.

Write $\mathcal{C}\vDash\varphi$ to mean that
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{w}$
is non-empty for any $w\in\mathcal{C}$ and any interpretation of
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle
p$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle
p$}\mathclose{}{\rrbracket}}$.

######  Lemma 4.8.

Let $f:\mathcal{C}\to\mathcal{D}$ be open and retractionally surjective. If
$\mathcal{C}\vDash\varphi$ then $\mathcal{D}\vDash\varphi$.

We may thus restrict the duality (11) to dualities

$\displaystyle\textbf{Cat}^{\text{op}}_{\text{cc,
open}}\simeq\textbf{PshCat}_{\Rightarrow}$
$\displaystyle\textbf{Cat}^{\text{op}}_{\text{cc, open,
rs}}\simeq\textbf{PshCat}_{\Rightarrow,\text{f}}$ (12)

In the first instance the category to the left of $\simeq$ is that of small
Cauchy-complete categories and open functors; and to the right of $\simeq$ it
is presheaf categories and (co)complete, cartesian closed functors. In the
second instance the category to the left of $\simeq$ is that of small Cauchy-
complete categories and open, retractionally surjective functors; and to the
right of $\simeq$ it is presheaf categories and (co)complete, faithful,
cartesian closed functors.

##  5 Modal Logic II

To make a two-dimensional Kripke semantics for modal logic we have to
categorify relations. We took the first step by considering bimodules, i.e.
information-order-respecting relations. The second step can be taken by
replacing $\mathbb{2}$ with $\mathbf{Set}$; this leads us to the notion of a
relation between categories, also known as a _profunctor_ or _distributor_ [9]
[17, §7].

######  Definition 5.1.

A _profunctor_
$R:\mathcal{C}\relbar\joinrel\mapstochar\joinrel\rightarrow\mathcal{D}$ is a
functor $R:\mathcal{C}^{\mathsf{op}}\times\mathcal{D}\to\mathbf{Set}$.

To formulate a two-dimensional Kripke semantics for modal logic we replace
modal Kripke frames with a small Cauchy-complete category $\mathcal{C}$ with
an (endo)profunctor
$R:\mathcal{C}^{\mathsf{op}}\times\mathcal{C}\to\mathbf{Set}$. To obtain the
modalities we can now play the same trick: putting $\lambda
R:\mathcal{C}^{\mathsf{op}}\to\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
into (9) we canonically obtain the following diagram by Kan extension:

$\mathcal{C}^{\mathsf{op}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$$\mathbf{y}$$\lambda
R$$\blacklozenge_{R}$$\dashv$$\Box_{R}$ (13)

Conversely, any adjunction $\blacklozenge\dashv\Box$ on
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
corresponds to the (endo)profunctor on $\mathcal{C}$ given by
$(c_{1},c_{2})\mapsto\mathrm{Hom}_{\mathcal{C}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
c_{1},\blacklozenge c_{2}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
c_{1},\blacklozenge c_{2}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
c_{1},\blacklozenge
c_{2}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
c_{1},\blacklozenge c_{2}$}\mathclose{}{)}}$.

We may then define
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\blacklozenge_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}:\mathcal{C}\longrightarrow\mathbf{Set}$
and
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}\stackrel{{\scriptstyle\mathclap{\mbox{\tiny
def}}}}{{=}}\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}:\mathcal{C}\longrightarrow\mathbf{Set}$.
It is worth unfolding what a proof of $\Box\varphi$ at a world $w$ is to
obtain an explicit description:

$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\Box\varphi$}\mathclose{}{\rrbracket}}_{w}=\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\Box_{R}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}(w)=\mathrm{Hom}_{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\lambda
R(w),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\lambda
R(w),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\lambda
R(w),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\lambda
R(w),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}=\mathrm{Hom}_{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
R(w,-),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
R(w,-),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
R(w,-),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
R(w,-),\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}$
(14)

Thus, a proof that $\varphi$ holds at $w$ is a natural transformation
$\alpha:R(w,-)\Rightarrow\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$.
This has the expected shape of Kripke semantics for $\Box$: for each
$v\in\mathcal{C}$ and proof $x\in R(w,v)$ that $v$ is accessible from $w$ it
gives us a proof
$\alpha_{v}(x)\in\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}$
that $\varphi$ holds at $v$.

It is a little harder to see what a proof of $\blacklozenge\varphi$ at a world
$w$ is. It becomes more perspicuous if we use the coend formula for the left
Kan extension [74, §2.3]:

$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\blacklozenge\varphi$}\mathclose{}{\rrbracket}}=\lambda
R_{{!}}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}\cong\int^{v\in\mathcal{C}}\mathrm{Hom}_{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v$}\mathclose{}{)}},\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v$}\mathclose{}{)}},\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v$}\mathclose{}{)}},\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{y}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
v$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
v$}\mathclose{}{)}},\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$}\mathclose{}{)}}\times\lambda
R(v)\cong\int^{v\in\mathcal{C}}\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}_{v}\times
R(v,-)$ (15)

Hence, a proof that $\blacklozenge\varphi$ holds at $w$ consists of a world
$v\in\mathcal{C}$, a proof that $R(v,w)$, and a proof that $\varphi$ holds at
$v$—which is exactly what one would expect. The difference is that the coend
quotients some of these pairs according to the action of $\mathcal{C}$. See
Mac Lane and Moerdijk [76, §VII.2] for a textbook exposition on why this is a
tensor product of
$\mathchoice{\mathopen{}{\llbracket}\hbox{$\displaystyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\textstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptstyle\varphi$}\mathclose{}{\rrbracket}}{\mathopen{}{\llbracket}\hbox{$\scriptscriptstyle\varphi$}\mathclose{}{\rrbracket}}$
and $\lambda R$.

How well does this fit the categorical semantics of modal logic? As with
intuitionistic modal logic, there is also a number of proposals of what that
might be. A fairly recent idea is to define it as the semantics of a _Fitch-
style calculus_ , as studied by Clouston [25]. This is exactly a bicartesian
closed category $\mathcal{C}$ equipped with an adjunction:

$\mathcal{C}$$\mathcal{C}$$\Box$$\blacklozenge$

$\dashv$

(16)

The left adjoint $\blacklozenge$ is often written as lock. It does not
commonly appear as a modality, but as an operator on contexts that corresponds
to ‘opening a box’ in Fitch-style natural deduction [59, §5.4]. The modality
$\Box$ is a right adjoint, so that it automatically preserves all limits,
including products. This idea has proven remarkably robust: variations on it
have worked well for modal dependent type theories [13, 51, 52, 50, 49]. The
fact that an adjunction on a presheaf category corresponds precisely to a two-
dimensional Kripke semantics is further evidence that this is the correct
notion of categorical model of modal logic.

Finally, note that (14) and (15) look suspiciously similar to the modal
structure of Normalization-by-Evaluation models for modal type theories. This
is explicitly visible in the paper by Valliappan et al. [97, §2], and also
implicitly present in the paper by Gratzer [48].

###  5.1 Morphisms

Define the category Prof to have as objects profunctors. A morphism
$(f,g,\alpha):R\to S$ from
$R:\mathcal{C}\relbar\joinrel\mapstochar\joinrel\rightarrow\mathcal{D}$ to
$S:\mathcal{C}^{\prime}\relbar\joinrel\mapstochar\joinrel\rightarrow\mathcal{D}^{\prime}$
consists of functors $f:\mathcal{C}\longrightarrow\mathcal{C}^{\prime}$ and
$g:\mathcal{D}\longrightarrow\mathcal{D}^{\prime}$, and a natural
transformation $\alpha:R(-,-)\Rightarrow
S\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
f(-),g(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
f(-),g(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
f(-),g(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
f(-),g(-)$}\mathclose{}{)}}$. The subcategory EProf consists of
endoprofunctors
$R:\mathcal{C}\relbar\joinrel\mapstochar\joinrel\rightarrow\mathcal{C}$, and
triples of the form $(f,f,\alpha)$. I will synecdochically refer to
$\alpha:R(-,-)\Rightarrow S(f(-),f(-))$ as a morphism of EProf. Thus, objects
are two-dimensional Kripke frames, and morphisms are functors that proof-
relevantly preserve the relation.

######  Lemma 5.2.

Morphisms of endoprofunctors $\alpha:R(-,-)\Rightarrow S(f(-),f(-))$ are in
bijection with natural transformations
$\gamma:f^{*}\Box_{S}\Rightarrow\Box_{R}f^{*}$.

######  Proof 5.3.

Unfolding the definitions,
$\gamma:\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
S(f(-),-),-$}\mathclose{}{)}}\Rightarrow\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
R(-,-),f^{*}(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
R(-,-),f^{*}(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
R(-,-),f^{*}(-)$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
R(-,-),f^{*}(-)$}\mathclose{}{)}}$. As $f_{{!}}\dashv f^{*}$ this is exactly a
transformation $\mathrm{Hom}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
S(f(-),-),-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
S(f(-),-),-$}\mathclose{}{)}}\Rightarrow\mathrm{Hom}\mathchoice{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\displaystyle
f_{{!}}R(-,-),-$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\textstyle
f_{{!}}R(-,-),-$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\scriptstyle
f_{{!}}R(-,-),-$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}{\mathopen{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{(}\hbox{$\scriptscriptstyle
f_{{!}}R(-,-),-$}\mathclose{{\mathchoice{\Big{missing}}{\Big{missing}}{\big{missing}}{missing}}}{)}}$.
By the Yoneda lemma, any such transformation arises by precomposition with a
unique transformation $f_{{!}}R(-,-)\Rightarrow S(f(-),-)$. By $f_{{!}}\dashv
f^{*}$ again, this uniquely corresponds to a transformation
$\alpha:R(-,-)\Rightarrow f^{*}S(f(-),-)=S(f(-),f(-))$.

We thus obtain a duality

$\textbf{EProf}^{\text{op}}_{\text{cc}}\simeq\textbf{PshCatO}$ (17)

where PshCatO is the category of presheaf categories
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$
equipped with a continuous
$\Box:\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}\longrightarrow\mathchoice{\mathopen{}{[}\hbox{$\displaystyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle\mathcal{C},\mathbf{Set}$}\mathclose{}{]}}$.
Note that, as presheaf categories are locally finitely presentable, $\Box$
always has a left adjoint $\blacklozenge$. Thus, the objects are categorical
models of modal logic. Morphisms are pairs $(f,\gamma)$ of a (co)continuous
$f:\mathcal{C}\longrightarrow\mathcal{D}$ and a natural transformation
$\gamma:f^{*}\Box\Rightarrow\Box f^{*}$.

As before, open functors do not preserve truth; for that we need a notion of