# Stack Representation of Finitely Presented Heyting Pretoposes I

Lingyuan Ye

###### Abstract

This is the first of a series of papers on stack representation of finitely
presented Heyting pretoposes. In this paper, we provide the first step by
constructing a $(2,1)$-site, which can be thought of as the site of finite
Kripke frames, such that the $(2,1)$-category of finitely presented Heyting
pretoposes contravariantly embeds into the $(2,1)$-topos of stacks on this
$(2,1)$-site. This provides an entry point to use categorical and higher
sheaf-theoretic tools to study the properties of certain classes of
intuitionistic first-order theories.

###### Contents

  1. 1 Introduction
  2. 2 Duality for Finite Pretoposes
    1. 2.1 Finite Categories as Models
    2. 2.2 Duality for Finite Pretoposes
    3. 2.3 Geometric Surjection
    4. 2.4 Open Functors and Duality of Finite Heyting Pretoposes
  3. 3 Stack Representation
    1. 3.1 The $(2,1)$-Site of Finite Kripke Frames
    2. 3.2 Stack Representation of Heyting Pretoposes
    3. 3.3 From Gros to Petit

##  1 Introduction

In this paper we are interested in stack representation of finitely presented
Heyting pretoposes. We shall comment immediately that by finitely presentable,
we mean those Heyting pretoposes which are _complete_ w.r.t. _finite models_
on _finite Kripke frames_. Typical examples include those equivalent to a
finite quotient of the free Heyting pretopos generated by a finite pretopos. A
pretopos is _finite_ if its _category of models_ is essentially finite.

In particular, this notion does _not_ coincide with those Heyting pretoposes
generated by a first-order intuitionisitic theory with finitely many non-
logical symbols and finitely many axioms. In general, such first-order
intuitionistic theories will not be complete w.r.t. the particular class of
finite models we are interested in. Towards the end of this section, we will
comment on the reason why we are interested in this restricted class of
Heyting pretoposes.

Categorically, this work can be thought of as a _categorification_ of the
sheaf representation of the category of finitely presented Heyting algebras
described in the book [7]. We give a brief overview below.

The starting point of the sheaf representation of finitely presented Heyting
algebras is the _duality_ of finite distributive lattices and finite Heyting
algebras as follows,

${\mathbf{HA}^{\operatorname{op}}_{\mathrm{f}}}$${\mathbf{Por}_{\mathrm{f}}}$${\mathbf{DL}^{\operatorname{op}}_{\mathrm{f}}}$${\mathbf{Pos}_{\mathrm{f}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

where $\mathbf{DL}_{\mathrm{f}}$, $\mathbf{HA}_{\mathrm{f}}$ are the
categories of finite distributive lattices and finite Heyting algebras,
respectively. Notice that $\mathbf{HA}_{\mathrm{f}}$ is a wide subcategory of
$\mathbf{DL}_{\mathrm{f}}$, since any finite distributive lattice is
automatically Heyting. Their corresponding dual categories are
$\mathbf{Pos}_{\mathrm{f}}$, the category of finite posets, and
$\mathbf{Por}_{\mathrm{f}}$, the wide subcategory of
$\mathbf{Pos}_{\mathrm{f}}$ with _open_ functions, or _p-morphisms_ as denoted
by modal logicians.

Concretely, the duality between finite posets and finite distributive lattices
takes any poset $L$ to the distributive lattice $D(L)$ of upward closed
subsets of $L$, while $L$ will be isomorphic to the poset of _models_ of
$D(L)$. Since any finite distributive lattice is also a Heyting algebra, for
any finitely presented Heyting algebra $H$ we may look the poset of its
$L$-valued models $\mathbf{HA}_{\mathrm{fp}}(H,D(L))$ for a finite poset $L$.
In particular, a Heyting algebra morphism from $H$ to $D(L)$ is exactly the
same as a Krpike-model on $L$ for the intuitionistic propositional theory
encoded by $H$.

This gives us a _presheaf_ on $\mathbf{Por}_{\mathrm{f}}$,

$\mathbf{HA}_{\mathrm{fp}}(H,D(-)):\mathbf{Por}_{\mathrm{f}}^{\operatorname{op}}\to\mathbf{Set},$

which turns out to be a sheaf for a suitable Grothendieck topology $J$ on
$\mathbf{Por}_{\mathrm{f}}$. The topology $J$ on $\mathbf{Por}_{\mathrm{f}}$
is in fact the _canonical_ one, with covering families being jointly
surjective maps. This gives us a sheaf representation functor

$\Phi_{-}:\mathbf{HA}_{\mathrm{fp}}^{\operatorname{op}}\rightarrowtail\mathbf{Sh}(\mathbf{Por}_{\mathrm{f}},J),$

which intuitively embeds any finitely presented Heyting algebra to the sheaf
of its models on finite Kripke frames.

As is well-known, categorification is an art rather than a science. But if we
are careful enough, there will still be tracible links. Recall the indexation
for higher categories, e.g. see [15]. For
$r,s\in\overline{\mathbb{N}}=\mathbb{N}\cup\left\\{\infty\right\\}$, an
$(r,s)$-category is a higher category where $k$-cells are trivial for all
$k>r$ and $j$-cells are inverible for all $j>s$. An $(n,n)$-category in this
sense is the same as an $n$-category; an $(n,0)$-category is usually called an
$n$-groupoid; while an $(n,n+1)$-category can be identified with an $n$-poset.

In this way, Heyting algebras can be thought of as $(0,1)$-Heyting pretoposes,
and in full generality the collection of Heyting algebras should organise
themselves into a $(1,2)$-category. However, the ordinary sheaf representation
chooses a $1$-site $\mathbf{Por}_{\mathrm{f}}$, which is just an ordinary
category, and embeds the underlying $1$-category $\mathbf{HA}_{\mathrm{fp}}$
of finitely presented Heying algebras into the category of $1$-sheaves on this
$1$-site. The underlying $1$-category $\mathbf{HA}_{\mathrm{fp}}$ actually
suffices for the purpose of studying propositional intuitionistic logic. For
instance, the interpolation property and Beth definability for propositional
intuitionistic logic are concerned with _pushout_ squares in
$\mathbf{HA}_{\mathrm{fp}}$, e.g. see [16], rather than lax or oplax colimits
computed in the $(1,2)$-category of Heyting algebras.

Now the categorification we are working towards concerns increasing the first
entry. We intend to study the collection of $(1,1)$-Heyting pretoposes, which
are simply Heyting pretoposes in the usual 1-categorical sense. They organise
themselves into a $2$-category, while we are concerned in providing a stack
representation for its underlying $(2,1)$-category, i.e. the $2$-category of
Heyting pretoposes with Heyting functors and natural _isomorphisms_ between
them. We denote the $(2,1)$-category of finitely presented Heyting pretoposes
as $\mathbf{HPt}_{\mathrm{fp}}$, while the full $2$-category as
$\mathbf{HPretopos}_{\mathrm{fp}}$. Similar convention applies to
$\mathbf{Pt}_{\mathrm{fp}}$ and $\mathbf{Pretopos}_{\mathrm{fp}}$ for
pretoposes, and their finitary versions. Again, for the purpose of studying
the properties of first-order intuitionistic logic,
$\mathbf{HPt}_{\mathrm{fp}}$, rather than $\mathbf{HPretopos}_{\mathrm{fp}}$,
is the right environment we want to work in. For instance, as shown in [17],
the interpolation property of first-order intuitionistic logic is again
concerned with $2$-pushouts in $\mathbf{HPt}$, rather than cocomma squares in
the full $2$-category $\mathbf{HPretopos}$ of Heyting pretoposes.

Thus, our first task in Section 2 is to obtain a categorification of the
duality result for _finite pretoposes_ and _finite Heyting pretoposes_. And it
turns out that, according to our definition, finite pretoposes are again
automatically _Heyting_ , in fact even _toposes_.111In this paper, we will
follow the more traditional usage of the notion of topos to mean _elementary
topos_ , unless otherwise stated. And a similar duality result holds as
indicated below,

${\mathbf{HPretopos}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}}$${\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

Here ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is the $2$-category of _finite Cauchy complete
categories_ , and
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is its wide subcategory with a suitable notion of
_open_ functors. This gives us a duality for the full 2-categorical version,
and for us latter we will restrict to their underlying $(2,1)$-categories to
construct a $(2,1)$-site.

After obtaining the duality, in Section 3 we proceed to construct the stack
representation for the $(2,1)$-category $\mathbf{HPt}_{\mathrm{fp}}$. We
similarly choose the underlying $(2,1)$-category to be
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, the underlying $(2,1)$-category of
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ which is dual to $\mathbf{HPt}_{\mathrm{f}}$. By
putting a suitable Grothendieck topology $J$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, we once more obtain a stack
representation $2$-functor

$\Phi_{-}:\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}\rightarrowtail\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J).$

In this paper, our use of the term stack follows the traditional convention,
i.e. it indicates suitable _groupoid_ valued pseudo-functors. In other words,
we have embedded the opposite $(2,1)$-category of $\mathbf{HPt}_{\mathrm{fp}}$
into the $(2,1)$-category of $(2,1)$-sheaves on the $(2,1)$-site
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}},J)$.

We will denote the above representation functor as the _gros_ representation
functor. It also generates a _petit_ representation functor for a single
finitely presented Heyting pretopos $\mathcal{H}$, via the embedding

$\mathcal{H}\rightarrowtail\mathcal{H}/\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}},$

sending each $\varphi\in\mathcal{H}$ to the pullback onto the slice category
over it $\mathcal{H}\to\mathcal{H}/\varphi$. Composed with the gros
representation, this gives us a representation of $\mathcal{H}$ as follows,

$\mathcal{H}\rightarrowtail\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)/\Phi_{\mathcal{H}}.$

Section 3.3 will be devoted to the study of this induced petit representation.
In fact, there we will show that the image of $\mathcal{H}$ under the petit
representation restricts to _discrete opfibrations_ over $\Phi_{\mathcal{H}}$
in the $(2,1)$-category
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$, and the induced functor

$\mathcal{H}\rightarrowtail\mathbf{opDisc}(\Phi_{\mathcal{H}})$

will be a _Heyting_ functor. In this sense, the internal structure of the
$(2,1)$-topos
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$ realises the Heyting structure of
_every_ finitely presented Heyting pretoposes.

One of the reasons to develop the ordinary sheaf representation of Heyting
algebras is that, it can be used to show that
$\mathbf{HA}_{\mathrm{fp}}^{\operatorname{op}}$ is itself a _Heyting category_
, by proving $\mathbf{HA}_{\mathrm{fp}}^{\operatorname{op}}$ is closed under
the Heyting operation in $\mathbf{Sh}(\mathbf{Por}_{\mathrm{f}},J)$. As
explained in [7], this implies that propositional intuitionisitic logic has
quantifier elimination for _second-order_ quantifiers which is originally
proven in [18], and that the algebraic theory of Heyting algebras has a model
companion.

Similarly, we expect our stack representation for finitely presented Heyting
algebras to show that $\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}$ will
also be a $(2,1)$-Heyting category. For the notion of higher Heyting
categories, see [20]. In particular, we expect to show that
$\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}$ via this stack representation
is closed under the $(2,1)$-Heyting operations in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$.

The first step towards such a result is to characterise the image of the stack
representation of $\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}$ in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$. In the sequal to this paper, we will
characterise the image of the stack representation functor in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$, by introducing a suitable notion of
_bisimulation_ between models of finitely presented Heyting pretoposes. We
will also show in the sequal that the topology $J$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ exactly encodes this logical information
of bisimulation, and the notion of $J$-stacks is equivalent to a bisimulation-
invariant class of models. Under this notion of bisimulation, we are also
going to characterise the image of the stack representation functor as certain
_finitary_ stacks.

Along with such semantic investigations, we also expect to extract similar
quantifier elimination results of _higher quantifiers_ for this restricted
class of first-order intuitionistic theories in future work. This also
explains our motivation for looking at first-order intuitionistic theories
with strong finite model properties: For a general first-order intuitionistic
theory, if it contains infinite models, then the second-order extension will
in general have _stronger_ expressive power than the first-order fragment.
However, for the restricted class of Heyting pretoposes, such a result is at
least not outright contradictory. And from our limited knowledge, there hasn’t
been an attempt for such a result in the literature.

##  2 Duality for Finite Pretoposes

As mentioned in the introduction, our first objective is to study a suitable
notion of finite pretoposes. For us, the definition that works is the
following:

######  Definition 2.1.

A pretopos is _finite_ iff its category of models is essentially finite, i.e.
equivalent to a finite category.

It is then natural to ask whether all finite categories could be the category
of models of some pretopos. The answer is negative due to the following simple
observation:

######  Lemma 2.2.

For any pretopos $\mathcal{D}$, its category of models
$\mathrm{Mod}(\mathcal{D})$ is closed under filtered colimits in
$[\mathcal{D},\mathbf{Set}]$, thus in particular is Cauchy complete.

###### Proof.

The fact that $\mathrm{Mod}(\mathcal{D})$ is closed under filtered colimits
computed in $[\mathcal{D},\mathbf{Set}]$ is well-known, e.g. see Chapter 5 of
[1]. The splitting of idempotent is in particular a filtered colimit, thus
$\mathrm{Mod}(\mathcal{D})$ must be Cauchy complete. ∎

In fact, for finite categories, Cauchy completeness is the only obstacle, i.e.
all Cauchy complete finite categories can arise as the category of models of a
finite theory. Moreover, we obtain a duality result, where there is an
equivalence

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}\simeq\mathbf{Pretopos}_{\mathrm{f}},$

from the opposite 2-category of all Cauchy complete finite categories, to the
2-category of finite pretoposes. We prove this by proving the following
duality

$\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}\simeq\mathbf{Topos}_{\mathrm{f}},$

where $\mathbf{Topos}_{\mathrm{f}}$ is the 2-category of
$\mathbf{Set}_{\mathrm{f}}$-bounded toposes. The previous duality follows from
this because from Corollary 2.2.23 in [9] we already know that the 2-category
of finite Cauchy complete categories is equivalent to the 2-category of
$\mathbf{Set}_{\mathrm{f}}$-bounded toposes. This latter result can be seen as
a consequence of the following facts:

  * •

There is a general 2-fully faithful embedding of Cauchy complete categories
into toposes with _essential_ geometric morphism,

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}}\mkern
4.0mu}\mkern-4.0mu}{}}\hookrightarrow\mathbf{EssTopos}.$

  * •

In [8], it has shown that any geometric morphism between
$\mathbf{Set}_{\mathrm{f}}$-bounded toposes is _automatically essential_.

  * •

It can be shown that any $\mathbf{Set}_{\mathrm{f}}$-bounded topos is of the
form $\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ for some finite Cauchy complete
category $\mathcal{I}$, by showing that any Grothendieck topology on finite
Cauchy complete categories are so called _rigid_ , thus is of presheaf type.
Again, see Lemma 2.2.21 in [9].

Section 2.1 will first provide an analysis of finite pretoposes, while Section
2.2 proceeds to prove the above mentioned duality result for finite
pretoposes. By the equivalence
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathbf{Topos}_{\mathrm{f}}$, we also study
certain geometric aspects of finite Cauchy complete categories, notably that
of geometric surjections, in Section 2.3, which turns out to be crucial for
the Grothendieck topology we will be constructing in the next section. Finally
in Section 2.4, we restrict the duality for finite pretoposes to one for
finite Heyting pretoposes, and study certain properties of open functors,
again in preparation for the next section.

###  2.1 Finite Categories as Models

To show every Cauchy complete finite category can arise as the category of
models of some theory, the following observation is of vital importance:

######  Lemma 2.3.

For any finite category $\mathcal{I}$, we have a canonical equivalence

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathrm{Ind}(\mathcal{I}),$

where ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is the _Cauchy completion_ of $\mathcal{I}$, and
$\mathrm{Ind}(\mathcal{I})$ is its _ind-completion_.

###### Proof.

This follows from the fact that for a finite category, essentially the only
non-trivial filtered colimit is the splitting of idempotency, thus
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}$ already has all filtered colimits. For a proof, see
[23]. ∎

In particular, Lemma 2.3 implies that if $\mathcal{I}$ is already Cauchy
complete, then $\mathcal{I}\simeq\mathrm{Ind}(\mathcal{I})$. Lemma 2.3 also
allows us to compute the category of points of the copresheaf category on a
finite category:

######  Lemma 2.4.

For any finite category $\mathcal{I}$, there is an equivalence

$\mathbf{Topos}(\mathbf{Set},[\mathcal{I},\mathbf{Set}])\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}.$

###### Proof.

We have the following sequence of equivalences,

$\mathbf{Topos}(\mathbf{Set},[\mathcal{I},\mathbf{Set}])\simeq\mathrm{Flat}(\mathcal{I}^{\operatorname{op}},\mathbf{Set})\simeq\mathrm{Ind}(\mathcal{I})\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}.$

The first equivalence holds by Diaconescu’s theorem; the second equivalence is
well-known; and the last equivalence is by Lemma 2.3. ∎

In particular, this gives us a very simple way of determining what the
classifying pretopos should be for finite categories: Let us write
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ for the functor category
$[\mathcal{I},\mathbf{Set}_{\mathrm{f}}]$,

######  Proposition 2.5.

For any finite category $\mathcal{I}$, we have an equivalence

$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\simeq\mathbf{Set}_{\mathrm{f}}[{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}],$

such that

$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}])\simeq\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}])\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}.$

###### Proof.

It is easy to see that $\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ is exactly the
coherent objects in the Grothendieck topos $[\mathcal{I},\mathbf{Set}]$
because $\mathcal{I}$ is a finite category. Now we have a well-known
equivalence

$[\mathcal{I},\mathbf{Set}]\simeq[{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}},\mathbf{Set}],$

thus the equivalence restricts to their corresponding coherent objects

$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\simeq\mathbf{Set}_{\mathrm{f}}[{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}].$

Furthermore, since the copresheaf topos $[\mathcal{I},\mathbf{Set}]$ is
coherent, its category of points is equivalent to the category of models of
the pretopos $\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$, thus we have

$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}])\simeq\mathbf{Topos}(\mathbf{Set},[\mathcal{I},\mathbf{Set}])\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}.\qed$

Thus for any category $\mathcal{I}$, it embeds into
$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}])\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathcal{I}}\mkern
4.0mu}\mkern-4.0mu}{}}$ as follows: For any $x\in\mathcal{I}$, as a model it
is simply the evaluation functor

$x^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\to\mathbf{Set}_{\mathrm{f}},$

which we view as precomposition with $x:\mathbf{1}\to\mathcal{I}$ where
$\mathbf{1}$ is the terminal category. Since finite limits and colimits are
computed point-wise in $\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$, $x^{*}$
preserves all finite limits and colimits, thus is in particular coherent.
Given $f:x\to y$, this gives a natural transformation

$f:x\to y:\mathbf{1}\to\mathcal{I},$

and by wiskering with $f$ we get a natural transformation

$f^{*}:x^{*}\to y^{*}.$

Furthermore, we can thus show that all finite pretoposes are equivalent to
this form:

######  Corollary 2.6.

Any finite pretopos is equivalent to one of the form
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ for some finite Cauchy complete
category $\mathcal{I}$. In particular, all finite pretoposes are Heyting, and
in fact toposes.

###### Proof.

This follows from Makkai’s conceptual completeness theorem [12]. Let
$\mathcal{D}$ be any finite pretopos with category of models equivalent to
some finite Cauchy complete category $\mathcal{I}$. Then we have an
equivalence between category of models as follows,

$\mathrm{Mod}(\mathcal{D})\simeq\mathcal{I}\simeq\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]),$

which by conceptual completeness provides a syntactic equivalence

$\mathcal{D}\simeq\mathbf{Set}_{\mathrm{f}}[\mathcal{I}].$

Thus all finite pretoposes are of this form. ∎

The above result also essentially appears as exercises in SGA4, see Exercise
3.12 in volume 2 of [2]. There a Grothendieck topos is called _finite_ if it
is equivalent to the category of presheaves on a finite category. This is
consistent with our definition of a finite pretopos, in that Corollary 2.6
implies a pretopos is finite in our sense iff its classifying topos is finite
in the sense of SGA4.

######  Remark 2.7.

From a logical perspective, the pretopos
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ is the classifying theory for flat
functors out of $\mathcal{I}^{\operatorname{op}}$, which can be written down
quite explicitly, e.g. see Chapter 2 of [4]. This is somewhat surprising in
that all coherent first-order theories whose category of models is essentially
finite can be axiomatised in a _uniform_ way.

For any pretopos $\mathcal{D}$ and any model of $\mathcal{D}$

$M:\mathcal{D}\to\mathbf{Set},$

there is also the notion of this particular model $M$ being finite. We say $M$
is _finite_ if it factors through $\mathbf{Set}_{\mathrm{f}}$. For a finite
pretopos, not only its category of models is essentially finite, but all of
its models are also finite:

######  Lemma 2.8.

All models of a finite pretopos are finite.

###### Proof.

By Corollary 2.6, it suffices to consider those toposes of the form
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$. Now notice that
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ is generated by a _countable_ , in
fact finite, theory, thus by Löwenheim–Skolem theorem, if it has an infinite
model then it must have a model of each cardinality, which implies
$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}])$ cannot be essentially
finite. Thus, any model
$M:\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\to\mathbf{Set}$ must be finite. ∎

One may wonder whether the converse of Lemma 2.8 is also true, i.e. if a
pretopos only has finite models, then whether or not it must be finite as
well. The answer to this question is _negative_. Consider the theory
$\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]=[\mathbb{Z},\mathbf{Set}_{\mathrm{f}}]$
where $\mathbb{Z}$ is the integer group considered as a category with one
element. It can be shown that $\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$ is
_categorical_ , i.e. it only has one model upto isomorphism, and in fact we
have an equivalence

$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}])\simeq\widehat{\mathbb{Z}},$

where $\widehat{\mathbb{Z}}$ is the profinite completion of $\mathbb{Z}$,
which is a profinite groupoid with one connected component. A canonical choice
of a model of $\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$ is given by the
forgetful functor

$\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]\to\mathbf{Set},$

which factors through $\mathbf{Set}_{\mathrm{f}}$, thus is finite. This
implies that all models of $\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$ are finite,
because all of them are isomorphic to a finite model. However, the profinite
groupoid $\widehat{\mathbb{Z}}$ is by no means finite, because its morphism
group is uncountable. More generally, for any group $G$, we have the
equivalence

$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[G])\simeq\widehat{G},$

where $\widehat{G}$ is the profinite completion of $G$. And all of the
theories of such form have only finite models, but their category of models is
not necessarily essentially finite. For a reference for these calculations see
[19].

From a logical perspective, the caveat is that a theory might have _countably
many sorts_. For instance, to present $\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$
as the classifying pretopos of a certain coherent theory, we must have
countably many sorts, because there are countably many connected components in
$\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$. Now even though any model of
$\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$ must be finite, there is no bound on
the size of the interpretation of the sorts, i.e. for any $n\in\mathbb{N}$,
there exists a sort of $\mathbf{Set}_{\mathrm{f}}[\mathbb{Z}]$ such that its
size in this model is larger than $n$. Thus, even though this model is finite,
the automorphism group of this model can still be uncountable.

###  2.2 Duality for Finite Pretoposes

Now that we have understood better the class of finite pretoposes, we proceed
further to establish a duality result. The first task is to describe the
functoriality of the construction
$\mathcal{I}\mapsto\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$. For any functor
$A:\mathcal{I}\to\mathcal{J}$ with $\mathcal{I},\mathcal{J}$ finite Cauchy
complete categories, by precomposition we have a functor

$A^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{I}],$

which is coherent because the coherent structure on
$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ and
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ are computed point-wise. Given a
natural transformation

$\eta:A\to B:\mathcal{I}\to\mathcal{J},$

there is an induced natural transformation

$\eta^{*}:A^{*}\to
B^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{I}],$

by wiskering, such that for any $F:\mathcal{J}\to\mathbf{Set}_{\mathrm{f}}$,

$\eta^{*}_{F}=F\eta:FA\to FB$

This thus gives us a 2-functor from the 2-category of finite categories to the
2-category of finite pretoposes,

$\mathbf{Set}_{\mathrm{f}}[-]:{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}\to\mathbf{Pretopos}_{\mathrm{f}}.$

In fact, we have the following diagramme

$\textstyle{{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}}$$\textstyle{\mathbf{Topos}_{\mathrm{f}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

where as mentioned previously, under the same construction the 2-functor

$\mathbf{Set}_{\mathrm{f}}[-]:{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathbf{Topos}_{\mathrm{f}}$

is an equivalence. Hence, we only need to show
$\mathbf{Topos}_{\mathrm{f}}\to\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}$,
by sending a geometric morphism to its inverse image, is also an equivalence.

Notice that by Corollary 2.6, the 2-functor
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\to\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}$
is essentially surjective, thus so is
$\mathbf{Topos}_{\mathrm{f}}\to\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}$.
To show it is an equivalence, we prove it is also 2-fully faithful, which
amounts to prove that any coherent functor between finite pretoposes are in
fact the inverse image part of a geometric morphism. Hence, the crucial part
is to show any coherent functor between
$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ and
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ indeed preserves all finite
_colimits_.

We first compute the subobject lattices in
$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$. For any finite category
$\mathcal{I}$, we will use $D(\mathcal{I})$ to denote the finite distributive
lattice of all upward closed subsets of $\mathcal{I}$. Given a subset $U$ of
objects of $\mathcal{I}$, it is upward closed if for any $x\in U$ and $f:x\to
y$ in $\mathcal{I}$, we also have $y\in U$. Using this notion, it is easy to
see that:

######  Lemma 2.9.

For any finite category $\mathcal{J}$ and
$X\in\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$, there is an isomorphism

$\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]}(X)\cong
D(\smallint\\!\\!_{\mathcal{J}}X).$

where $\smallint\\!\\!_{\mathcal{J}}X$ is the category of elements of $X$.

###### Proof.

We first show the case when $X=1$ is the terminal object in
$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$. In this case, given any subobject
$\sigma\rightarrowtail 1$, there is an associated upward closed subset
$U_{\sigma}$, such that for any $x\in\mathcal{I}$,

$x\in U_{\sigma}\Leftrightarrow\sigma(x)\cong 1.$

It is straight forward to verify that this gives us an isomorphism. For
general $X$, we have the following sequence of isomorphisms,

$\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]}(X)\cong\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]/X}(1)\cong\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[\smallint\\!\\!_{\mathcal{J}}X]}(1)\cong
D(\smallint\\!\\!_{\mathcal{J}}X).$

This completes the proof. ∎

In particular, for any finite category $\mathcal{J}$, Lemma 2.9 implies that
the subobject lattice on $X$ for any
$X\in\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ is a finite distributive lattice,
since $\smallint\\!\\!_{\mathcal{J}}X$ is a finite category. This allows us to
show:

######  Lemma 2.10.

Any coherent functor
$M:\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$
preserves all finite colimits.

###### Proof.

It suffices to show $M$ preserves all coequalisers. Given any coequaliser,
taking a countable union of subobjects can inductively generate an effective
coequaliser that has the same colimit. Since the subobject lattices in
$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ are _finite_ distributive lattices,
such countable unions are in fact finite, thus are preserved under coherent
functors. Of course effective quotients are also preserved by coherent
functors, thus they preserve arbitrary coequalisers. ∎

######  Lemma 2.11.

Any coherent functor from $\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ to
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ is the inverse image part of a
geometric morphism.

###### Proof.

Consider any coherent functor
$A^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$,
we construct its right adjoint $A_{*}$ as follows: For any
$X\in\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$ and $a\in\mathcal{J}$,

$A_{*}X(a)\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{I}](A^{*}\mathsf{y}^{a},X),$

where $\mathsf{y}^{a}$ is the corepresentable on $a\in\mathcal{J}$. We show
that this indeed defines the right adjoint of $A^{*}$: For any
$Y\in\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$ and
$X\in\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$,

$\displaystyle\mathbf{Set}_{\mathrm{f}}[\mathcal{J}](Y,A_{*}X)$
$\displaystyle\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{J}](\underrightarrow{\operatorname{Lim}}_{\mathsf{y}^{a}\to
Y}\mathsf{y}^{a},A_{*}X)$
$\displaystyle\cong\underleftarrow{\operatorname{Lim}}_{\mathsf{y}^{a}\to
Y}\mathbf{Set}_{\mathrm{f}}[\mathcal{J}](\mathsf{y}^{a},A_{*}X)$
$\displaystyle\cong\underleftarrow{\operatorname{Lim}}_{\mathsf{y}^{a}\to
Y}\mathbf{Set}_{\mathrm{f}}[\mathcal{I}](A^{*}\mathsf{y}^{a},X)$
$\displaystyle\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{I}](\underrightarrow{\operatorname{Lim}}_{\mathsf{y}^{a}\to
Y}A^{*}\mathsf{y}^{a},X)$
$\displaystyle\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{I}](A^{*}Y,X)$

The third isomorphism holds due to our definition of $A_{*}X$. Also notice
that the last step uses the fact that $A^{*}$ preserves finite colimits. ∎

As a corollary, we obtain our desired duality result between finite pretoposes
and finite Cauchy complete categories:

######  Theorem 2.12.

There are equivalences of 2-categories as follows

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathbf{Topos}_{\mathrm{f}}\simeq\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}},$

under the construction $\mathbf{Set}_{\mathrm{f}}[-]$.

###### Proof.

As mentioned, we only need to show that the following functor

$\mathbf{Topos}_{\mathrm{f}}\to\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}$

by taking a geometric morphism to its inverse image is an equivalence. This is
a corollary of Lemma 2.11. ∎

One nice thing about showing the above equivalence is that we can now also
compute explicitly what is the left adjoint $A_{!}$ of any coherent functor
between two finite pretoposes, since now we know that any such coherent
functor
$A^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$
is induced by some functor $A:\mathcal{I}\to\mathcal{J}$. Since $A_{!}$ is a
left adjoint, it suffices to know its value on corepresentables:

######  Lemma 2.13.

For any $A:\mathcal{I}\to\mathcal{J}$, for any $x\in\mathcal{I}$ we have

$A_{!}\mathsf{y}^{x}\cong\mathsf{y}^{Ax}.$

###### Proof.

For any $X\in\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$, there is the following
natural isomorphisms

$\mathbf{Set}_{\mathrm{f}}[\mathcal{J}](A_{!}\mathsf{y}^{x},X)\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{I}](\mathsf{y}^{x},A^{*}X)\cong
X(Ax)\cong\mathbf{Set}_{\mathrm{f}}[\mathcal{J}](\mathsf{y}^{Ax},X).$

This implies the two copresheaves are naturally isomorphic. ∎

The previously shown equivalence is indeed a categorification of the
$(0,1)$-level duality between finite posets and finite distributive lattices
in the following sense:

######  Proposition 2.14.

There is a commutative diagramme as follows,

${\mathbf{Pos}_{\mathrm{f}}^{\operatorname{op}}}$${\mathbf{DL}_{\mathrm{f}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}}$${\mathbf{Pretopos}_{\mathrm{f}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$

where the vertical left adjoints are posetal reflection of categories and
localic reflection of pretoposes, respectively.

###### Proof.

For a finite poset $I$, its dual is the distributive lattice $D(I)$ of upward
closed subsets of $I$. For the two equivalences to commute with the two right
adjoint inclusions, we need to show that

$\mathbf{Sh}_{\mathrm{f}}(D(I))\simeq\mathbf{Set}_{\mathrm{f}}[I],$

i.e. the category of finite sheaves on $D(I)$ is equivalent to the presheaf
finite topos $\mathbf{Set}_{\mathrm{f}}[I]$. But this is evident, because any
element in $D(I)$ is a _finite_ join of corepresentable elements, thus the
sheaf condition implies that the value of a sheaf on $D(I)$ is completely
determined by that in $I$. This means that the equivalences commutes with the
right adjoint inclusions, thus they also commutes with the left adjoints,
since they are equivalences, and adjoints are unique upto natural isomorphism.
∎

Another way to look at the above proof if to use our result in Lemma 2.6,
which suggests that the free pretopos generated by $D(I)$ is indeed given by
$\mathbf{Set}_{\mathrm{f}}[I]$, because

$\mathrm{Mod}(\mathbf{Set}_{\mathrm{f}}[I])\simeq I\simeq\mathrm{Mod}(D(I)).$

The above reflection then also implies that, for any Cauchy complete finite
category $\mathcal{I}$, we can compute its localic reflection by computing the
posetal reflection of $\mathcal{I}$. In particular, let $I$ denote its posetal
reflection, then we have

$D(\mathcal{I})\cong\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]}(1)\cong\operatorname{Sub}_{\mathbf{Set}_{\mathrm{f}}[I]}(1)\cong
D(I).$

######  Remark 2.15.

The above equivalence can also be restricted to the Boolean case. It is also
well-known that a topos of the form $\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$
is _Boolean_ iff $\mathcal{I}$ is a groupoid. In particular, if $\mathcal{I}$
is a poset, then it must be discrete. Thus from above we furthermore obtain a
duality for finite Boolean pretoposes and finite Boolean algebras as follows,

${\mathbf{Set}_{\mathrm{f}}^{\operatorname{op}}}$${\mathbf{BA}_{\mathrm{f}}}$${\mathbf{Grpd}_{\mathrm{f}}^{\operatorname{op}}}$${\mathbf{BPretopos}_{\mathrm{f}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$

###  2.3 Geometric Surjection

To restrict the duality
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}$
to one for finite _Heyting_ pretoposes, we need a convenient geometric
language on the dual side of finite Cauchy complete categories. Recall the
following equivalence

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}\simeq\mathbf{Topos}_{\mathrm{f}}.$

This way, a lot of geometric properties in the domain of toposes can be
transferred to the world of finite Cauchy complete categories. For any
property $P$ of geometric morphisms in topos theory, we say a functor
$A:\mathcal{I}\to\mathcal{J}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is $P$, iff its induced geometric morphism
$A:\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$
is $P$.

For us, the most crucial geometric notion is that of a _surjection_. Recall a
geometric morphism $A$ is a surjection iff its inverse image $A^{*}$ is
faithful, and we would like to characterise surjections by viewing $A$ as
functors $A:\mathcal{I}\to\mathcal{J}$. For this we use the extensive results
in [5]:

######  Lemma 2.16.

$A:\mathcal{I}\to\mathcal{J}$ is a surjection iff it is essentially surjective
upto retracts, i.e. for any $a\in\mathcal{J}$, it is a retract in
$\mathcal{J}$ of $Ax$ for some $x\in\mathcal{I}$.

###### Proof.

Note that the geometric morphism
$A:\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{J}]$
is induced by viewing the opposite functor
$A^{\operatorname{op}}:\mathcal{I}^{\operatorname{op}}\to\mathcal{J}^{\operatorname{op}}$
as a _comorphism of site_. By Proposition 7.1 in [5], since
$A^{\operatorname{op}}$ preserves covers, $A$ is a surjection iff
$A^{\operatorname{op}}$ is _dense_ , iff for any $a\in\mathcal{J}$, there
exists some $x\in\mathcal{I}$ and an arrow $s:a\to Ax$ such that $1_{a}$
factors through $s$. This is equivalent to say that there exists $r:Ax\to a$
with $rs=1_{a}$, i.e. $A$ is essentially surjective upto retracts. ∎

Recall that we have an orthogonal factorisation system in
$\mathbf{Topos}_{\mathrm{f}}$ consisting of geometric inclusions and geometric
surjections. By Lemma 2.16, this also translates to the following orthogonal
factorisations system $(E,M)$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$:

$\displaystyle E$ $\displaystyle=\text{essentially surjective upto retracts},$
$\displaystyle M$ $\displaystyle=\text{fully faithful whose image is closed
under retracts}$

It is well-known that these form an orthogonal factorisation system on
$\mathbf{Cat}$, e.g. see [6]. It also restricts one to
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, since for any functor $A:\mathcal{I}\to\mathcal{J}$
in ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, the factorisation is given by
$\mathcal{I}\to{{\hat{\rule{0.0pt}{5.16663pt}\smash{\operatorname{img}A}\mkern
4.0mu}\mkern-4.0mu}{}}\to\mathcal{J}$, where
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\operatorname{img}A}\mkern
4.0mu}\mkern-4.0mu}{}}$ is the retract closure of $\operatorname{img}A$ in
$\mathcal{J}$, which is again Cauchy complete. However, the nice thing in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is that the image of a full functor is automatically
closed under retract:

######  Lemma 2.17.

Let $A:\mathcal{I}\to\mathcal{J}$ be a full functor in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$. Then the image of $A$ is closed under retracts in
$\mathcal{J}$, i.e. for any retract $r:Ax\rightleftarrows a:s$ with
$x\in\mathcal{I}$ and $a\in\mathcal{J}$ there exists some $y\in\mathcal{I}$
that $Ay\cong a$.

###### Proof.

Suppose we have a retract pair in $\mathcal{J}$

$r:Ax\rightleftarrows a:s.$

Let $g=sr:Ax\to Ax$, and let $\mathcal{I}_{g}(x,x)$ denote the set of
endomorphisms on $x$ in $\mathcal{I}$ that is mapped to $g$. By fullness,
$\mathcal{I}_{g}(x,x)$ is non-empty. Since $g$ is idempotent, we know that
$\mathcal{I}_{g}(x,x)$ is a multiplicative closed set in $\mathcal{I}(x,x)$.
Since $\mathcal{I}_{g}(x,x)$ is finite, every orbit in $\mathcal{I}_{g}(x,x)$
must be finite, thus there exists an idempotent map $f:x\to x$ which is mapped
to $g$. Since $\mathcal{I}$ is Cauchy complete, the splitting of $f$, which is
a pair $x\rightleftarrows y$, exists in $\mathcal{I}$. Since splitting of
idempotency is an absolute colimit, it is preserved by $A$, hence we must have
$Ay\cong a$. ∎

Thus, the (surjection, inclusion)-factorisation system on
$\mathbf{Topos}_{\mathrm{f}}$ transports to the (essentially surjective upto
retract, fully faithful)-factorisation system in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$. For any functor $A:\mathcal{I}\to\mathcal{J}$, it can
be factored as
$\mathcal{I}\to{{\hat{\rule{0.0pt}{5.16663pt}\smash{\operatorname{img}A}\mkern
4.0mu}\mkern-4.0mu}{}}\to\mathcal{J}$, where
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\operatorname{img}A}\mkern
4.0mu}\mkern-4.0mu}{}}$ is the retract closure of images of $A$ in
$\mathcal{J}$. Notice that to take retract closure is forced when working in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, because the image $\operatorname{img}A$ might not be
Cauchy complete.

The argument in the proof of Lemma 2.17 is typical for the class of finite
Cauchy complete categories, and we will see further examples when we look at
open functors to describe the duality for finite Heyting pretoposes.

However, the class of surjections is not entirely well-behaved in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, because it is not stable under 2-pullbacks. For
instance, consider the following category in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$

$\mathcal{I}:=\leavevmode\hbox to51.22pt{\vbox
to14.27pt{\pgfpicture\makeatletter\hbox{\hskip 25.61107pt\lower-8.39287pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.61107pt}{-5.88193pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
6.80554pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\bullet}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.80554pt\hfil&\hfil\hskip 30.80551pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\bullet}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
6.80554pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}}{}{{}} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-9.72011pt}{-0.97083pt}\pgfsys@lineto{11.40002pt}{-0.97083pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-9.52013pt}{-0.97083pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.6pt}{-0.97083pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {
{}{}{}}{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{}{{{}{}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}}{}{{{{}}}{{{}}}}{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{}}{{}}}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{}}{}{}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}}{}{{}} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{11.79999pt}{-5.79303pt}\pgfsys@lineto{-11.40002pt}{-5.79303pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-10.1601pt}{-5.79303pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-11.6pt}{-5.79303pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

which can be viewed as the classifying category of retract pairs. Note that
$\mathcal{I}$ has two points, which we denote as

$s,r:\mathbf{1}\to\mathcal{I},$

where $r$ denote the point on the right and $s$ the point on the left, which
is a retract of $r$. By Lemma 2.16, the point $r$ is actually _surjective_ ,
because the only other object is a retract of it. However, its 2-pullback
along the point $s$ is _empty_ ,

$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s}$$\textstyle{\mathcal{J}}$

because the two points are _not_ isomorphic. The functor
$\emptyset\to\mathbf{1}$ is evidently _not_ a surjection. This motivates us to
define the following stronger notion of surjection:

######  Definition 2.18.

We say a functor $A:\mathcal{I}\to\mathcal{J}$ is _stably surjective_ , if its
pullback along any other functor is again surjective.

It is easy to see that stably surjective morphisms are exactly _essentially
surjective functors_ :

######  Lemma 2.19.

A functor $A:\mathcal{I}\to\mathcal{J}$ is stably surjective iff it is
essentially surjective.

###### Proof.

The if direction is easy because essentially surjective functors are stable
under 2-pullbacks. On the other hand, suppose $A$ is not essentially
surjective, then we can find $a\in\mathcal{J}$ which does not lie in the
essential image of $A$. This way, again we have a 2-pullback square

$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\mathbf{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\textstyle{\mathcal{J}}$

which implies $A$ cannot be stably surjective. ∎

This stronger notion will play an important role when we study open morphisms
in the next section, and ultimately in constructing a 2-site to represent
finitely presented Heyting pretoposes.

######  Remark 2.20.

Note that there are further factorisation systems in
$\mathbf{Topos}_{\mathrm{f}}$, and all of them have corresopnding
factorisation systems in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$. We record the following results without proof, where
most of which can be seen as consequences of the results in [5]:

  * •

The (hyperconnected, localic)-factorisation system in
$\mathbf{Topos}_{\mathrm{f}}$ corresponds to the (essentially surjective and
full, faithful)-factorisation on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$. Note that Lemma 2.17 implies that this factorisation
always produces Cauchy complete categories.

  * •

The pair (terminally connected, étale) forms an orthogonal factorisation
system in the 2-category $\mathbf{EssTopos}$ of Grothendieck toposes and
essential geometric morphisms. An essential geometric morphism $f$ is
terminally connected iff the further left adjoint $f_{!}$ of $f^{*}$ preserves
the terminal object. Since all geometric morphisms between
$\mathbf{Set}_{\mathrm{f}}$-bounded toposes are essential, they again form an
orthogonal factorisation system in $\mathbf{Topos}_{\mathrm{f}}$, and this
exactly corresopnds to the (initial, discrete opfibration)-factorisation
system in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$.

###  2.4 Open Functors and Duality of Finite Heyting Pretoposes

As we have mentioned, it turns out that any finite pretopos is automatically
Heyting. Let $\mathbf{HPretopos}_{\mathrm{f}}$ be the 2-category of _finite
Heyting pretoposes_ , which is defined to be a wide subcategory of
$\mathbf{Pretopos}_{\mathrm{f}}$ with Heyting functors between them. Recall
that a geometric morphism is called _open_ if its inverse image functor is
Heyting. According to Lemma 2.11, to find the dual of
$\mathbf{HPretopos}_{\mathrm{f}}$, it is equivalent to characterise _open_
geometric morphisms between $\mathbf{Set}_{\mathrm{f}}$-bounded toposes.

In fact, Chapter C3.1 of [9] already contains a classification of open
geometric morphisms between presheaf toposes which are induced by a functor
between the underlying categories. This suffices for our purpose because any
geometric morphism in $\mathbf{Topos}_{\mathrm{f}}$ arises this way.
Concretely, a functor $A:\mathcal{I}\to\mathcal{J}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ induces an _open_ geometric morphism iff it satisfies
the following combinatorial property: For any $x\in\mathcal{I}$ and any
$f:Ax\to a$ in $\mathcal{J}$, there exists some $u:x\to y$ in $\mathcal{I}$
such that $a$ is a _retract_ of $Ay$ under $Ax$,

${a}$${Ay}$${Ax}$$\scriptstyle{f}$$\scriptstyle{Au}$

From our characterisation of surjections, we can rephrase it as follows:

######  Definition 2.21.

We say a functor $A:\mathcal{I}\to\mathcal{J}$ is _upwards surjective_ if for
any $x\in\mathcal{I}$, the induced functor

$A_{x/}:\mathcal{I}_{x/}\to\mathcal{J}_{Ax/}$

is a surjection.

Although open functors are not necessarily surjective, they will be once we
restricts to any upwards part of the functor:

######  Lemma 2.22.

$A:\mathcal{I}\to\mathcal{J}$ is open iff it is upwards surjective.

###### Proof.

Recall that by Proposition 2.16, a functor is a surjection iff it is
essentially surjective upto retracts. It is then straight forward to see that
openness is equivalent to being upwards surjective. ∎

This way, let us use
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ to denote the wide subcategory of
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ consisting of open, or equivalently upwards
surjective, functors. As a consequence, we have the following duality result
for finite Heyting pretoposes:

######  Theorem 2.23.

The equivalence
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}\simeq\mathbf{Pretopos}_{\mathrm{f}}$
restricts to one

${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}\simeq\mathbf{HPretopos}_{\mathrm{f}}$

between the opposite 2-category of finite Cauchy complete categories with open
functors and the 2-category of finite Heyting pretoposes.

###### Proof.

By Theorem 2.12, $\mathbf{HPretopos}_{\mathrm{f}}$ is dual to the wide
subcategory of
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ of those functors inducing open geometric morphisms.
And as mentioned, the characterisation of open geometric morphisms as open
functors is given in [9]. ∎

######  Remark 2.24.

Just like that the duality between finite Cauchy complete categories and
finite pretoposes restricts to the localic case, so is our duality of open
functors with Heyting morphisms. This means that we have a commuative
diagramme as follows,

${\mathbf{Por}_{\mathrm{f}}^{\operatorname{op}}}$${\mathbf{HA}_{\mathrm{f}}}$${\mathbf{Pos}_{\mathrm{f}}^{\operatorname{op}}}$${{\mathbf{DL}_{\mathrm{f}}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}}$${{\mathbf{HPretopos}_{\mathrm{f}}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\operatorname{op}}}$${{\mathbf{Pretopos}_{\mathrm{f}}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\dashv}$

In our finitary case, open functors have nicer properties. As mentioned in
Section 2.3, surjections are not necessarily stable under 2-pullbacks in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$. One important observation for open functors in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ is that, open morphisms $A:\mathcal{I}\to\mathcal{J}$
in ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ are not just upwards surjective, but _upwards stably
surjective_ :

######  Proposition 2.25.

For any functor $A:\mathcal{I}\to\mathcal{J}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, $A$ is open iff it is upwards stably surjective, i.e.
for any $x\in\mathcal{I}$, $A_{x/}:\mathcal{I}_{x/}\to\mathcal{J}_{Ax/}$ is
essentially surjective.

###### Proof.

The if direction is trivial. Suppose $A:\mathcal{I}\to\mathcal{J}$ is open,
consider any $f:Ax\to a$. Now by assumption, there exists some $u_{1}:x\to
x_{1}$ and a retract pair $s_{1}:a\rightleftarrows Ax_{1}:r_{1}$, inducing the
following diagramme,

${a}$${Ax}$${{Ax_{1}}}$$\scriptstyle{f}$$\scriptstyle{Au_{1}}$

Consider the following recursive process:

  * •

If the retract pair $s_{1}:a\rightleftarrows Ax_{1}:r_{1}$ is trivial, viz. an
isomorphism, then we are done, since now $f$ is isomorphic to $Au_{1}$ in
$\mathcal{J}_{Ax/}$.

  * •

If the retract pair is not trivial, then we may apply the openness condition
on $r_{1}:Ax_{1}\twoheadrightarrow a$ again, to obtain another retract pair
$s_{2}:a\rightleftarrows Ax_{2}:r_{2}$,

${a}$${{Ax_{1}}}$${{Ax_{2}}}$$\scriptstyle{r_{1}}$$\scriptstyle{Au_{2}}$

Note that $Au_{2}$ cannot be an isomorphism, because if it is, then by the
fact that $s_{2}r_{1}=Au_{2}$, $r_{1}$ must be monic; but $r_{1}$ is already
split epic, thus it is monic iff it is an isomoprhism, which by our assumption
it isn’t. Thus, $Au_{2}$ is not an isomorphism. Now we may run the algorithm
again recursively on $r_{2}$.

Notice that if our algorithm generates the following sequence

$\textstyle{Ax_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Au_{2}}$$\textstyle{Ax_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Au_{3}}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Au_{n}}$$\textstyle{Ax_{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Au_{n+1}}$$\textstyle{\cdots}$

with their corresponding non-trivial retract pairs $s_{i}:a\rightleftarrows
Ax_{i}:r_{i}$ for $i\leq n$, none of the composite $Au_{i+j}\circ\cdots\circ
Au_{i+1}\circ Au_{i}$ can be an isomorphism, again due to the fact that
$r_{i}$ cannot be an isomorphism by definition. Thus, either the algorithm
stops at some point, which means we have obtained a trivial retract pair,
$s_{n}:a\cong Ax_{n}:r_{n}$ for some $n$, and it follows that

$f\cong Au_{n}\circ\cdots\circ Au_{1}.$

Or the sequence is ultimately periodic, viz. there is a cofinal part of the
sequence which can be viewed as constant on some $Av:Ay\to Ay$ generating the
same retract pair $s:a\rightleftarrows Ay:r$, as indicated as follows,

${a}$${a}$${Ay}$${Ay}$$\scriptstyle{s}$$\scriptstyle{r}$$\scriptstyle{Av}$$\scriptstyle{s}$$\scriptstyle{r}$

Now by the same argument in the proof of Lemma 2.17, we may assume $v$ to be
idempotent and split $y$ in $\mathcal{I}$ as it is Cauchy complete. Since any
functor preserves splitting of idempotencies, it follows that the retract pair
$r:Ay\rightleftarrows a:s$ also lies in the essential image of $A$. ∎

This result allows us to see more directly why open functors are stable under
pullback in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ in the next section, which will be crucial for our
construction of a $(2,1)$-site on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$.

##  3 Stack Representation

In the previous section we have shown that there are dualty results as
follows,

${\mathbf{HPretopos}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}}$${\mathbf{Pretopos}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

which is a duality for the full 2-categorical version. By restricting the
above 2-categories to their corresopnding $(2,1)$-categories, similarly we
have

${\mathbf{HPt}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}}$${\mathbf{Pt}_{\mathrm{f}}^{\operatorname{op}}}$${{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

As mentioned in Section 1, our task in this section is to first put a suitable
Grothendieck topology on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, the $(2,1)$-category of finite Cauchy
complete categories with open functors, so as to realise it as a $(2,1)$-site.
Notice that as a $(2,1)$-category,
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ may not admit all finite 2-limits, but
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ does. Even if some limit does exist in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, the inclusion
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}\rightarrowtail{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ not necessarily preserves it. In the
following texts, whenever we are taking finite 2-limits of finite Cauchy
complete categories, we are always taking the 2-limits in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, even though the 2-limit might exists in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$.

However, 2-colimits in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ _do_ coincide with that in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, because they are dual to
$\mathbf{Pt}_{\mathrm{f}}$ and $\mathbf{HPt}_{\mathrm{f}}$ respectively, and
the two $(2,1)$-categories compute the same finite 2-limits. This is due to
the fact that $\mathbf{HPretopos}$ is _monadic_ over $\mathbf{Pretopos}$.

By following a logical intuition, we will be thinking about
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ as the $(2,1)$-category of _finite
Kripke frames_. Our task in Section 3.1 is to construct a Grothendieck
topology $J$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, that in some sense fully reflects its
underlying logical information. In Section 3.2 we will first construct the
stack representation functor

$\Phi_{-}:\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}\to\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J),$

where it intuitively sends each finitely presented Heyting pretopos to the
stack of its _Kripke models_.

We think of the above functor as _gros representation_ , which embeds the
opposite of the total $(2,1)$-category of finitely presented Heyting
pretoposes in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$. Any such representation also induces
a _petit representation_ , which embeds a particular Heyting pretopos
$\mathcal{H}$ in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$ via taking slices. Concretely, this
is obtained via first embed $\mathcal{H}$ as

$\mathcal{H}\to\mathcal{H}/\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}},$

by sending any $\varphi\in\mathcal{H}$ to the pullback onto the slice over it
$\mathcal{H}\to\mathcal{H}/\varphi$, and then compose with the gros
representation to get a functor

$\mathcal{H}\to\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)/\Phi_{\mathcal{H}}.$

We will show that this functor actually lands in _discrete opfibrations_ over
$\Phi_{\mathcal{H}}$, and will be a _faithful Heyting functor_ from
$\mathcal{H}$ to the discrete opfibration slice over $\Phi_{\mathcal{H}}$.
These will be developed in Section 3.3.

###  3.1 The $(2,1)$-Site of Finite Kripke Frames

For a general discussion on 2-categorical notions of sites and stacks, we
refer the readers to [22]. The Grothendieck topology $J$ we put on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ is obtained by choosing a specific
family of covers. For us, the relevant notion lies in _open surjections_. For
any
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ and any family of maps
$\left\\{A_{i}:\mathcal{Q}_{i}\to\mathcal{P}\right\\}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, we say it is a _$J$ -cover_ if it
contains a _finite_ family which is _jointly surjective_. Since we work in the
$(2,1)$-category
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, this is equivalent to the existence of
a finite set $I$ such that the induced coproduct

$[A_{i}]_{i\in I}:\coprod_{i\in
I}\mathcal{Q}_{i}\twoheadrightarrow\mathcal{P}$

is an open surjection. Notice that it is necessarily open, thus the condition
solely lies in surjectivity.

To see this gives a well-defined Grothendieck coverage $J$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, we first establish certain stability
result. Our first observation is that, due to our characterisation of open
maps in Proposition 2.25, open maps are indeed stable under 2-pullback in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$:

######  Lemma 3.1.

In ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$, if $A:\mathcal{Q}\to\mathcal{P}$ is
open, then its pullback along any $B:\mathcal{R}\to\mathcal{P}$ will again be
open,

$\textstyle{\mathcal{Q}\times_{\mathcal{P}}\mathcal{R}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\scriptstyle{D}$$\scriptstyle{C}$$\textstyle{\mathcal{Q}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\mathcal{R}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{\mathcal{P}}$

###### Proof.

Recall by Proposition 2.25, a morphism is open iff it is upwards stably
surjective, thus the results will follow from a computation of slices. For any
$(q,r,\alpha)\in\mathcal{Q}\times_{\mathcal{P}}\mathcal{R}$ with
$\alpha:Aq\cong Br$, let $p$ be some element in $\mathcal{P}$ isomorphic to
both $Aq$ and $Br$. This way, we would also have a 2-pullback square on
slices,

$\textstyle{(\mathcal{Q}\times_{\mathcal{P}}\mathcal{R})_{(q,r)/}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\scriptstyle{D}$$\scriptstyle{C}$$\textstyle{\mathcal{Q}_{q/}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{A}$$\textstyle{\mathcal{R}_{r/}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B}$$\textstyle{\mathcal{P}_{p/}}$

By $A$ being open, we know that
$\mathcal{Q}_{q/}\twoheadrightarrow\mathcal{P}_{p/}$ is stably surjective,
thus so is its pullback. This implies $C$ is open as well. ∎

######  Remark 3.2.

In topos theory, it is true more generally that open geometric morphisms are
stable under pullback along bounded geometric morphisms, e.g. see Chapter C3.1
in [9]. In the finitary case of our interest, as shown in Lemma 3.1 this
stability result can be seen as a direct consequence of the combinatorial
properties of open maps established in Proposition 2.25. In contrast, for a
general functor $F:\mathcal{C}\to\mathcal{D}$ which is open, its pullback
along any other functor $G:\mathcal{B}\to\mathcal{D}$ computed in
$\mathbf{Cat}$ is by no means necessarily still open.

As an easy consequence, so is open surjections:

######  Lemma 3.3.

A functor in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ is an open surjection iff it is stably
surjective and upwards stably surjective, thus in particular open surjections
are also stable under 2-pullbacks.

###### Proof.

We only need to show any open surjection is stably surjective, viz.
essentially surjective. Suppose $A:\mathcal{I}\to\mathcal{J}$ is an open
surjection, then for any $a\in\mathcal{J}$, by $A$ being surjective we can
find a retract pair $s:a\rightleftarrows Ax:r$. Now by $A$ being open, the
functor

$A_{x/}:\mathcal{I}_{x/}\twoheadrightarrow\mathcal{J}_{Ax/}$

is essentially surjective, thus we can find $u:x\to y$ in $\mathcal{I}_{x/}$
such that $Au\cong r$ in $\mathcal{J}_{Ax/}$. In particular, this implies
$a\cong Ay$, thus $A$ is essentially surjective. ∎

With such a stability result, we can now easily see that $J$ is a Grothendieck
coverage on the $(2,1)$-category
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$:

######  Lemma 3.4.

$J$ is a Grothendieck coverage on the $(2,1)$-category
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$.

###### Proof.

Any equivalence is evidently an open surjection. For any $J$-covering family
on $\mathcal{P}$, suppose it contains a jointly surjective family
$\left\\{A_{i}:\mathcal{Q}_{i}\to\mathcal{P}\right\\}_{i\in I}$. For any
$B:\mathcal{R}\to\mathcal{P}$, the family of pullbacks
$\left\\{B^{*}A_{i}:\mathcal{Q}_{i}\times_{\mathcal{P}}\mathcal{R}\to\mathcal{R}\right\\}_{i\in
I}$ by Lemma 3.3 is again jointly surjective, because coproducts in the
$(2,1)$-category
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ are disjoint. Thus, $J$ satisfies stability.
Transitivity is evident from the fact that open surjections are closed under
composition. ∎

This way, we have constructed a $(2,1)$-site
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$. Before studying the $(2,1)$-topos
generated by this $(2,1)$-site, we observe that in practice it is often easier
to work with a _dense subsite_ of it. Let
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ be the full sub
2-category of
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ consisting of those finite Cauchy
complete categories which has an _initial object_. If
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ has an initial object, we
will also call it _rooted_ , and use $*$ to denote the root, or the initial
object, of $P$.

We show that objects in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ are _regular_ for the
site $({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$:

######  Lemma 3.5.

If $\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ is rooted, then
$A:\mathcal{Q}\to\mathcal{P}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ is an open surjection iff
$*\in\mathcal{P}$ lies in the essential image of $A$.

###### Proof.

By Lemma 3.3, an open surjection $A:\mathcal{Q}\to\mathcal{P}$ must be
essentially surjective, thus $*$ does lie in the essential image of $A$. On
the other hand, if there exists $q\in\mathcal{Q}$ with $Aq\cong*$, then since
$A$ is open, we have a stable surjection

$A_{q/}:\mathcal{Q}_{q/}\twoheadrightarrow\mathcal{P}_{*/}\cong\mathcal{P}$

This particularly implies that $A:\mathcal{Q}\twoheadrightarrow\mathcal{P}$ is
also essentially surjective, thus $A$ is an open surjection. ∎

######  Corollary 3.6.

If $\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ is rooted, then any
covering family on $\mathcal{P}$ contains a single open surjection.

###### Proof.

Consider any finite family
$\left\\{A_{i}:\mathcal{Q}_{i}\to\mathcal{P}\right\\}$ which is jointly
surjective,

$[A_{i}]:\coprod\mathcal{Q}_{i}\twoheadrightarrow\mathcal{P}.$

Now since $*\in\mathcal{P}$ lies in the essential image, there must exist some
$i$ that $*\in\mathcal{P}$ lies in the essential image of
$A_{i}:\mathcal{Q}_{i}\to\mathcal{P}$. By Lemma 3.5, $A_{i}$ is already an
open surjection. ∎

Furthermore, any object in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ can be covered by these regular objects:

######  Lemma 3.7.

Any
$\mathcal{I}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$ admits a $J$-covering family
$\left\\{\mathcal{P}_{i}\to\mathcal{I}\right\\}_{i\in I}$ where each
$\mathcal{P}_{i}$ is rooted.

###### Proof.

For any $x\in\mathcal{I}$, consider the functor
$\mathcal{I}_{x/}\to\mathcal{I}$. All such maps are open, and the finite
family $\left\\{\mathcal{I}_{x/}\to\mathcal{I}\right\\}_{x\in\mathcal{I}}$
evidently is a $J$-covering family. ∎

######  Corollary 3.8.

The inclusion $({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)\hookrightarrow({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J)$ induces an equivalence on the
$(2,1)$-toposes of stacks over them,

$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)\simeq\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong},J).$

###### Proof.

Lemma 3.7 implies ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}$ is a $J$-dense full subcategory of
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$, and the desired result follows from a comparison
lemma for 2-toposes, e.g. see Theorem 3.8 in [22]. ∎

Thus, we can always work with the site
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, where now for any
rooted $\mathcal{P}$, a family is $J$-covering iff it contains a single open
surjection. This means that $J$ is a _regular_ topology on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}$, which helps us greatly to compute
2-colimits of stacks.

###  3.2 Stack Representation of Heyting Pretoposes

Now for a general Heyting pretopos $\mathcal{H}$, we know that they are not
complete w.r.t. classical models. For our focus of finitely presented Heyting
pretopos, we will consider its models in all _finite Kripke frames_ , i.e.
models valued in the Heyting pretoposes of the form
$\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$, for
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$. In particular, _any_
Heyting pretopos $\mathcal{H}$ induces a prestack $\Phi_{\mathcal{H}}$ on the
$(2,1)$-category ${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ as follows:

$\Phi_{\mathcal{H}}:=\mathbf{HPt}(\mathcal{H},\mathbf{Set}_{\mathrm{f}}[-]),$

where $\mathbf{HPt}$ is the $(2,1)$-category of Heyting pretoposes. In
particular, $\Phi_{\mathcal{H}}$ is groupoid valued. The action of
$\Phi_{\mathcal{H}}$ on $A:\mathcal{Q}\to\mathcal{P}$ in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ is given by post-
composition with the inverse image
$A^{*}:\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]\to\mathbf{Set}_{\mathrm{f}}[\mathcal{Q}]$.
For any finite Kripke frame
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$, we think of
$\Phi_{\mathcal{H}}(\mathcal{P})$ as the _groupoid of models_ of $\mathcal{H}$
on the $\mathcal{P}$, or simply _$\mathcal{P}$ -models_ of $\mathcal{H}$. In
particular, the pre-stack records the information of all _finite_ models of
$\mathcal{H}$ on _finite_ Kripke frames.

Our first task then is to show that $\Phi_{\mathcal{H}}$ will indeed be a
_stack_ for the topology $J$ we have chosen on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$, and this in fact can be
seen as a consequence of the descent theorem for toposes.

######  Lemma 3.9.

For any Heyting pretopos $\mathcal{H}$, $\Phi_{\mathcal{H}}$ is a stack of
groupoids on the $(2,1)$-site
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$.

###### Proof.

Recall the descent theorem for toposes first given in [10], which states that
open surjections are of effective descent for toposes. Since the descent
theorem can be proven in purely elementary means, e.g. see [14], in our
finitary case this implies that the following diagramme will be a 2-colimit in
$\mathbf{Topos}_{\mathrm{f}}$ under the equivalence with
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$,

${\mathcal{Q}\times_{\mathcal{P}}\mathcal{Q}\times_{\mathcal{P}}\mathcal{Q}}$${\mathcal{Q}\times_{\mathcal{P}}\mathcal{Q}}$${\mathcal{Q}}$${\mathcal{P}}$$\scriptstyle{A}$

By duality, this becomes a 2-limit in $\mathbf{Pretopos}_{\mathrm{f}}$. In
fact, the dual will be a 2-limit in $\mathbf{Pretopos}$, since the full
inclusion $\mathbf{Pretopos}_{\mathrm{f}}\hookrightarrow\mathbf{Pretopos}$
evidently preserves and creates finite 2-limits. As we’ve mentioned, 2-limits
in $\mathbf{HPretopos}$ are computed the same as in $\mathbf{Pretopos}$, thus
the dual diagramme is also a 2-limit for Heyting pretoposes. ∎

######  Remark 3.10.

In fact for our finitary case, it is fairely straight forward to directly
prove that the above diagramme is a 2-colimit in
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}$ when $A$ is an open surjection, which avoids the more
technical topos-theoretic proofs. We leave the details for the interested
readers.

This way, we have realised any Heyting pretopos $\mathcal{H}$ as a stack of
groupoid of finite models over the $(2,1)$-category of finite Kripke frames.
However, due to our restriction on finite models on finite Kripke frames, we
cannot expect that this stack $\Phi_{\mathcal{H}}$ we associate to
$\mathcal{H}$ will reveal all the information for an arbitrary Heyting
pretopos. This way, we introduce the relevant class of _finitely presentable_
Heyting pretoposes:

######  Definition 3.11.

We say a Heyting pretopos $\mathcal{H}$ is _finitely presentable_ , if it is
complete w.r.t. finite models on finite Kripke frames, i.e. the following
canonical functor is _faithful_

$\mathcal{H}\rightarrowtail\prod_{\mathcal{P}\in{{\hat{\rule{0.0pt}{3.61664pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*},F\in\Phi_{\mathcal{H}}(\mathcal{P})}\mathbf{Set}_{\mathrm{f}}[\mathcal{P}],$

Let us use $\mathbf{HPt}_{\mathrm{fp}}$ to denote the $(2,1)$-category of
finitely presentable Heyting pretoposes. From the above definition,
$\mathbf{HPt}_{\mathrm{fp}}$ basically contains those sub Heyting pretoposes
of products of finite ones. We thus view our stack representation as a
2-functor as follows,

$\Phi_{-}:\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}\to\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J),$

This way, we have indeed embedded our interested class of Heyting pretoposes
into the 2-category of stacks on the 2-site
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, contravariantly.

Evidently, finite Heyting pretoposes are finitely presentable. More generally,
the _free_ Heyting pretopos generated by a finite pretopos will also be
finitely presentable. For any finite Pretopos
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]$, the free Heyting pretopos generated
by it will be denoted as $\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]$. In
particular, for any Heyting pretopos $\mathcal{H}$, we have a natural
equivalence of categories

$\mathbf{Pretopos}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}],\mathcal{H})\simeq\mathbf{HPretopos}(\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}],\mathcal{H}).$

where the equivalence is induced by an inclusion
$\mathbf{Set}_{\mathrm{f}}[\mathcal{I}]\rightarrowtail\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]$.
For instance, the _initial_ Heyting pretopos can be identified as the free
Heyting pretopos
$\mathbf{Hey}_{\mathrm{f}}\simeq\mathbf{Hey}_{\mathrm{f}}[\mathbf{1}]$, which
is freely generated by
$\mathbf{Set}_{\mathrm{f}}=\mathbf{Set}_{\mathrm{f}}[\mathbf{1}]$.

It is instructive to look at the stack representation of these free Heyting
pretoposes. Notice that for any
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ we have the following
equivalences,

$\displaystyle\Phi_{\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]}(\mathcal{P})$
$\displaystyle\simeq\mathbf{HPt}_{\mathrm{fp}}(\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}],\mathbf{Set}_{\mathrm{f}}[\mathcal{P}])$
$\displaystyle\simeq\mathbf{Pt}_{\mathrm{fp}}(\mathbf{Set}_{\mathrm{f}}[\mathcal{I}],\mathbf{Set}_{\mathrm{f}}[\mathcal{P}])$
$\displaystyle\simeq{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}(\mathcal{P},\mathcal{I}).$

We also write the stack
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}(-,\mathcal{I})$ on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ as
$\underline{\mathcal{I}}$. The above equivalence shows that for any finite
Cauchy complete category $\mathcal{I}$, we have

$\Phi_{\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]}\simeq\underline{\mathcal{I}}$

in the $(2,1)$-category
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, and thus by Lemma
3.9, all prestacks of the form $\underline{\mathcal{I}}$ are in fact stacks
for the topology $J$.

######  Remark 3.12.

In fact, one can show that $J$ is the _canonical_ topology on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$, i.e. the largest
topology such that all representable prestacks are stacks. One can write down
a proof of this fact very similar to the posetal case presented in [7]. But
since this is irrelevant for our investigation, we omit it here.

We also note that the 2-category of finite Heyting pretoposes is closed under
slices, thus as a consequence it is closed under finite quotients of finitely
presentable Heyting pretoposes:

######  Lemma 3.13.

If $\mathcal{H}$ is a finite Heyting pretopos, then so is the slice
$\mathcal{H}/\varphi$ for any $\varphi\in\mathcal{H}$.

###### Proof.

Recall that the slice $\mathcal{H}/\varphi$ classifies $\varphi$-points of
models of $\mathcal{H}$,

$\mathbf{HPt}_{\mathrm{f}}(\mathcal{H}/\varphi,\mathbf{Set}_{\mathrm{f}}[\mathcal{P}])\cong\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}\Gamma
F\varphi\cong\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(F\varphi)_{*}.$

Here $\Gamma$ is the global section functor, and the sum notation
$\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}\Gamma F\varphi$ denote the
category of pairs $(F,\alpha)$ with $F\in\Phi_{\mathcal{H}}(\mathcal{P})$ a
model of $\mathcal{H}$ in $\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$, while
$\alpha:1\to F\varphi$ is a global point of $F\varphi$ in
$\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$. This is well-known, and one explicit
proof can be found e.g. in Chapter 2.3 of [3].222The proof there is given for
pretoposes, but the same proof works for Heyting pretoposes as well. The final
isomorphism is due to the fact that $\mathcal{P}$ has an initial object, thus
taking the global section is equivalent of evaluating on the root.

Now if we have a proper subterminal object $U$ in $\mathcal{H}/\varphi$, it
corresponds to some proper subobject $U\rightarrowtail\varphi$. By
$\mathcal{H}$ being finite, we can find a finite model
$F:\mathcal{H}\to\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$ such that
$FU\subsetneq F\varphi$ is proper. Then we may choose some
$a\in(F\varphi)_{*}$ such that $a\not\in(FU)_{*}$. The pair $(F,a)$ then gives
us a model of $\mathcal{H}/\varphi$ which falsifies $U$. ∎

######  Remark 3.14.

It might be tempting to say that _all_ finitely presentable Heyting pretoposes
are finite quotients of some free one of the form
$\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]$. However we do not know whether this
is true or not at this point.

###  3.3 From Gros to Petit

Following the _“gros-petit”_ philosophy in topos theory, given any finitely
presented Heyting pretopos $\mathcal{H}$, the _petit_ category $\mathcal{H}$
can be embedded into the gros category
$\mathcal{H}/\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}$ of the opposite
of the 2-category of finite Heyting pretoposes under $\mathcal{H}$,

$\mathcal{H}\rightarrowtail\mathcal{H}/\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}},$

sending any $\varphi\in\mathcal{H}$ to the pullback onto the slice over it,

$\varphi^{*}:\mathcal{H}\to\mathcal{H}/\varphi.$

By composing with the stack representation
$\Phi_{-}:\mathbf{HPt}_{\mathrm{fp}}^{\operatorname{op}}\to\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$ functor, which we may
as well denote it as the _gros representation functor_ , we naturally get a
_petit representation_ of $\mathcal{H}$ as follows,

$\mathcal{H}\to\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)/\Phi_{\mathcal{H}}.$

On the left we have a _1-category_ $\mathcal{H}$, thus we expect that this
representation to land in _discrete_ objects over $\Phi_{\mathcal{H}}$
internally in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$.

Following the general development of fibrations in a 2-category in [21], in a
2-category $\mathcal{K}$ a morphism $f:A\to B$ is called a _discrete
opfibration_ if for any $C\in\mathcal{K}$, the induced functor
$\mathcal{K}(C,A)\to\mathcal{K}(C,B)$ is a discrete opfibration. Notice that
for a fibration, we would also require that for any $g:D\to C$ the base change
square will be a morphism of fibrations. However, since for discrete
opfibrations every morphism in the over category will be Cartesian, this
condition is trivially satisfied. Equivalently, $f:A\to B$ is a discrete
fibration iff it is a discrete object in the 2-category of opfibrations over
$B$, and discrete opfibrations over some object naturally forms a
_1-category_.

In the $(2,1)$-category of stacks over
$({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, to check opdiscrete
fibrations it suffices to check on representables. For any stack $\mathcal{F}$
in $\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, we use
$\mathbf{opDisc}(\mathcal{F})$ to denote the 1-category of opdiscrete
fibrations on $\mathcal{F}$. Furthermore, the category
$\mathbf{opDisc}(\mathcal{F})$ will in fact be a _Heyting category_ , e.g. see
[20].

We first show the petit representation functor indeed lands in discrete
opfibrations in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$:

######  Lemma 3.15.

The petit representation restricts to a functor as follows:

$\mathcal{H}\to\mathbf{opDisc}(\Phi_{\mathcal{H}}).$

###### Proof.

Given any $\varphi\in\mathcal{H}$, by construction for any
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$, the morphism

$\Phi_{\mathcal{H}/\varphi}(\mathcal{P})\cong\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}\Gamma
F\varphi\cong\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(F\varphi)_{*}\to\Phi_{\mathcal{H}}(\mathcal{P})$

is given by the projection map. Evidently, for any
$F\in\Phi_{\mathcal{H}}(\mathcal{P})$, the fibre of $F$ over this projection
is the _discrete set_ $(F\varphi)_{*}$. Furthermore, for any $\eta:F\cong G$,
this naturally provides a map $(F\varphi)_{*}\to(G\varphi)_{*}$. This shows
for any $\mathcal{P}$ the above map morphism is a discrete opfibration, thus
$\Phi_{\mathcal{H}/\varphi}\to\Phi_{\mathcal{H}}$ is a discrete opfibration in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$. ∎

More importantly, when restricting the codomain the discrete opfibrations over
$\Phi_{\mathcal{H}}$, the petit representation will be a _faithful Heyting
functor_ for any finitely presented Heyting pretopos:

######  Theorem 3.16.

For any $\mathcal{H}$ in $\mathbf{HPt}_{\mathrm{fp}}$, the petit
representation

$\mathcal{H}\rightarrowtail\mathbf{opDisc}(\Phi_{\mathcal{H}})$

is a faithful Heyting functor.

###### Proof.

Faithfulness is basically built in in our definition of finitely presented
Heyting pretoposes. Once we know it is a Heyting functor, it suffices to show
for any proper subterminal object $\varphi$, it is not mapped to the identity
on $\Phi_{\mathcal{H}}$. However, by $\mathcal{H}$ being finitely presented,
there exists some
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ and a Heyting functor
$F:\mathcal{H}\to\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$ that
$F\varphi\rightarrowtail 1$ is a proper subterminal object in
$\mathbf{Set}_{\mathrm{f}}[\mathcal{P}]$. This implies $(F\varphi)_{*}$ must
be empty, thus $F\not\in\Phi_{\mathcal{H}/\varphi}(\mathcal{P})$. Hence, the
induced injection
$\Phi_{\mathcal{H}/\varphi}\rightarrowtail\Phi_{\mathcal{H}}$ must also be
proper. Hence, the remaining is to show it is a Heyting functor.

We first show it preserves finite limits. Preserving the terminal objects is
evident, since we have

$\mathcal{H}/1\simeq\mathcal{H}\mapsto\Phi_{\mathcal{H}}=\Phi_{\mathcal{H}}.$

For any $\alpha:\psi\to\varphi$ and $\beta:\chi\to\varphi$ in $\mathcal{H}$,
we have the following equivalences,

$\displaystyle\,(\Phi_{\mathcal{H}/\psi}\times_{\Phi_{\mathcal{H}/\varphi}}\Phi_{\mathcal{H}/\chi})(\mathcal{P})$
$\displaystyle\cong$
$\displaystyle\,\\{\,(F,a)\in\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(F\psi)_{*},(G,b)\in\sum_{G\in\Phi_{\mathcal{H}}(\mathcal{P})}(G\chi)_{*}\mid
F=G\operatorname{\&}F\alpha a=G\beta b\,\\}$ $\displaystyle\cong$
$\displaystyle\sum_{H\in\Phi_{\mathcal{H}}(\mathcal{P})}(H\psi)_{*}\times_{(H\varphi)_{*}}(H\chi)_{*}$
$\displaystyle\cong$
$\displaystyle\sum_{H\in\Phi_{\mathcal{H}}(\mathcal{P})}H(\psi\times_{\varphi}\chi)_{*}$
$\displaystyle\cong$
$\displaystyle\,\Phi_{\mathcal{H}/\psi\times_{\varphi}\chi}(\mathcal{P})$

The first isomorphism is due to the fact that pullbacks in
$\mathbf{opDisc}(\Phi_{\mathcal{H}})$ are computed point-wise; the second and
the last isomorphisms have used the computation of models of slice Heyting
pretoposes mentioned in the proof of Lemma 3.15; the third holds due to the
fact that both $H$ and evaluation on the root preserve pullbacks.

Next, we show that for any $X\in\mathcal{H}$, the induced map on subobjects

$\operatorname{Sub}_{\mathcal{H}}(X)\to\operatorname{Sub}_{\mathbf{opDisc}(\Phi_{\mathcal{H}})}(\Phi_{\mathcal{H}/X})$

is a distributive lattice morphism. Now subobjects of $\Phi_{\mathcal{H}/X}$
in $\mathbf{opDisc}(\Phi_{\mathcal{H}})$ coincides with subobjects of
$\Phi_{\mathcal{H}/X}$ which are discrete opfibrations, e.g. see [20], thus we
have the following isomorphism

$\operatorname{Sub}_{\mathbf{opDisc}(\Phi_{\mathcal{H}})}(\Phi_{\mathcal{H}/X})\cong\operatorname{Sub}_{\mathbf{opDisc}(\Phi_{\mathcal{H}/X})}(\Phi_{\mathcal{H}/X}).$

This means it suffices to consider when $X$ is the terminal object. Given
subterminal objects $\varphi,\psi\rightarrowtail 1$ in $\mathcal{H}$, by
definition for any
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$,

$\displaystyle\Phi_{\mathcal{H}/\varphi\wedge\psi}(\mathcal{P})$
$\displaystyle\cong\\{\,F\in\Phi_{\mathcal{H}}(\mathcal{P})\mid
F(\varphi\wedge\psi)_{*}\cong 1\,\\}$
$\displaystyle\cong\\{\,F\in\Phi_{\mathcal{H}}(\mathcal{P})\mid(F\varphi)_{*}\,\\}\cap\\{\,F\in\Phi_{\mathcal{H}}(\mathcal{P})\mid(F\models\psi)_{*}\,\\}$
$\displaystyle\cong\Phi_{\mathcal{H}/\varphi}\cap\Phi_{\mathcal{H}/\psi}$

Again, the second isomorphism holds since any such $F$ preserves finite
limits. This shows the petit representation preserves meets in subobject
lattices. Completely similarly it also preserves disjunctions. However, this
further relies on the fact that $J$ is a _regular_ topology on
${{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$, thus disjunction in
subobject lattices of $\mathbf{opDisc}(\Phi_{\mathcal{H}})$ are also computed
point-wise.

To show it is a map between Heyting categories, we also need to show that the
functor commutes with exisential and universal quantifiers. Given any
$\alpha:Y\to X$ and $\varphi\rightarrowtail Y$, for the case of existential
quantification,

$\displaystyle\,\Phi_{\mathcal{H}/\exists_{\alpha}\varphi}(\mathcal{P})$
$\displaystyle\cong$
$\displaystyle\,\\{\,(F,a)\in\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(FX)_{*}\mid
a\in(F\exists_{\alpha}\varphi)_{*}\,\\}$ $\displaystyle\cong$
$\displaystyle\,\\{\,(F,a)\in\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(FX)_{*}\mid
a\in\exists_{(F\alpha)_{*}}(F\varphi)_{*}\,\\}$ $\displaystyle\cong$
$\displaystyle\,\\{\,(F,a)\in\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(FX)_{*}\mid\exists
b\in(F\varphi)_{*}.\alpha b=a\,\\}$ $\displaystyle\cong$
$\displaystyle\,\exists_{\Phi_{\mathcal{H}/\alpha}}\Phi_{\mathcal{H}/\varphi}(\mathcal{P})$

The second isomorphism holds since $F$ preserves existential quantifier, and
that again due to the topology $J$ being regular, existential quantification
is also computed point-wise thus preserved by $\mathrm{ev}_{*}$; the last
isomorphism holds for the same reason.

Finally, for universal quantification, we have

$\displaystyle\Phi_{\mathcal{H}/\forall_{\alpha}\varphi}(\mathcal{P})\cong\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}(\forall_{F\alpha}F\varphi)_{*}$
$\displaystyle\cong$
$\displaystyle\sum_{F\in\Phi_{\mathcal{H}}(\mathcal{P})}\\{\,x\in(FX)_{*}\mid\forall
p\in\mathcal{P}.\forall y\in(FY)_{p}.\alpha y=px\Rightarrow
y\in(F\varphi)_{p}\,\\}$

The last isomorphism is basically by Kripke-Joyal semantics, for a reference
see Chapter VI of [11]. On the other hand, if we compute the universal
quantification in $\mathbf{opDisc}(\Phi_{\mathcal{H}})$, again by Kripke-Joyal
semantics we have

$\displaystyle\,\forall_{\Phi_{\mathcal{H}/\alpha}}\Phi_{\mathcal{H}/\varphi}(\mathcal{P})$
$\displaystyle\cong$
$\displaystyle\,\\{\,(F,x)\in\Phi_{\mathcal{H}/X}(\mathcal{P})\,\mid\,$
$\displaystyle\forall
A\\!\\!:\\!\\!\mathcal{Q}\to\mathcal{P}.\,\forall(G,y)\in\Phi_{\mathcal{H}/Y}(\mathcal{Q})$
$\displaystyle G=A^{*}F\operatorname{\&}\alpha
y=A^{*}x\Rightarrow(G,y)\in\Phi_{\mathcal{H}/\varphi}(\mathcal{P})\\}$
$\displaystyle\cong$
$\displaystyle\,\\{\,(F,x)\in\Phi_{\mathcal{H}/X}(\mathcal{P})\,\mid\,$
$\displaystyle\forall A\\!\\!:\\!\\!\mathcal{Q}\to\mathcal{P}.\,\forall
y\in(A^{*}FY)_{*}$ $\displaystyle\alpha y=A^{*}x\Rightarrow
y\in(A^{*}F\varphi)_{*}\\}$

However, for any such $A:\mathcal{Q}\to\mathcal{P}$, we know that

$y\in(A^{*}F\varphi)_{*}\Leftrightarrow y\in(F\varphi)_{p}.$

where $p=A*$. Hence, the above two subobjects are isomorphic, which shows that
the petit representation also commutes with the universal quantification. This
completes the proof that the petit representation is a faithful Heyting
functor. ∎

Thus, according to Theorem 3.16, any finitely presented Heyting pretopos
$\mathcal{H}$ now can be viewed as a sub Heyting category of the discrete
opfibred objects over $\Phi_{\mathcal{H}}$ in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$. As we’ve mentioned,
when $\mathcal{H}$ is free of the form
$\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]$ for some
$\mathcal{I}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cat}_{\mathrm{f}}}\mkern
4.0mu}\mkern-4.0mu}{}}^{\\!\\!\cong}$,
$\Phi_{\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]}$ is isomorphic to
$\underline{\mathcal{I}}$. Thus, for this special case, the petit
representation provides a faithful Heyting functor

$\mathbf{Hey}_{\mathrm{f}}[\mathcal{I}]\rightarrowtail\mathbf{opDisc}(\underline{\mathcal{I}}).$

At last, we look at the base change of petit representations, which explains
its relationship with the gros representation in more concrete terms:

######  Lemma 3.17.

For any Heyting functor $\alpha:\mathcal{H}\to\mathcal{G}$ in
$\mathbf{HPt}_{\mathrm{fp}}$, the following diagramme commutes,

${\mathcal{H}}$${\mathbf{opDisc}(\Phi_{\mathcal{H}})}$${\mathcal{G}}$${\mathbf{opDisc}(\Phi_{\mathcal{G}})}$$\scriptstyle{\alpha}$$\scriptstyle{\Phi_{\alpha}^{*}}$

where $\Phi_{\alpha}:\Phi_{\mathcal{G}}\to\Phi_{\mathcal{H}}$ is the morphism
of stacks induced by the gros representation, and $\Phi_{\alpha}^{*}$ is the
functor of pullback along $\Phi_{\alpha}$, which preserves discrete
opfibrations.

###### Proof.

To show this, it suffices to prove that for any $\varphi\in\mathcal{H}$, the
following diagramme is a pullback in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$,

$\textstyle{\Phi_{\mathcal{G}/\alpha\varphi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\Phi_{\mathcal{H}/\varphi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\Phi_{\mathcal{G}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Phi_{\alpha}}$$\textstyle{\Phi_{\mathcal{H}}}$

We may dicretely compute the pullback on
$\mathcal{P}\in{{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong}$ as follows,

$\displaystyle\,(\Phi_{\mathcal{G}}\times_{\Phi_{\mathcal{H}}}\Phi_{\mathcal{H}/\varphi})(\mathcal{P})$
$\displaystyle\cong$
$\displaystyle\,\\{\,G\in\Phi_{\mathcal{G}}(\mathcal{P}),(F,a)\in\Phi_{\mathcal{H}/\varphi}(\mathcal{P})\mid
G\alpha=F\,\\}$ $\displaystyle\cong$
$\displaystyle\left\\{G\in\Phi_{\mathcal{G}}(\mathcal{P}),a\in(G\alpha\varphi)_{*}\right\\}$
$\displaystyle\cong$
$\displaystyle\,\Phi_{\mathcal{G}/\alpha\varphi}(\mathcal{P})$

The first holds since pullback between discrete opfibrations are computed
point-wise in
$\mathbf{St}({{\hat{\rule{0.0pt}{5.16663pt}\smash{\mathbf{Cas}}\mkern
4.0mu}\mkern-4.0mu}{}}_{\mathrm{f},*}^{\\!\\!\cong},J)$, and the remaining is
standard calculation. This completes the proof. ∎

Now for those Heyting functors induced by pullback along some
$\varphi\in\mathcal{H}$, the induced morphism between stacks by Lemma 3.15
will be a discrete opfibration

$\Phi_{\varphi}:\Phi_{\mathcal{H}/\varphi}\to\Phi_{\mathcal{H}}.$

This means the pullback functor

$\Phi_{\varphi}^{*}:\mathbf{opDisc}(\Phi_{\mathcal{H}})\to\mathbf{opDisc}(\Phi_{\mathcal{H}/\varphi})$

also has a _left adjoint_ $\Sigma_{\Phi_{\varphi}}$, which is simply given by
composition with $\Phi_{\varphi}$ because discrete opfibrations are closed
under composition. In such a case, the petit representation commutes with both
adjoints:

######  Corollary 3.18.

For any $\varphi\in\mathcal{H}$, the following diagramme commutes,

${{\mathcal{H}/\varphi}}$${{\mathbf{opDisc}(\Phi_{\mathcal{H}/\varphi})}}$${{\mathcal{H}}}$${{\mathbf{opDisc}(\Phi_{\mathcal{H}})}}$$\scriptstyle{\varphi^{*}}$$\scriptstyle{\dashv}$$\scriptstyle{\Sigma_{\varphi}}$$\scriptstyle{\dashv}$$\scriptstyle{\Sigma_{\Phi_{\varphi}}}$$\scriptstyle{\Phi_{\varphi}^{*}}$

###### Proof.

From Lemma 3.17 we already know it commutes with pullbacks. It commutes with
left adjoints by functoriality of gros representation. ∎

## References

  * Adámek and Rosicky, [1994] Adámek, J. and Rosicky, J. (1994).  Locally presentable and accessible categories, volume 189.  Cambridge University Press.
  * Artin et al., [1971] Artin, M., Grothendieck, A., and Verdier, J.-L. (1971).  Theorie de Topos et Cohomologie Etale des Schemas I, II, III, volume 269, 270, 305 of Lecture Notes in Mathematics.  Springer.
  * Breiner, [2013] Breiner, S. (2013).  Scheme representation for first-order logic.  Phd thesis, Carnegie Mellon University.  Available at arXiv:1402.2600.
  * Caramello, [2018] Caramello, O. (2018).  Theories, Sites, Toposes: Relating and studying mathematical theories through topos-theoretic’bridges’.  Oxford University Press.
  * Caramello, [2019] Caramello, O. (2019).  Denseness conditions, morphisms and equivalences of toposes.  arXiv preprint arXiv:1906.08737.
  * Dupont and Vitale, [2003] Dupont, M. and Vitale, E. M. (2003).  Proper factorization systems in 2-categories.  Journal of Pure and Applied Algebra, 179(1-2):65–86.
  * Ghilardi and Zawadowski, [2013] Ghilardi, S. and Zawadowski, M. (2013).  Sheaves, games, and model completions: A categorical approach to nonclassical propositional logics, volume 14.  Springer Science & Business Media.
  * Haigh, [1980] Haigh, J. (1980).  Essential geometric morphisms between toposes over finite sets.  Mathematical Proceedings of the Cambridge Philosophical Society, 87(1):21–24.
  * Johnstone, [2002] Johnstone, P. T. (2002).  Sketches of an Elephant: A Topos Theory Compendium, volume 1, 2\.  Oxford University Press.
  * Joyal and Tierney, [1984] Joyal, A. and Tierney, M. (1984).  An extension of the Galois theory of Grothendieck, volume 309.  American Mathematical Soc.
  * MacLane and Moerdijk, [2012] MacLane, S. and Moerdijk, I. (2012).  Sheaves in geometry and logic: A first introduction to topos theory.  Springer Science & Business Media.
  * Makkai, [1982] Makkai, M. (1982).  Stone duality for first order logic.  In Studies in Logic and the Foundations of Mathematics, volume 107, pages 217–232. Elsevier.
  * Makkai, [1993] Makkai, M. (1993).  The fibrational formulation of intuitionistic predicate logic i: completeness according to gödel, kripke, and läuchli. i.  Notre Dame Journal of Formal Logic, 34(3):334–377.
  * Moerdijk, [1985] Moerdijk, I. (1985).  An elementary proof of the descent theorem for grothendieck toposes.  Journal of Pure and Applied Algebra, 37:185–191.
  * nLab authors, [2024] nLab authors (2024).  (n,r)-category.  https://ncatlab.org/nlab/show/%28n%2Cr%29-category.  Revision 59.
  * [16] Pitts, A. (1983a).  Amalgamation and interpolation in the category of heyting algebras.  Journal of Pure and Applied Algebra, 29(2):155–165.
  * [17] Pitts, A. M. (1983b).  An application of open maps to categorical logic.  Journal of pure and applied algebra, 29(3):313–326.
  * Pitts, [1992] Pitts, A. M. (1992).  On an interpretation of second order quantification in first order intuitionistic propositional logic.  The Journal of Symbolic Logic, 57(1):33–52.
  * Rogers, [2023] Rogers, M. (2023).  Toposes of Topological Monoid Actions.  Compositionality, 5.
  * Shulman, [2024] Shulman, M. (2024).  Heyting 2-category.  https://ncatlab.org/nlab/show/Heyting+2-category.  Revision 1.
  * Street, [1974] Street, R. (1974).  Fibrations and yoneda’s lemma in a 2-category.  In Kelly, G. M., editor, Category Seminar, pages 104–133, Berlin, Heidelberg. Springer Berlin Heidelberg.
  * Street, [1982] Street, R. (1982).  Two-dimensional sheaf theory.  Journal of Pure and Applied Algebra, 23(3):251–270.
  * Tendas, [2022] Tendas, G. (2022).  On continuity of accessible functors.  Applied Categorical Structures, 30(5):937–946.