Iso¿—¿¿

#  Induced morphisms between Heyting-valued models

José Goudet Alvim
Universidade de São Paulo, São Paulo, Brasil
Arthur Francisco Schwerz Cahali
Universidade de São Paulo, São Paulo, Brasil
Hugo Luiz Mariano
Universidade de São Paulo, São Paulo, Brasil
jose.alvim@usp.brarthur.cahali<EMAIL_ADDRESS>
###### Abstract

To the best of our knowledge, there are very few results on how Heyting-valued
models are affected by the morphisms on the complete Heyting algebras that
determine them: the only cases found in the literature are concerning
automorphisms of complete Boolean algebras and complete embedding between them
(_i.e_., injective Boolean algebra homomorphisms that preserves arbitrary
suprema and arbitrary infima). In the present work, we consider and explore
how more general kinds of morphisms between complete Heyting algebras
$\mathbb{H}$ and $\mathbb{H}^{\prime}$ induce arrows between
$\text{V}^{(\mathbb{H})}$ and $\text{V}^{(\mathbb{H}^{\prime})}$, and between
their corresponding localic toposes $\mathbf{Set}^{\left(\mathbb{H}\right)}$
($\simeq\mathbf{Sh}\left(\mathbb{H}\right)$) and
$\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$
($\simeq\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$). In more details: any
geometric morphism
$f^{*}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$,
(that automatically came from a unique locale morphism
$f:\mathbb{H}\to\mathbb{H}^{\prime}$), can be “lifted” to an arrow
$\tilde{f}:\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$. We
also provide also some semantic preservation results concerning this arrow
$\tilde{f}:\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$.

## Introduction

The expression “Heyting-valued model of set theory” has two (related)
meanings, both parametrized by a complete Heyting algebra $\mathbb{H}$:

(i) The canonical Heyting-valued models in set theory,
$\text{V}^{(\mathbb{H})}$, as introduced in the setting of complete boolean
algebras in the 1960s by D. Scott, P. Vopěnka and R. M. Solovay in an attempt
to help understand the, then recently introduced, notion of _forcing_ in ZF
set theory developed by P. Cohen ([Jec03], [Kun11], [Bel05]);

(ii) The (local) “set-like” behavior of categories called topoi, specially in
the case of the (localic) topoi of the form
$\mathbf{Sh}\left(\mathbb{H}\right))$ ([Bor08c], [Bel88]).

The concept of a Heyting/Boolean-valued model is nowadays a general model-
theoretic notion, whose definition is independent from forcing in set theory:
it is a generalization of the ordinary Tarskian notion of structure where the
truth values of formulas are not limited to “true” and “false”, but instead
take values in some fixed complete Heyting algebra $\mathbb{H}$. More
precisely, a $\mathbb{H}$-valued model $M$ in a first-order language $L$
consists of an underlying set $M$ and an assignment
$\left\llbracket\varphi\right\rrbracket_{\mathbb{H}}$ of an element of
$\mathbb{H}$ to each formula $\varphi$ with parameters in $M$, satisfying
convenient conditions.

The canonical Heyting-valued model in set theory associated to $\mathbb{H}$ is
the pair $\left\langle\text{V}^{(\mathbb{H})},\left\llbracket\
\right\rrbracket_{\mathbb{H}}\right\rangle$, where both components are
recursively defined. Explicitly, $\text{V}^{(\mathbb{H})}$ is the proper class
$\text{V}^{(\mathbb{H})}:=\bigcup_{\beta\in\operatorname{On}}\text{V}^{(\mathbb{H})}_{\beta}$,
where $\text{V}^{(\mathbb{H})}_{\beta}$ is the set of all functions $f$ such
that $\text{dom}\left({f}\right)\subseteq\text{V}^{(\mathbb{H})}_{\alpha}$,
for some $\alpha<\beta$, and $\text{img}\left({f}\right)\subseteq\mathbb{H}$.
Whenever $\mathbb{H}$ is a complete boolean algebra
$\left\langle\text{V}^{(\mathbb{H})},\left\llbracket\
\right\rrbracket_{\mathbb{H}}\right\rangle$ is a model of ZFC in the sense
that for each axiom $\sigma$ of ZFC,
$\left\llbracket\sigma\right\rrbracket_{\mathbb{H}}=1_{\mathbb{H}}$; more
generaly, if $\mathbb{H}$ is a complete Heyting algebra, then
$\left\langle\text{V}^{(\mathbb{H})},\left\llbracket\
\right\rrbracket_{\mathbb{H}}\right\rangle$ is a model IZF, the intuitionistic
counterpart of of ZFC.

On the other hand, it is well known that $\text{V}^{(\mathbb{H})}$ gives rise
to a localic topos, $\mathbf{Set}^{\left(\mathbb{H}\right)}$, that is
equivalent to the (Grothendieck) topos $\mathbf{Sh}\left(\mathbb{H}\right)$ of
all sheaves over the locale (= complete Heyting algebra) $\mathbb{H}$
([Bel05], [Bel88]). The objects of $\mathbf{Set}^{\left(\mathbb{H}\right)}$
are equivalence classes of members of $\text{V}^{(\mathbb{H})}$ and the arrows
are (equivalence classes of) members $f$ of $\text{V}^{(\mathbb{H})}$ such
that “$\text{V}^{(\mathbb{H})}$ believes, with probability $1_{\mathbb{H}}$,
that $f$ is a function”. A general topos encodes an internal (higher-order)
intuitionistic logic, given by the “forcing-like” Kripke-Joyal semantics, and
some form of (local) set-theory ([Bel88], [Bor08c]); a localic Grothendieck
topos is guided by a more well behaved internal logic and set theory.

All the considerations above concern to a fixed complete Heyting algebra
$\mathbb{H}$. However, to the best of our knowledge, there are very few
results on how Heyting-valued models are affected by the morphisms on the
complete Heyting algebras that determine them: the only cases found in the
literature ([Bel05]) are concerning automorphisms of complete Heyting algebras
and complete embeddings (_i.e_., injective Heyting algebra homomorphisms that
preserves arbitrary suprema and arbitrary infima). In the present work, we
consider and explore how more general kinds of morphisms between complete
Heyting algebras $\mathbb{H}$ and $\mathbb{H}^{\prime}$ induce arrows between
$\text{V}^{(\mathbb{H})}$ and $\text{V}^{(\mathbb{H}^{\prime})}$, and between
their corresponding Heyting toposes $\mathbf{Set}^{\left(\mathbb{H}\right)}$
($\simeq\mathbf{Sh}\left(\mathbb{H}\right)$) and
$\mathbf{Set}^{\left((\mathbb{H}^{\prime})\right)}$
($\simeq\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$). In more details: any
_geometric morphism_
$f^{*}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$,
(that automatically came from a unique locale morphism
$f:\mathbb{H}\to\mathbb{H}^{\prime}$), can be “lifted” to an arrow
$\tilde{f}:\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$.

#### Outline:

In Section 1 we provide the main definitions on sheaves over locales (=
complete Heyting algebras), topos and Heyting-valued models of IZF. Section 2
is devoted to present the equivalent descriptions of the categories of sheaves
over a locales, in particular establishing a connection between the cumulative
construction of Heyting valued models and localic toposes. Section 3 contains
the main results of this work: the “lifting” of all geometric morphisms
$f^{*}:\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$
to arrows
$\tilde{f}:\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$ and the
corresponding semantic preservation results. We end this work in Section 4
presenting some remarks on possible further developments.

##  1 Preliminaries

For the reader’s convenience, we provide here the main definitions and results
on topos and Heyting valued models of set theory. The main references for
category theory is [Lan98] and [Bor08a]; for topos theory [Bor08c] and [Bel88]
and for Boolean and Heyting valued models [Bel05].

###  1.1 Topos and Grothendieck Topos

If $\left\langle X,\mathcal{O}(X)\right\rangle$ is a topological space, then
the family of sets of continuous functions $({\cal
C}(U,\mathbb{R}))_{U\in\mathcal{O}(X)}$ has the property that, for any open
subset $U$ and any open covering $U=\bigcup_{i\in I}V_{i}$ then every family
of continuous functions $(f_{i}\in{\cal C}(V_{i},\mathbb{R}))_{i\in I}$ that
is compatible (${f_{i}}_{|V_{i}\cap V_{j}}={f_{j}}_{|V_{i}\cap V_{j}}$,
$\forall i,j\in I$), has a unique gluing $f\in{\cal C}(U,\mathbb{R})$
($f_{|V_{i}}=f_{i}$, $\forall i\in I$): This holds since the property of being
continuous is a local property; an analogous remark holds for the ${\cal
C}^{\infty}$ functions if $X$ is a smooth manifolds. Formally, this is
captured by the following:

######  Definition 1.1.

Let $\left\langle X,\mathcal{O}(X)\right\rangle$ be a topological space.
Regard the poset $(\mathcal{O}(X),\subseteq)$ as a category, a presheaf on $X$
is a functor $F:\mathcal{O}(X)^{op}\to\mathbf{Set}$. A sheaf on $X$ is a
presheaf $F$ such that, for every open $U\in\mathcal{O}(X)$ and every open
covering $\\{U_{i}\in\mathcal{O}(X)\mid i\in I\\}$ of $U$, the diagram below
is an equalizer:

${F(U)}$${\prod\limits_{i\in I}F(U_{i})}$${\prod\limits_{\left\langle
i,j\right\rangle\in I\times I}F(U_{i}\cap U_{j})}$

We denote the category of presheaves on $X$ by $\mathbf{Psh}\left(X\right)$
and the category of sheaves on $X$ by $\mathbf{Sh}\left(X\right)$.

Notice that the definition of a sheaf depends only on the lattice of opens,
therefore we may define presheaves and sheaves for any locale
$\left\langle\mathbb{H},\leq\right\rangle$, _i.e._ a complete lattice
satisfying the following distributive law:

$a\wedge\bigvee_{i\in I}c_{i}=\bigvee_{i\in I}a\wedge c_{i}.$

Locales are precisely the complete Heyting algebras, where

$a\rightarrow b=\bigvee\\{c\in\mathbb{H}:a\wedge c\leq b\\}.$

It is also possible to define sheaves in more general categories, using
Grothendieck topologies.

######  Definition 1.2.

Let $\mathcal{C}$ be a small category. A Grothendieck topology on
$\mathcal{C}$ is a function $J$ which assigns to each object
$c\in\text{Obj}\left(\mathcal{C}\right)$ a family $J(c)$ of sieves on $c$,
satisfying:

  1. 1.

Maximal sieve: $\bigcup\limits_{a\in\mathcal{C}_{0}}\mathcal{C}(a,c)\in J(c)$,
for all $c\in\text{Obj}\left(\mathcal{C}\right)$;

  2. 2.

Pullback stability: given $c\in\text{Obj}\left(\mathcal{C}\right)$, for every
$S\in J(c)$ and every arrow $f:a\to c$, the pullback $f^{\ast}S$ of the sieve
$S$ along $f$ is an element of $J(a)$;

  3. 3.

Transitivity: given $c\in\text{Obj}\left(\mathcal{C}\right)$ and $S\in J(c)$,
if $R$ is a sieve on $c$ such that $f^{\ast}R$ is a sieve on $a$ for every
$f:a\to c$ in $S$, then $R\in J(c)$.

We call the pair $(\mathcal{C},J)$ a (small) site.

Every locale $(\mathbb{H},\leq)$ gives rise to a Grothendieck topology: if
$c\in\mathbb{H}$, then $J(c)$ is the set of all coverings of $c$ that are
downward closed. Another important example is the Zariski topology in
algebraic geometry.

######  Definition 1.3.

Let $(\mathcal{C},J)$ be a site and $F:\mathcal{C}^{op}\to\mathbf{Set}$ a
presheaf. We say $F$ is a sheaf on $(\mathcal{C},J)$ if, for all
$c\in\text{Obj}\left(\mathcal{C}\right)$, every collection $\\{f_{i}:a_{i}\to
c\mid i\in I\\}\in J(c)$ and every $F$-compatible family $\\{s_{i}\in
F(a_{i})\mid i\in I\\}$, there exists a unique $s\in F(c)$ such that
$F(f_{i})(s)=s_{i}$, for all $i\in I$. We denote the category of sheaves on
$(\mathcal{C},J)$ by $\mathbf{Sh}\left(\mathcal{C},J\right)$.

A Grothendieck topos is a category which is equivalent to the topos of sheaves
on a site. Apart from categories of sheaves, the category of presheaves is
also an example of a Grothendieck topos.

Some properties of Grothendieck topos are of particular interest for
developing logic in the context of category theory, such as containing a
subobject classifier and being Cartesian closed.

######  Definition 1.4.

Given a category $\mathcal{C}$ with pullbacks, a subobject classifier in
$\mathcal{C}$ is a mono $\top:u\rightarrowtail\Omega$ satisfying: for every
other mono $m:a\rightarrowtail b$, there exists a unique $\chi_{m}:b\to\Omega$
such that the following diagram is a pullback:

######  Definition 1.5.

Let $\mathcal{C}$ be a locally small category with binary products. The
category $\mathcal{C}$ is called Cartesian closed if, for every
$b\in\text{Obj}\left(\mathcal{C}\right)$, the product functor $-\times b$ has
a right adjoint (the exponentiation functor $(-)^{b}$).

Both these properties are used to define a more general notion of topos:
elementary topos.

###  1.2 Localic Topos

######  Definition 1.6.

A topos is said to be localic if it is equivalent to the topos of sheaves on a
locale.

######  Theorem 1.7.

For a Grothendieck topos $\mathcal{T}$, the following conditions are
equivalent:

  1. 1.

$\mathcal{T}$ is a localic topos;

  2. 2.

the subobjects of the terminal object constitute a family of generators of
$\mathcal{T}$.

######  Theorem 1.8.

For a Grothendieck topos $\mathcal{T}$, the following conditions are
equivalent:

  1. 1.

$\mathcal{T}$ is a localic and Boolean topos;

  2. 2.

$\mathcal{T}$ satisfies the axiom of choice;

  3. 3.

$\mathcal{T}\simeq\mathbf{Sh}\left(\mathbb{B}\right)$, for some Boolean
algebra $\mathbb{B}$.

A continuous function between topological spaces defines a
$\left(\wedge,\bigvee\right)$-preserving morphism (_i. e._ , the left adjoint
of a morphism of locales) between the locales of open sets, and a geometric
morphism between the corresponding sheaf topos:

| $\qquad\mapsto\qquad$ |  | $\qquad\mapsto\qquad$ |
---|---|---|---|---

That is, $(\varphi_{\ast},\varphi^{\ast})$ is a pair of functors such that
$\varphi^{\ast}\dashv\varphi_{\ast}$ and $\varphi^{\ast}$ preserves finite
limits.

This mapping from the category of topological spaces to the category of topos
and geometric morphisms is not full nor faithful. However, the mapping from
the category of locales to the category of topos and geometric morphisms is
fully faithful:

######  Theorem 1.9.

The mapping below, given by $\varphi_{\ast}(F)=F\circ f^{\ast}$, for every
sheaf $F$ on $\mathbb{H}$,

| $\qquad\mapsto\qquad$ |
---|---|---

defines a fully faithful functor
$\mathbf{Sh}:\mathbf{Loc}\to\mathbf{Topos}_{geo}$.

###  1.3 Locale-Valued Models

######  Definition 1.10.

Locale-Valued Model

We define, for a locale $\mathbb{H}$, the universe of $\mathbb{H}$-names by
ordinal recursion. Given an ordinal $\alpha$ let

$\text{V}^{(\mathbb{H})}_{\alpha}=\left\\{f\in\mathbb{H}^{X}\mid\exists\beta<\alpha,X\subseteq\text{V}^{(\mathbb{H})}_{\beta}\right\\}$

It is readily seen that
$\text{V}^{(\mathbb{H})}_{\alpha}\subset\text{V}^{(\mathbb{H})}_{\alpha+1}$
and that for limit ordinals it is simply the union of the earlier stages. So
we let the (proper class) $\text{V}^{(\mathbb{H})}$ be defined as:

$\text{V}^{(\mathbb{H})}=\bigcup_{\alpha\in\operatorname{On}}\text{V}^{(\mathbb{H})}_{\alpha}$

Furthermore, we define for elements of this universe $\text{V}^{(\mathbb{H})}$
a function $\varrho\left(x\right)$ defined as:

$\varrho\left(x\right)=\min\left\\{\alpha\in\operatorname{On}\mid
x\in\text{V}^{(\mathbb{H})}_{\alpha}\right\\}$

Which is trivially well-founded.

######  Definition 1.11.

Atomic Formulas’ Values

We endow this class with two111Technically three. binary function on
$\mathbb{H}$, namely $\left\llbracket\cdot\in\cdot\right\rrbracket$ and
$\left\llbracket\cdot=\cdot\right\rrbracket$ defined by simultaneous recursion
on a well founded relation we’ll define now:

Given a Locale/complete Heyting algebra $\mathbb{H}$ define first:

$\left\langle x,y\right\rangle\prec\left\langle u,v\right\rangle\iff(x=u\land
y\in\text{dom}\left({v}\right))\lor(x\in\text{dom}\left({u}\right)\land y=v)$

We will later see that this is a well founded relation on
$\text{V}^{(\mathbb{H})}\times\text{V}^{(\mathbb{H})}$, for now belief
suffices and we shall define the three functions which we spoke of. By
recursion on $\prec$, define for pairs of elements in
$\text{V}^{(\mathbb{H})}$ the following:

$\displaystyle\left\llbracket\cdot\in\cdot\right\rrbracket:\text{V}^{(\mathbb{H})}$
$\displaystyle\times\text{V}^{(\mathbb{H})}\longrightarrow\mathbb{H}$
$\displaystyle\langle x$
$\displaystyle,y\rangle\longmapsto\bigvee_{u\in\text{dom}\left({y}\right)}y(u)\wedge\left\llbracket
x=u\right\rrbracket$

$\displaystyle\left\llbracket\cdot\ni\cdot\right\rrbracket:\text{V}^{(\mathbb{H})}$
$\displaystyle\times\text{V}^{(\mathbb{H})}\longrightarrow\mathbb{H}$
$\displaystyle\langle x$
$\displaystyle,y\rangle\longmapsto\bigvee_{v\in\text{dom}\left({x}\right)}x(v)\wedge\left\llbracket
v=y\right\rrbracket$

$\displaystyle\left\llbracket\cdot=\cdot\right\rrbracket:\text{V}^{(\mathbb{H})}$
$\displaystyle\times\text{V}^{(\mathbb{H})}\longrightarrow\mathbb{H}$
$\displaystyle\langle x$
$\displaystyle,y\rangle\longmapsto\bigwedge_{\begin{subarray}{c}u\in\text{dom}\left({y}\right)\\\
v\in\text{dom}\left({x}\right)\end{subarray}}\left(y(u)\rightarrow\left\llbracket
x\ni u\right\rrbracket\right)\wedge\left(x(v)\rightarrow\left\llbracket v\in
y\right\rrbracket\right)$

We call these the $\mathbb{H}$-values of the membership, co-membership and
equality, respectively.

Where ambiguity may arise, we shall make distinction between valuations of
different locale-valued models.

######  Proposition 1.12.

$\prec$ is well-founded as we claimed

Firstly, define
$\varrho^{\prime}\left(x,y\right)=\min\left\\{\varrho\left(x\right),\varrho\left(y\right)\right\\}$.
Now, take any subclass $X$ of
$\text{V}^{(\mathbb{H})}\times\text{V}^{(\mathbb{H})}$ and consider its image
under $\varrho^{\prime}$. For one, it has a minimum, due to the well-
orderedness of $\operatorname{On}$, let us call this minimum value $\alpha$
and one such pair that attains value $\alpha$ we shall name $\left\langle
x,y\right\rangle$ and — without loss of generality — we may impose on them
that $\varrho\left(x\right)=\alpha$, as otherwise we can consider the same
argument but swapping coordinates.

Suppose now there is some $\left\langle f,g\right\rangle$ such that
$\left\langle f,g\right\rangle\prec\left\langle x,y\right\rangle$. Thus, by
definition:

$(f\in\text{dom}\left({x}\right)\land g=y)\lor(f=x\land
g\in\text{dom}\left({y}\right))$

Now, breaking the disjunction we realize that the value of $\left\langle
f,g\right\rangle$ under $\varrho^{\prime}$ must be no more than $\alpha$:

$f\in\text{dom}\left({x}\right)\land g=y$
$\varrho^{\prime}\left(f,g\right)\leq\varrho^{\prime}\left(x,y\right)$
$f=x\land g\in\text{dom}\left({y}\right)$
$\varrho^{\prime}\left(f,g\right)\leq\varrho^{\prime}\left(x,y\right)$
$\varrho^{\prime}\left(f,g\right)\leq\varrho^{\prime}\left(x,y\right)$

But since $\alpha$ is minimal, it follows that they must be the same.
Therefore, it is impossible for $f$ to be in the domain of $x$, for then it
would have a smaller rank than $\alpha$. One is forced to conclude that, under
this assumption, $\left\langle f,g\right\rangle\prec\left\langle
x,y\right\rangle\rightarrow g\in\text{dom}\left({y}\right)$, and since it is
necessary that $f=x$. Consequently, — since the relation
$(\cdot\in\text{dom}\left({\cdot}\right))$ is well-founded — one is forced to
concede that if a descending $\prec$-chain does not stabilize so too will a
descending $(\cdot\in\text{dom}\left({\cdot}\right))$-chain, which would be
absurd. ∎

We are thus entitled to make the definition of those $\mathbb{H}$-values as we
previously claimed. The definitions of $\mathbb{H}$-values are then extended
to the class of the language of ${\mathcal{L}_{\in}}$-formulas enriched with
constant symbols for each member of the class $\text{V}^{(\mathbb{H})}$:

######  Definition 1.13.

$\mathbb{H}$-valuation of Formulas

We define the value of a ${{\mathcal{L}_{\in}}^{\mathbb{H}}}$-formula $\phi$
which is the language ${\mathcal{L}_{\in}}$ extended by constant symbols for
each element of $\text{V}^{(\mathbb{H})}$ the valuation
$\left\llbracket\phi\right\rrbracket$ inductively on the complexity of $\phi$.

$\left\llbracket\phi\right\rrbracket:({\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})})\to\mathbb{H}$

For an atomic formula $\phi$ involving only constants symbols as terms,
$\left\llbracket\phi\right\rrbracket$ is simply the value of the corresponding
function defined earlier, that is if $\phi\equiv aRb$ then, its valuation is
the constant function:

$\left\llbracket\phi\right\rrbracket=\left\llbracket aRb\right\rrbracket$

For atomic formulas with free variables, the valuation is — fittingly — a
function of the language’s variable symbols. Namely, given a function that
assigns values to its free variables it yields the value of the corresponding
valuation, ie. if $\phi\equiv x_{i}Rx_{j}$ for variable symbols $x_{i}$,
$x_{j}$.

$\displaystyle\left\llbracket\phi\right\rrbracket:\left({\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}\right)$
$\displaystyle\to\mathbb{H}$ $\displaystyle v$
$\displaystyle\mapsto\left\llbracket v(x_{i})Rv(x_{j})\right\rrbracket$

If $\phi$ has mixed constants and variable symbols, the definition is
analogous but fixing the constants, obviously.

When $\phi$ has free variables, we often write
$\left\llbracket\phi(x,y\cdots)\right\rrbracket$ to denote the function on its
free variables, rather than writing
$\left\llbracket\phi\right\rrbracket(\cdots)$.

For complex formulas, we define, for negation:

$\left\llbracket\neg\phi\right\rrbracket=\left\llbracket\phi\right\rrbracket\rightarrow\bot$

For a binary connective $*$ among $\rightarrow$, $\wedge$, $\vee$:

$\left\llbracket\phi*\psi\right\rrbracket=\left\llbracket\phi\right\rrbracket*\left\llbracket\psi\right\rrbracket$

Define now, given $x_{i}$ a variable symbol and $x\in\text{V}^{(\mathbb{H})}$
and a function
$v:{\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}$,
the function

$v_{[x_{i}\mid x]}(s)=\begin{cases}v(s)\text{, if }s\not=x_{i}\\\ x\text{,
otherwise}\end{cases}$

For quantifiers:

$\displaystyle\left\llbracket\forall
x_{i}:\phi\right\rrbracket:\left({\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}\right)$
$\displaystyle\to\mathbb{H}$ $\displaystyle v$
$\displaystyle\mapsto\bigwedge_{x\in\text{V}^{(\mathbb{H})}}\left\llbracket\phi\right\rrbracket\left(v_{[x_{i}\mid
x]}\right)$

And dualy,

$\displaystyle\left\llbracket\exists
x_{i}:\phi\right\rrbracket:\left({\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}\right)$
$\displaystyle\to\mathbb{H}$ $\displaystyle v$
$\displaystyle\mapsto\bigvee_{x\in\text{V}^{(\mathbb{H})}}\left\llbracket\phi\right\rrbracket\left(v_{[x_{i}\mid
x]}\right)$

Obviously, if two functions
$f,g:{\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}$
coincide on $\operatorname{free}_{\phi}$, then
$\left\llbracket\phi\right\rrbracket(f)=\left\llbracket\phi\right\rrbracket(g)$,
this gives also the fact that sentences are constant functions — and we will
often forget ourselves that these valuations are indeed functions of the
values we assign to the variable symbols of the formulas and concern ourselves
with sentences, which correspond to values in $\mathbb{H}$.

We also shall not draw a distiction between the constant symbols corresponding
to elements of $\text{V}^{(\mathbb{H})}$ and _the_ elements they correspond
to.

Thus we simply state the following results without proof — as their proofs can
be straightforwardly adapted from those on [Bel05]

######  Theorem 1.14.

Properties of Formula valuation

  1. 1.

$\left\llbracket x=x\right\rrbracket=1$.

  2. 2.

$\forall x\in\text{dom}\left({y}\right):y(x)\leq\left\llbracket x\in
y\right\rrbracket$.

  3. 3.

$\left\llbracket x=y\right\rrbracket=\left\llbracket y=x\right\rrbracket$.

  4. 4.

$\left\llbracket x\in y\right\rrbracket=\left\llbracket y\ni
x\right\rrbracket$.

  5. 5.

$\left\llbracket x=y\right\rrbracket\wedge\left\llbracket
y=z\right\rrbracket\leq\left\llbracket x=z\right\rrbracket$.

  6. 6.

$\left\llbracket x=y\right\rrbracket\wedge\left\llbracket y\in
z\right\rrbracket\leq\left\llbracket x\in z\right\rrbracket$.

  7. 7.

$\left\llbracket x\in y\right\rrbracket\wedge\left\llbracket
y=z\right\rrbracket\leq\left\llbracket x\in z\right\rrbracket$.

  8. 8.

$\left\llbracket x=y\right\rrbracket\wedge x(u)\leq\left\llbracket u\in
y\right\rrbracket$.

  9. 9.

$\left\llbracket
x=y\right\rrbracket\wedge\left\llbracket\varphi(x)\right\rrbracket=\left\llbracket
y=x\right\rrbracket\wedge\left\llbracket\varphi(y)\right\rrbracket$.

  10. 10.

$\left\llbracket\exists u\in
x:\varphi(u)\right\rrbracket=\bigvee_{u\in\text{dom}\left({x}\right)}x(u)\wedge\left\llbracket\varphi(u)\right\rrbracket$

  11. 11.

$\left\llbracket\forall u\in
x:\varphi(u)\right\rrbracket=\bigwedge_{u\in\text{dom}\left({x}\right)}x(u)\rightarrow\left\llbracket\varphi(u)\right\rrbracket$

Where $Qu\in x:\phi(u)$ is the usual shorthand for either $[\forall u:u\in
x\rightarrow\phi(u)]$ or $[\exists u:u\in x\land\phi(u)]$.

We then must define a “localic semantic”, or a notion of truth for that
structure so that we may claim that it actually models some form of set
theory.

######  Definition 1.15.

$\mathbb{H}$-Semantic / $\mathbb{H}$-Validity / Localic Semantic

We define a Tarskian-like $\vDash$ for each $\mathbb{H}$ to say:

$\text{V}^{(\mathbb{H})}\vDash\phi\iff\left\llbracket\phi\right\rrbracket=\top$

Since $\left\llbracket\phi\right\rrbracket$ is a function in disguise, to
properly make this comparison, it either must be constant or we must convert
$\top$ to the constantly tautological function. The latter allows us to
interpret formulas with free variables, and will assign them truth if they are
always true under any valuation.

We, thus, extend the notion for, given
$\sigma:{\operatorname{Vars}_{{\mathcal{L}_{\in}}^{\mathbb{H}}}}\to\text{V}^{(\mathbb{H})}$,

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\phi\iff\left\llbracket\phi\right\rrbracket(\sigma)=\top$

######  Proposition 1.16.

Some Properties of the Localic $\vDash$

  1. 1.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\varphi$ and
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\psi$ $\iff$
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\varphi\land\psi$

  2. 2.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\forall x:\varphi(x)$ $\iff$ for all
$X$, $\text{V}^{(\mathbb{H})}\vDash_{\sigma[x\mid X]}\varphi(x)$

  3. 3.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\exists x:\varphi(x)$ $\iff$ for all
$X$, $\text{V}^{(\mathbb{H})}\vDash_{\sigma[x\mid X]}\varphi(x)$

  4. 4.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\neg\varphi$ $\Rightarrow$
$\text{V}^{(\mathbb{H})}\not\vDash_{\sigma}\varphi$

  5. 5.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\varphi$ or
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\psi$ $\Rightarrow$
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\varphi\lor\psi$

  6. 6.

$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\psi$ or
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\neg\varphi$ $\Rightarrow$
$\text{V}^{(\mathbb{H})}\vDash_{\sigma}\varphi\rightarrow\psi$

Furthermore, modus ponens; generalization; instances of intuitionistic
tautology (or classical tautologies if $\mathbb{H}$ is Boolean) and the
intuitionistic first order logic axioms are all valid under the eyes of our
$\mathbb{H}$-validity.

In fact, $\mathbb{H}$-$\vDash$ is sound with respect to $\vdash$.

######  Remark.

The difference between the Tarskian and this Localic semantic is that some of
the biimplication that hold for Tarski do not in the non trivial
($\mathbb{H}=\left\\{0,1\right\\}$) case. Also, there is very little reason —
a priori — to expect there to be a witness to an existential formula, as it is
the arbitrary supremum of values of other formulas.

The supremum in existential formulas is attained by witnesses, but this relies
on the additional property of $\mathbb{H}$ being Boolean, otherwise holds only
an weaker statement.

There is, in fact, a canonical representation of elements of our universe $V$
and the many universes $\text{V}^{(\mathbb{H})}$. For the case
$\mathbb{H}=2=\left\\{0,1\right\\}$, this canonical representation establishes
a sort of model equivalence, has a good left inverse and is surjective modulus
$\text{V}^{(\mathbb{H})}$-equality with value $\top$.

######  Definition 1.17.

Immersion of $V$ in $\text{V}^{(\mathbb{H})}$

Define, $\in$-recursively:

${\hat{x}}=\left\\{\left\langle{\hat{y}},\top\right\rangle\mid y\in
x\right\\}$

Also, for $x\in\text{V}^{(2)}$ define
$(\cdot\in\text{dom}\left({\cdot}\right))$-recursively:

${\check{x}}=\left\\{{\check{y}}\mid y\in\text{dom}\left({x}\right)\land
x(y)=\top\right\\}$

######  Proposition 1.18.

The following hold:

  1. 1.

$\forall x,y:x\in
y\leftrightarrow\left\llbracket{\hat{x}}\in{\hat{y}}\right\rrbracket=1$

  2. 2.

$\forall
x^{\prime},y^{\prime}\in\text{V}^{(2)}:{\check{x^{\prime}}}\in{\check{y^{\prime}}}\leftrightarrow\left\llbracket
x^{\prime}\in y^{\prime}\right\rrbracket=1$

  3. 3.

$\forall
x,y:x=y\leftrightarrow\left\llbracket{\hat{x}}={\hat{y}}\right\rrbracket=1$

  4. 4.

$\forall
x^{\prime},y^{\prime}\in\text{V}^{(2)}:{\check{x^{\prime}}}={\check{y^{\prime}}}\leftrightarrow\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket=1$

  5. 5.

$\forall x:{\check{{\hat{x}}}}=x$

  6. 6.

$\forall
x^{\prime}\in\text{V}^{(2)}:\left\llbracket{\hat{{\check{x^{\prime}}}}}=x^{\prime}\right\rrbracket=1$

######  Corollary 1.19.

  1. 1.

$V\vDash_{\sigma}\phi\iff\text{V}^{(2)}\vDash_{{\hat{\\_}}\circ\sigma}\phi$

  2. 2.

$\phi\in\Sigma_{0}\Rightarrow\left[V\vDash_{\sigma}\phi\Rightarrow\text{V}^{(\mathbb{B})}\vDash_{{\hat{\\_}}\circ\sigma}\phi\right]$

  3. 3.

$\phi\in\Sigma_{1}\Rightarrow\left[V\vDash_{\sigma}\phi\Rightarrow\text{V}^{(\mathbb{B})}\vDash_{{\hat{\\_}}\circ\sigma}\phi\right]$

######  Theorem 1.20.

$\text{V}^{(\mathbb{H})}$ are models of Intuitionistic Set Theory. And
furthermore, if $\mathbb{H}$ is Boolean, it validates classical set theory and
the Axiom of Choice.

This is to say, for all $\phi$ axioms of the appropriate theory:

$\text{V}^{(\mathbb{H})}\vDash\phi$

This shall be stated without proof because it is rather well established
([Bel05]).

##  2 $\text{V}^{(\mathbb{H})}$V^(H) and Equivalent Descriptions of
$\mathbf{Sh}\left(\mathbb{H}\right)$Sh(H)

In this section, that is based on [Bel05] and [Bor08c], we present, for the
reader’s convenience, many equivalent description of category of sheaves of a
cHA $\mathbb{H}$,
$\mathbf{Sh}\left(\mathbb{H}\right)\simeq\mathbb{H}\text{-}\mathbf{Set}\simeq\mathbf{Set}^{\left(\mathbb{H}\right)}$,
where the later is obtained by the cumulative hierarchy $V^{(\mathbb{H})}$ by
taking quotients as below:

######  Definition 2.1.

Consider the equivalence relation in $\text{V}^{(\mathbb{H})}$ given by
$f\equiv g$ if, and only if, $\left\llbracket f=g\right\rrbracket=1$. The
category $\mathbf{Set}^{\left(\mathbb{H}\right)}$ is defined as:

$\text{Obj}\left(\mathbf{Set}^{\left(\mathbb{H}\right)}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\faktor{\text{V}^{(\mathbb{H})}}{\equiv}$
$\mathbf{Set}^{\left(\mathbb{H}\right)}\left([x],[y]\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{[\phi]\in\mathbf{Set}^{\left(\mathbb{H}\right)}\
\middle|\ \left\llbracket\text{fun}\left({\phi:x\to
y}\right)\right\rrbracket=1\right\\}$

The arrows do not depend on the choice of representative of the equivalence
classes $[x]$ and $[y]$. The composition and identity are defined as in
$\mathbf{Set}$.

######  Definition 2.2.

A $\mathbb{H}$-set is a pair $\left\langle X,\delta\right\rangle$ such that
$X$ is a set and $\delta:X\times X\to\mathbb{H}$ satisfies, for every
$x,y,z\in X$,

  1. 1.

$\delta(x,y)=\delta(y,x)$;

  2. 2.

$\delta(x,y)\wedge\delta(y,z)\leq\delta(x,z)$.

######  Definition 2.3.

A morphism $\phi:\left\langle X,\delta\right\rangle\to\left\langle
X^{\prime},\delta^{\prime}\right\rangle$ of $\mathbb{H}$-sets is a function
$\phi:X\times X^{\prime}\to\mathbb{H}$ such that, for all $x,y\in X$ e
$x^{\prime},y^{\prime}\in X^{\prime}$:

  1. 1.

$\delta^{\prime}(x^{\prime},y^{\prime})\wedge\phi(x,y^{\prime})\leq\phi(x,x^{\prime})$;

  2. 2.

$\delta(x,y)\wedge\phi(x,y^{\prime})\leq\phi(y,y^{\prime})$;

  3. 3.

$\phi(x,x^{\prime})\wedge\phi(x,y^{\prime})\leq\delta^{\prime}(x^{\prime},y^{\prime})$;

  4. 4.

$\bigvee\limits_{z^{\prime}\in X^{\prime}}\phi(x,z^{\prime})=\delta(x,x)$.

A morphism of $\mathbb{H}$-sets, then, can be understood as an
$\mathbb{H}$-valued functional relation.

Given morphisms $\phi:\left\langle X,\delta\right\rangle\to\left\langle
X^{\prime},\delta^{\prime}\right\rangle$ and $\psi:\left\langle
X^{\prime},\delta^{\prime}\right\rangle\to\left\langle
X^{\prime\prime},\delta^{\prime\prime}\right\rangle$ of $\mathbb{H}$-sets,
their composition $\psi\circ\phi$ is given by:

$(\psi\circ\phi)(x,x^{\prime\prime})=\bigvee\limits_{x^{\prime}\in
X^{\prime}}\phi(x,x^{\prime})\wedge\psi(x^{\prime},x^{\prime\prime})$

for all $x\in X,x^{\prime\prime}\in X^{\prime\prime}$. The identity morphism
$id_{\left\langle X,\delta\right\rangle}$ is the function such that:

$id_{\left\langle X,\delta\right\rangle}(x,y)=\delta(x,y),\text{ for all
}x,y\in X$

Thus, we can define the category $\mathbb{H}\text{-}\mathbf{Set}$, of
$\mathbb{H}$-sets and their morphisms.

One result on morphisms of $\mathbb{H}$-sets in particular will be useful for
us later on:

######  Proposition 2.4.

Given morphisms $\phi,\psi:\left\langle X,\delta\right\rangle\to\left\langle
X^{\prime},\delta^{\prime}\right\rangle$ of $\mathbb{H}$-sets, the following
conditions are equivalent:

  1. 1.

$\phi=\psi$;

  2. 2.

$\phi(x,x^{\prime})\leq\psi(x,x^{\prime})$, for all $x\in X$ and
$x^{\prime}\in X^{\prime}$.

######  Definition 2.5.

A singleton of an $\mathbb{H}$-set $\left\langle X,\delta\right\rangle$ is a
mapping $\sigma:X\to H$ such that, for every $x,y\in X$,

  1. 1.

$\sigma(x)\wedge\sigma(y)\leq\delta(x,y)$;

  2. 2.

$\sigma(x)\wedge\delta(x,y)\leq\sigma(y)$.

Notice that, given $x\in X$, the function $\sigma_{x}:X\to H$ such that
$\sigma_{x}(y)=\delta(x,y)$, for all $y\in H$, defines a singleton.

######  Definition 2.6.

Consider $\sigma(X)$ the collection of singletons of an $\mathbb{H}$-set
$\left\langle X,\delta\right\rangle$. $\left\langle X,\delta\right\rangle$ is
said to be complete if the function $\Upsilon:X\to\sigma(X)$, given by
$\Upsilon(x)=\sigma_{x}$, for all $x\in X$, is bijective. We denote the full
subcategory of complete $\mathbb{H}$-sets by
$\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$.

There is also an alternative description of complete $\mathbb{H}$-sets:

######  Proposition 2.7.

$\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$ is isomorphic to the category whose
objects are complete $\mathbb{H}$-sets and arrows are functions $f:X\to
X^{\prime}$ such that:

  1. 1.

$\delta(x,y)\leq\delta^{\prime}(f(x),f(y))$;

  2. 2.

$\delta(x,x)=\delta^{\prime}(f(x),f(x))$;

for all $x,y\in X$. The composition is given by usual function composition,
and the identity arrow is the identity function.

######  Theorem 2.8.

Let $\left\langle X,\delta\right\rangle$ be an $\mathbb{H}$-set. Define the
$\mathbb{H}$-set $\left\langle\sigma(X),\sigma(\delta)\right\rangle$ where

$\sigma(\delta)(\rho,\tau)=\bigvee\limits_{x\in X}\rho(x)\wedge\tau(x),\text{
for all }(\rho,\tau)\in\sigma(X)\times\sigma(X)$

Then, $\left\langle\sigma(X),\sigma(\delta)\right\rangle$ is complete and
isomorphic to $\left\langle X,\delta\right\rangle$.

The inverse isomorphisms $\phi:\left\langle
X,\delta\right\rangle\to\left\langle\sigma(X),\sigma(\delta)\right\rangle$ e
$\psi:\left\langle(\sigma(X),\sigma(\delta)\right\rangle\to\left\langle
X,\delta\right\rangle$ are given by:

$\phi(x,\rho)=\rho(x),\text{ for all }(x,\rho)\in X\times\sigma(X)$
$\psi(\rho,x)=\rho(x),\text{ for all }(\rho,x)\in\sigma(X)\times X$

######  Corollary 2.9.

There is an equivalence of categories
$\mathbb{H}\text{-}\mathbf{Set}\simeq\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$.

We can thereby define the functor
$\Gamma:\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$
by:

$\Gamma(F)=\left\langle X_{F},\delta_{F}\right\rangle,\text{ for all sheaf
}F\text{ on }\mathbb{H},\text{ where }X_{F}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\coprod\limits_{a\in\mathbb{H}}F(a)\text{
and}\\\ \delta_{F}\text{ is given by
}\left\langle(s,b),(t,c)\right\rangle\mapsto\bigvee\left\\{d\leq b\wedge c\mid
s\restriction^{b}_{d}=t\restriction^{c}_{d}\right\\}$
$\Gamma(\eta):\Gamma(F)\to\Gamma(G),\text{ for every natural transformation
}\eta:F\Rightarrow G\\\ \text{in
}\mathbf{Sh}\left(\mathbb{H}\right),\text{where
}\Gamma(\eta)(s,b)=(\eta_{b}(s),b),\text{ for all }(s,b)\in\Gamma(F)$

######  Theorem 2.10.

The functor
$\Gamma:\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$
defined above is fully faithful, and for all complete $\mathbb{H}$-set
$\left\langle X,\delta\right\rangle$ there exists a sheaf $F$ on $\mathbb{H}$
such that $\left\langle X,\delta\right\rangle\cong\Gamma(F)$. Therefore,
$\Gamma$ defines an equivalence of categories
$\mathbf{Sh}\left(\mathbb{H}\right)\simeq\mathbf{c}\mathbb{H}\text{-}\mathbf{Set}$.

Finally, to show the equivalence between $\mathbb{H}\text{-}\mathbf{Set}$ and
$\mathbf{Set}^{\left(\mathbb{H}\right)}$, two constructions in
$\text{V}^{(\mathbb{H})}$ (here we follow closely [Bel05]). Firstly, given
$x\in\text{V}$, we define its “natural representative” $\hat{x}$ in
$\text{V}^{(\mathbb{H})}$ using recursion over the (well-founded) membership
relation: $\hat{x}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\left\langle
y,1\right\rangle\mid y\in x\right\\}$. This allows us to define an ordered
pair in $\text{V}^{(\mathbb{H})}$: given $u,v\in\text{V}^{(\mathbb{H})}$,

$\left\\{u\right\\}^{(H)}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\left\langle
u,1\right\rangle\right\\}\hskip
113.81102pt\left\\{u,v\right\\}^{(H)}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{u\right\\}^{(H)}\cup\left\\{v\right\\}^{(H)}$
$\left\langle u,v\right\rangle^{(\mathbb{H})}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\left\\{u\right\\}^{(H)},\left\\{u,v\right\\}^{(H)}\right\\}^{(H)}$

Now let $\left\langle X,\delta\right\rangle$ be an $\mathbb{H}$-set. For each
$x\in X$, define $\dot{x}\in\text{V}^{(\mathbb{H})}$ as:

$\text{dom}\left({\dot{x}}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\hat{z}\mid
z\in X\right\\}\quad\text{ and }\quad\dot{x}(\hat{z})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\delta(x,z),\text{
for all }z\in X$

Then, define $X^{\dagger}\in\text{V}^{(\mathbb{H})}$ as

$\text{dom}\left({X^{\dagger}}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\dot{x}\mid
x\in X\right\\}\quad\text{ and }\quad X^{\dagger}(\dot{x})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\delta(x,x),\text{
for all }x\in X$

Similarly, given a morphism $\phi:\left\langle
X,\delta\right\rangle\to\left\langle X^{\prime},\delta^{\prime}\right\rangle$
of $\mathbb{H}$-sets, we may consider
$\varphi^{\dagger}\in\text{V}^{(\mathbb{H})}$ given by:

$\text{dom}\left({\phi^{\dagger}}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\\{\left\langle\dot{x},\dot{x}^{\prime}\right\rangle^{(\mathbb{H})}\
\middle|\ x\in X,x^{\prime}\in X^{\prime}\right\\}$
$\phi^{\dagger}\left(\left\langle\dot{x},\dot{x}^{\prime}\right\rangle^{(\mathbb{H})}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\phi(x,x^{\prime}),\text{
for all }x\in X,x^{\prime}\in X^{\prime}$

Since $\text{V}^{(\mathbb{H})}\models\text{fun}\left({\phi^{\dagger}}\right)$,
we may define a functor
$\Phi:\mathbb{H}\text{-}\mathbf{Set}\to\mathbf{Set}^{\left(\mathbb{H}\right)}$
by taking $\Phi(X,\delta)=\left[X^{\dagger}\right]$, for every
$\mathbb{H}$-set $\left\langle X,\delta\right\rangle$, and
$\Phi(\phi)=\phi^{\dagger}$, for every arrow $\phi$
$\mathbb{H}\text{-}\mathbf{Set}$.

On the other hand, given $u\in\text{V}^{(\mathbb{H})}$, define
$X_{u}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\text{dom}\left({u}\right)$
and $\delta_{u}:X_{u}\times X_{u}\to\mathbb{H}$ as

$\delta_{u}(x,y)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\llbracket
x\in u\right\rrbracket\wedge\left\llbracket
x=y\right\rrbracket\wedge\left\llbracket y\in u\right\rrbracket,\text{ for all
}x,y\in X_{u}$

Notice, however, that $\left\llbracket u=u^{\prime}\right\rrbracket=1$ does
not imply
$X_{u}=\text{dom}\left({u}\right)=\text{dom}\left({u^{\prime}}\right)=X_{u^{\prime}}$,
and that we may not define an $\mathbb{H}$-set using
$[\text{dom}\left({u}\right)]$ since this class is not a set (later we will
show that $\left\\{u^{\prime}\in\text{V}^{(H)}\mid\left\llbracket
u=u^{\prime}\right\rrbracket=1\right\\}$ is a proper class). In that case, we
will use Scott’s trick to define a functor
$\Psi:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbb{H}\text{-}\mathbf{Set}$.

Firstly, if $\left\llbracket u=u^{\prime}\right\rrbracket=1$, then
$\left\langle X_{u},\delta_{u}\right\rangle\cong\left\langle
X_{u^{\prime}},\delta_{u^{\prime}}\right\rangle$. Indeed, define
$\lambda_{u,u^{\prime}}:\left\langle
X_{u},\delta_{u}\right\rangle\to\left\langle
X_{u^{\prime}},\delta_{u^{\prime}}\right\rangle$ such that

$\lambda_{u,u^{\prime}}(x,x^{\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\llbracket
x\in u\right\rrbracket\wedge\left\llbracket
x=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket,\text{ for all
}x\in\text{dom}\left({u}\right),x^{\prime}\in\text{dom}\left({u^{\prime}}\right)$

We verify this is a morphism of $\mathbb{H}$-sets. Let $x,y\in X_{u}$ and
$x^{\prime},y^{\prime}\in X_{u^{\prime}}$.

  1. 1.

$\delta_{u^{\prime}}(x^{\prime},y^{\prime})\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})\leq\lambda_{u,u^{\prime}}(x,x^{\prime})$.
Indeed,

$\displaystyle\delta_{u^{\prime}}(x^{\prime},y^{\prime})$
$\displaystyle\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})=$
$\displaystyle=\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket\wedge\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket x=y^{\prime}\right\rrbracket$
$\displaystyle\leq\left\llbracket x\in u\right\rrbracket\wedge\left\llbracket
x=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket$
$\displaystyle=\lambda_{u,u^{\prime}}(x,x^{\prime})$

  2. 2.

$\delta_{u}(x,y)\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})\leq\lambda_{u,u^{\prime}}(y,y^{\prime})$.
Indeed,

$\displaystyle\delta_{u}(x,y)$
$\displaystyle\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})=$
$\displaystyle=\left\llbracket x\in u\right\rrbracket\wedge\left\llbracket
x=y\right\rrbracket\wedge\left\llbracket y\in
u\right\rrbracket\wedge\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket
x=y\right\rrbracket\wedge\left\llbracket y\in
u\right\rrbracket\wedge\left\llbracket
x=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket y\in
u\right\rrbracket\wedge\left\llbracket
y=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$
$\displaystyle=\lambda_{u,u^{\prime}}(y,y^{\prime})$

  3. 3.

$\lambda_{u,u^{\prime}}(x,x^{\prime})\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})\leq\delta_{u^{\prime}}(x^{\prime},y^{\prime})$.
Indeed,

$\displaystyle\lambda_{u,u^{\prime}}(x,x^{\prime})$
$\displaystyle\wedge\lambda_{u,u^{\prime}}(x,y^{\prime})=$
$\displaystyle=\left\llbracket x\in u\right\rrbracket\wedge\left\llbracket
x=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket
x=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket
x=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket\wedge\left\llbracket y^{\prime}\in
u^{\prime}\right\rrbracket$
$\displaystyle=\delta_{u^{\prime}}(x^{\prime},y^{\prime})$

  4. 4.

$\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}\lambda_{u,u^{\prime}}(x,z^{\prime})=\delta_{u}(x,x)$. Indeed,
using that $\delta_{u}(x,x)=\left\llbracket x\in u\right\rrbracket$,

     * •

on one hand, for every $z^{\prime}\in X_{u^{\prime}}$,

$\lambda_{u,u^{\prime}}(x,z^{\prime})=\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left\llbracket z^{\prime}\in
u^{\prime}\right\rrbracket\leq\left\llbracket x\in u\right\rrbracket$

Therefore, $\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}\lambda_{u,u^{\prime}}(x,z^{\prime})\leq\delta_{u}(x,x)$;

     * •

on the other hand, for every $z\in X_{u^{\prime}}$,

$u^{\prime}(z^{\prime})\wedge\left\llbracket
z^{\prime}=x\right\rrbracket=\left\llbracket
x=z^{\prime}\right\rrbracket\wedge u^{\prime}(z^{\prime})\wedge\left\llbracket
z^{\prime}=z^{\prime}\right\rrbracket\leq\\\ \leq\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left(\bigvee\limits_{t^{\prime}\in
X_{u^{\prime}}}u^{\prime}(t^{\prime})\wedge\left\llbracket
t^{\prime}=z^{\prime}\right\rrbracket\right)=\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left\llbracket z^{\prime}\in
u^{\prime}\right\rrbracket$

Thus,

$\left\llbracket x\in u^{\prime}\right\rrbracket=\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}u^{\prime}(z^{\prime})\wedge\left\llbracket
z^{\prime}=x\right\rrbracket\leq\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left\llbracket z^{\prime}\in
u^{\prime}\right\rrbracket$

But observe that $\left\llbracket u=u^{\prime}\right\rrbracket=1$ implies
$\left\llbracket x\in u\right\rrbracket=\left\llbracket x\in
u^{\prime}\right\rrbracket$, so:

$\displaystyle\left\llbracket x\in u\right\rrbracket$
$\displaystyle=\left\llbracket x\in u\right\rrbracket\wedge\left\llbracket
x\in u^{\prime}\right\rrbracket$ $\displaystyle\leq\left\llbracket x\in
u\right\rrbracket\wedge\left(\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left\llbracket z^{\prime}\in
u^{\prime}\right\rrbracket\right)$
$\displaystyle=\bigvee\limits_{z^{\prime}\in X_{u^{\prime}}}\left\llbracket
x\in u\right\rrbracket\wedge\left\llbracket
x=z^{\prime}\right\rrbracket\wedge\left\llbracket z^{\prime}\in
u^{\prime}\right\rrbracket$

That is, $\delta_{u}(x,x)\leq\bigvee\limits_{z^{\prime}\in
X_{u^{\prime}}}\lambda_{u,u^{\prime}}(x,z^{\prime})$.

Finally, we verify that $\lambda_{u,u^{\prime}}$ is an isomorphism, with
inverse morphism
$\lambda_{u,u^{\prime}}^{-1}=\lambda_{u^{\prime},u}:\left\langle
X_{u^{\prime}},\delta_{u^{\prime}}\right\rangle\to\left\langle
X_{u},\delta_{u}\right\rangle$. For all $x,y\in X_{u}$,

$(\lambda_{u^{\prime},u}\circ\lambda_{u,u^{\prime}})(x,y)=\bigvee\limits_{x^{\prime}\in
X_{u^{\prime}}}\lambda_{u,u^{\prime}}(x,x^{\prime})\wedge\lambda_{u^{\prime},u}(x^{\prime},y)=\\\
=\bigvee\limits_{x^{\prime}\in X_{u^{\prime}}}\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\wedge\left\llbracket y\in
u\right\rrbracket\wedge\left\llbracket
y=x^{\prime}\right\rrbracket\wedge\left\llbracket x^{\prime}\in
u^{\prime}\right\rrbracket\leq\\\ \leq\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket
x=y\right\rrbracket\wedge\left\llbracket y\in
u\right\rrbracket=\delta_{u}(x,y)$

Therefore, using proposition 2.4, we conclude that
$\lambda_{u^{\prime},u}\circ\lambda_{u,u^{\prime}}=id_{\left\langle
X,\delta\right\rangle}$. Analogously, it can be verified that
$\lambda_{u,u^{\prime}}\circ\lambda_{u^{\prime},u}=id_{\left\langle
X^{\prime},\delta^{\prime}\right\rangle}$.

Now, for each $[u]\in\mathbf{Set}^{\left(\mathbb{H}\right)}$, let $I^{[u]}$ be
the category given by:

$\text{Obj}\left(I^{[u]}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=[u]_{m}\qquad\qquad\text{Arr}\left(I^{[u]}\right)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=[u]_{m}\times[u]_{m}$

where $[u]_{m}$ is the equivalence class of the elements with minimum rank.
Consider the functor $F^{[u]}:I^{[u]}\to\mathbb{H}\text{-}\mathbf{Set}$ such
that

$F^{[u]}(u^{\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\langle
X_{u},\delta_{u}\right\rangle,\text{ for all }u^{\prime}\in[u]_{m}$
$F^{[u]}(u^{\prime},u^{\prime\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\lambda_{u^{\prime},u^{\prime\prime}}:\left\langle
X_{u^{\prime}},\delta_{u^{\prime}}\right\rangle\to\left\langle
X_{u^{\prime\prime}},\delta_{u^{\prime\prime}}\right\rangle,\text{ for all
}u^{\prime},u^{\prime\prime}\in[u]_{m}$

At last, we may define the functor
$\Psi:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbb{H}\text{-}\mathbf{Set}$
as $\Psi([u])=\lim\limits_{u^{\prime}\in[u]_{m}}F^{[u]}(u^{\prime})$.

We may also describe this functor more explicitly. The product of a family of
$\mathbb{H}$-sets $\left\\{\left\langle X_{i},\delta_{i}\right\rangle\mid i\in
I\right\\}$ is given by $\left\langle P,\delta\right\rangle$, where the set is
simply the cartesian product $P=\prod\limits_{i\in I}X_{i}$ and
$\delta:P\times P\to\mathbb{H}$ is given by:

$\delta\left(\left\langle x_{i}\right\rangle_{i\in I},\left\langle
x_{i}^{\prime}\right\rangle_{i\in I}\right)=\bigwedge\limits_{i\in
I}\delta(x,x^{\prime})$

The projections $\pi_{j}:P\times X_{j}\to\mathbb{H}$ are given by

$\pi_{j}\left(\left\langle x_{i}\right\rangle_{i\in
I},x^{\prime}_{j}\right)=\delta_{j}(x_{j},x^{\prime}_{j})$

for each $j\in I$ (see [Bor08c], exercise 2.13.15). The equalizer of two
morphisms $\phi,\psi:\left\langle X,\delta\right\rangle\to\left\langle
X^{\prime},\delta^{\prime}\right\rangle$ of $\mathbb{H}$-sets is $\left\langle
X,\tau\right\rangle$, where

$\tau(x,y)=\bigvee\limits_{x^{\prime}\in
X^{\prime}}\phi(x,x^{\prime})\wedge\psi(y,x^{\prime})$

(see [Bor08c], exercise 2.13.16)

We can then use the construction of limits by products and equalizers (see
[Bor08a], theorem 2.8.1), denoting $\Psi([u])$ by $\lim F^{[u]}$: where
$\pi^{\prime},\pi^{\prime\prime}$ are the projections (of the corresponding
products) and $\left\langle\lim F,E\right\rangle$ is the equalizer of $\alpha$
and $\beta$, which are the morphisms that make the diagram commute. That is,

$\pi^{\prime\prime}_{(u^{\prime},u^{\prime\prime})}\circ\alpha=\pi^{\prime}_{u^{\prime\prime}}\qquad\qquad\qquad\pi^{\prime\prime}_{(u^{\prime},u^{\prime\prime})}\circ\beta=\lambda_{u^{\prime},u^{\prime\prime}}\circ\pi^{\prime}_{u^{\prime}}$

We can proceed similarly for the arrows of the category. For each
$f\in\text{V}^{(\mathbb{H})}$ such that
$\left\llbracket\text{fun}\left({f:u\to v}\right)\right\rrbracket=1$, define
$\lambda_{f}:\left\langle X_{u},\delta_{u}\right\rangle\to\left\langle
X_{v},\delta_{v}\right\rangle$ as:

$\lambda_{f}(x,y)=\left\llbracket x\in
u\right\rrbracket\wedge\left\llbracket(x,y)\in
f\right\rrbracket\wedge\left\llbracket y\in v\right\rrbracket$

Now, given $f^{\prime}\in\text{V}^{(\mathbb{H})}$ such that
$\left\llbracket\text{fun}\left({f^{\prime}:u^{\prime}\to
v^{\prime}}\right)\right\rrbracket=1$ and $\left\llbracket
f=f^{\prime}\right\rrbracket=1$ (which already implies $u\equiv u^{\prime}$
and $v\equiv v^{\prime}$), we obtain the following commutative diagram: Thus,
we may define an arrow
$\Psi([f]):\lim\limits_{u^{\prime}\in[u]_{m}}F(u^{\prime})\to\lim\limits_{v^{\prime}\in[v]_{m}}F(v^{\prime})$.

######  Theorem 2.11.

The functors $\Phi,\Psi$ constructed above define an equivalence of
categories:
$\mathbb{H}\text{-}\mathbf{Set}\simeq\mathbf{Set}^{\left(\mathbb{H}\right)}$.

##  3 Induced morphisms in Heyting valued models

Previously, we saw (see Definition 1.17) an injection
$V\to\text{V}^{(\mathbb{B})}$ given by $\hat{\cdot}$ which preserves the truth
values of $\Sigma_{1}$ formulas (see Corollary 1.19). Currently, it is known
that if $\phi:\mathbb{A}\to\mathbb{B}$ is a complete and injective morfism of
Heyting algebras, we can define a map
$\tilde{\phi}:\text{V}^{(\mathbb{A})}\to\text{V}^{(\mathbb{B})}$ that is
injective and such that: for all $x,y\in\text{V}^{(\mathbb{A})}$,

$\phi\left\llbracket
x=y\right\rrbracket_{\mathbb{A}}=\left\llbracket\tilde{\phi}(x)=\tilde{\phi}(y)\right\rrbracket_{\mathbb{B}}$
$\phi\left\llbracket x\in
y\right\rrbracket_{\mathbb{A}}=\left\llbracket\tilde{\phi}(x)\in\tilde{\phi}(y)\right\rrbracket_{\mathbb{B}}$

For $\Delta_{0}$ formulas, the equality, trivially, still holds. One gets the
following inequalities for any $\Sigma_{1}$ formula $\psi$:

$\phi\left\llbracket\psi(x_{1}\cdots
x_{n})\right\rrbracket_{\mathbb{A}}\leq\left\llbracket\psi(\tilde{\phi}(x_{1})\cdots\tilde{\phi}(x_{n}))\right\rrbracket_{\mathbb{B}}$
$\phi\left\llbracket\psi(x_{1}\cdots
x_{n})\right\rrbracket_{\mathbb{A}}\leq\left\llbracket\psi(\tilde{\phi}(x_{1})\cdots\tilde{\phi}(x_{n}))\right\rrbracket_{\mathbb{B}}$

It is relatively straight forward to relax these conditions to injective
functions that preserve only arbitrary suprema and finite infima222 Geometric
morphisms or Locale morphisms, which are related to Topoi and Sheaves over
Locales. , one obtains the useful inequalities:

$\phi\left\llbracket
x=y\right\rrbracket_{\mathbb{A}}\leq\left\llbracket\tilde{\phi}(x)=\tilde{\phi}(y)\right\rrbracket_{\mathbb{B}}$
$\phi\left\llbracket x\in
y\right\rrbracket_{\mathbb{A}}\leq\left\llbracket\tilde{\phi}(x)\in\tilde{\phi}(y)\right\rrbracket_{\mathbb{B}}$

And we still have the inequalities for $\Sigma_{1}$ formulas.

Our current efforts were in providing a possible generalization of this
construction for non-injective maps that preserve arbitrary suprema and finite
infima. In this section we shall focus ourselves in this theme and some of the
difficulties we faced in the process. The reason for our search is that it is
taken as fact that the category of Heyting/Boolean valued models is related
other categories endowed with these morphisms.

Despite us having a _horizontal_ connection between models and topoi:

$\mathbb{H}\rightsquigarrow\text{V}^{(\mathbb{H})}\rightsquigarrow\mathbf{Set}^{(\mathbb{H})}\simeq\mathbb{H}\text{-}\mathbf{Set}$

The vertical connection between arrows from
$\mathbb{H}\to\mathbb{H}^{\prime}$,
$\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$, etc. does not
seem to have been widely explored in the literature; the only considered cases
were automorphisms of complete Boolean algebra, complete monomorphisms between
complete Boolean algebras (see exercise 3.12 in [Bel05]) and retractions to
them associated (see chapter 3 of [Gui13]). This motivated us to study how we
could induce arrows between models from more general arrows between complete
Heyting algebras.

In this section we present the main results of the present work, we consider
and explore how more general kinds of morphisms between complete Heyting
algebras $\mathbb{H}$ and $\mathbb{H}^{\prime}$ induce arrows between
$V^{\mathbb{H}}$ and $V^{\mathbb{H}^{\prime}}$, and between their
corresponding Heyting toposes
$\mathbf{Set}^{\left(\mathbb{H}\right)}(\simeq\mathbf{Sh}\left(\mathbb{H}\right))$
and
$\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}(\simeq\mathbf{Sh}\left(\mathbb{H}^{\prime}\right))$.
In more details: any geometric morphism
$f^{*}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$,
(that automatically came from a unique locale morphism
$f:\mathbb{H}\to\mathbb{H}^{\prime}$), can be “lifted” to an arrow
$\tilde{f}:V^{\mathbb{H}}\to V^{\mathbb{H}^{\prime}}$.

In the remainder of the section, $\mathbb{H}$, $\mathbb{H}^{\prime}$,
$\mathbb{A}$ and $\mathbb{B}$ shall be complete Heyting algebras, and
$f:\mathbb{A}\to\mathbb{B}$ shall be a locale morphism (notation:
$f\in\mathbf{Loc}(\mathbb{A},\mathbb{B})$), i.e., $f$ is a function that
preserves arbitrary suprema and finite infima.

###  3.1 Induced morphisms

######  Definition 3.1.

(First proposal) We define by recursion a family

$\left\\{\tilde{f}_{\alpha}:\text{V}^{(\mathbb{H})}_{\alpha}\rightharpoonup\text{V}^{(\mathbb{H}^{\prime})}_{\alpha}\
\middle|\ \alpha\in\operatorname{On}\right\\}$

where $\rightharpoonup$ indicates that $\tilde{f}_{\alpha}$ are “semi-
functions” (that is, for all $x\in\text{V}^{(\mathbb{H})}_{\alpha}$, there
exists $x^{\prime}\in\text{V}^{(\mathbb{H}^{\prime})}$ such that $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$), the following way: for every
$\alpha\in\operatorname{On}$ and every $\left\langle
x,x^{\prime}\right\rangle\in\text{V}^{(\mathbb{H})}_{\alpha}\times\text{V}^{(\mathbb{H}^{\prime})}$,
$\left\langle x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$ if, and only if,
there exists a surjection
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
such that $\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}_{\varrho(x)}$ for all
$u\in\text{dom}\left({x}\right)$, and the following diagram commutes: Under
these conditions, we say that $\varepsilon$ witnesses $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$. Note that, if we suppose (by
induction) that $\tilde{f}_{\beta}$ is defined for every $\beta<\alpha$, then
the semi-function
$\tilde{f}_{\varrho(x)}:\text{V}^{(\mathbb{H})}_{\varrho(x)}\rightharpoonup\text{V}^{(\mathbb{H}^{\prime})}_{\varrho(x)}$
is defined, therefore
$\text{dom}\left({x^{\prime}}\right)\subseteq\text{V}^{(\mathbb{H}^{\prime})}_{\varrho(x)}$
and $x^{\prime}\in\text{V}^{(\mathbb{H}^{\prime})}_{\alpha}$.

Thus, we define $\tilde{f}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\bigcup\limits_{\alpha\in\operatorname{On}}\tilde{f}_{\alpha}$
and

$dom\left(\tilde{f}\right)=\bigcup\limits_{\alpha\in\operatorname{On}}dom\left(\tilde{f}_{\alpha}\right)=\bigcup\limits_{\alpha\in\operatorname{On}}\text{V}^{(\mathbb{H})}_{\alpha}=\text{V}^{(\mathbb{H})}$

so that $\tilde{f}$ is also a semi-function
$\tilde{f}:\text{V}^{(\mathbb{H})}\rightharpoonup\text{V}^{(\mathbb{H}^{\prime})}$.

######  Proposition 3.2.

If $f$ is injective, then, for all $\alpha\in\operatorname{On}$,
$\tilde{f}_{\alpha}$ is an injective function.

###### Proof.

By induction. Suppose that $\tilde{f}_{\beta}$ is an injective function, for
all $\beta<\alpha$, and let $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$. Then,
$\varepsilon=\tilde{f}_{\varrho(x)}\restriction:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
is a bijection, because it’s surjective by definition, and, since
$\left\langle u,\varepsilon(u)\right\rangle\in\tilde{f}_{\varrho(x)}$ for all
$u\in\text{dom}\left({x}\right)$, the induction hypothesis implies that
$\varepsilon=\tilde{f}_{\varrho(x)}\restriction$ is injective. Therefore,
using the commutative diagram from the definition, $x^{\prime}$ is uniquely
determined by $x^{\prime}=f\circ x\circ\varepsilon^{-1}$, that is,
$\tilde{f}_{\alpha}$ is a function. Besides, if $x\neq y$ (in
$\text{V}^{(\mathbb{H})}_{\alpha}$), then $f$ being injective implies

$\tilde{f}_{\alpha}(x)=f\circ x\circ\varepsilon^{-1}\neq f\circ
y\circ\varepsilon^{-1}=\tilde{f}_{\alpha}(y)$

so that $\tilde{f}_{\alpha}$ is also injective. ∎

Hence, this function covers the result stated in [Bel05], exercise 3.12.

######  Remark.

Naive attempts to extend this initial proposal are fated to fail, for in the
absence of injectivity, the defined relation is not a function.

In fact, notice that definition 3.1 presents a serious problem: it does not
guarantee that
$\text{dom}\left({\tilde{f}}\right)_{\alpha}=\text{V}^{(\mathbb{H})}_{\alpha}$,
for each $\alpha\in\operatorname{On}$. For example, consider the Boolean
algebras $\mathbf{2}=\\{0,1\\}$ and $\mathbf{4}=\\{0,a,\neg a,1\\}$ (with
$0\neq a\neq 1$) and the function $f:\mathbf{4}\to\mathbf{2}$ given by
$f(a)=0$ and $f(\neg a)=1$. Firstly,

$\text{V}^{(\mathbf{4})}_{0}=\emptyset$ | $\text{V}^{(\mathbf{2})}_{0}=\emptyset$
---|---
$\text{V}^{(\mathbf{4})}_{1}=\\{\emptyset\\}$ | $\text{V}^{(\mathbf{2})}_{1}=\\{\emptyset\\}$
$\text{V}^{(\mathbf{4})}_{2}=\big{\\{}\\{(\emptyset,0)\\},\\{(\emptyset,1)\\},\\{(\emptyset,a)\\},\\{(\emptyset,\neg a)\\}\big{\\}}$ |  $\text{V}^{(\mathbf{2})}_{2}=\big{\\{}\\{(\emptyset,0)\\},\\{(\emptyset,1)\\}\big{\\}}$

Let $x\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\big{\\{}\big{(}\left\\{(\emptyset,0)\right\\},0\big{)}\big{\\}},\big{(}\left\\{(\emptyset,a)\right\\},1\big{)}\big{\\}}$,
$u\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\\{(\emptyset,0)\\}$
and $v\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\\{(\emptyset,1)\\}$.
It can be easily verified that $\\{(\emptyset,0)\\}$ is the only element of
$\text{V}^{(\mathbf{2})}_{2}$ such that $\left\langle
u,\\{(\emptyset,0)\\}\right\rangle,\left\langle
v,\\{(\emptyset,0)\\}\right\rangle\in\tilde{f}_{2}$.

Thus, consider $x^{\prime}\in\text{V}^{(\mathbf{2})}$ and suppose there exists
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
such that $\left\langle u,\varepsilon(u)\right\rangle,\left\langle
v,\varepsilon(v)\right\rangle\in\tilde{f}_{2}$, _i. e._
$\varepsilon(u)=\varepsilon(v)=\\{(\emptyset,0)\\}$. But in this case, we
cannot guarantee the diagram in the definition commutes, since we would have:

$0=\varphi(x(u))=x^{\prime}(\varepsilon(u))=x^{\prime}(\varepsilon(v))=\varphi(x(v))=1$

Therefore, there does not exist $x^{\prime}\in\text{V}^{(\mathbf{2})}$ such
that $\left\langle x,x^{\prime}\right\rangle\in\tilde{f}_{3}$.

To deal with this issue, we add more elements to the image of the semi-
function, closing it by the equivalence relation $\equiv$ (another option
would be to close the images only for the equivalent members with minimum
rank).

######  Definition 3.3.

Generalized Connection between $\text{V}^{(\mathbb{H})}$s

Let $\phi\in\mathbf{Loc}(\mathbb{A},\mathbb{B})$. Define the following
compatible family of relations by ordinal recursion:

$\displaystyle x\mathrel{\tilde{\phi}_{\alpha}}y\iff$
$\displaystyle\exists(\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({y}\right)):(y\circ\varepsilon=\phi\circ
x)\land$ $\displaystyle\forall u\in\text{dom}\left({x}\right):\exists
v\in\text{V}^{(\mathbb{B})}:\exists\beta<\alpha:(u\mathrel{\tilde{\phi}}_{\beta}v)\land\left\llbracket
v=\varepsilon(u)\right\rrbracket=1$

$\tilde{\phi}=\bigcup_{\alpha\in\operatorname{On}}\tilde{\phi}_{\alpha}$

This definition in particular was used because of the following: The
requirement of existence of a surjective function is due to our need that
every object that is related to $x$ has its (domain’s) elements determined by
elements of (the domain of) $x$. This is true in the injective case, where the
function is the witness of this existential. In the non-injective case,
$\varepsilon$ “essencially”333Up to
$\left\llbracket\cdot=\cdot\right\rrbracket=1$-equivalence. is going to be a
“piece” or “fragment” of $\tilde{\phi}$ that happens to be a function and
behaves _similarly_ to how $\tilde{\phi}$ would if $\phi$ was injective.

We demand that $y\circ\varepsilon=\phi\circ x$, to extend the original idea of
the construction by injective morfisms to more general ones:
$\tilde{\phi}(x)(\tilde{\phi}(u))=(\phi\circ x)(u)$. If $y$ is related to $x$,
then there is a function fragment of $\tilde{\phi}$ which makes the above
commute.

It is, however, not enough to ask only this, for one such $y$ could be chosen
ad hod without the members of its domain being related to the members of
$x$’s. There is no hope for us to attain the imposed conditions of
inequalities of atomic formulas, which depend recursively on the domains of
the involved objects, if we do not impose some similarly recursive demands for
the relation.

Thus, the final condition says that for every member $u$ of $x$’s domain,
there was some $u$ in some previous step which to which it was related. Surely
$\tilde{\phi}$ is only very rarely a function, but after taking the quotient
by $\left\llbracket\cdot=\cdot\right\rrbracket$-equivalence it is a function.

Were we to remove $\left\llbracket v=\varepsilon(u)\right\rrbracket=1$, and
simply require that $u\mathrel{\tilde{\phi}}_{\beta}\varepsilon(u)$, the
definition would coincide for injective functions, but in general the domain
of $\tilde{\phi}$ as a relation would not be total, i.e. it wouldn’t be all of
$\text{V}^{(\mathbb{A})}$.

######  Theorem 3.4.

$\tilde{\phi}$’s domain is total

This is: for all morfism $\phi:\mathbb{A}\to\mathbb{B}$,

$\forall x\in\text{V}^{(\mathbb{A})}:\exists
x^{\prime}\in\text{V}^{(\mathbb{B})}:x\mathrel{\tilde{\phi}}x^{\prime}$

###### Proof.

The proof follows from the 2 facts below:

######  Fact 3.5.

Suppose that $\forall
u\in\text{dom}\left({x}\right):\forall\kappa\in\operatorname{On}:\exists(u^{\prime}:\kappa\rightarrowtail{\text{V}^{(\mathbb{B})}}):\forall\alpha<\kappa:u\mathrel{\tilde{\phi}}u^{\prime}_{\alpha}$.
In this case, it is trivial to see that there is an
$X^{\prime}\subset\text{V}^{(\mathbb{B})}$ such that there is a bijection
$\varepsilon:\text{dom}\left({x}\right)\to\text{dom}\left({x^{\prime}}\right)=X^{\prime}$
such that $\forall
u\in\text{dom}\left({x}\right):u\mathrel{\tilde{\phi}}\varepsilon(u)$.

Thus, let $x^{\prime}=\phi\circ x\circ\varepsilon^{-1}$. It is evident that
$x\mathrel{\tilde{\phi}}x^{\prime}$.

Therefore, if there exists a proper class of elements to the right of every
member of the domain of $x$, then there is some $x^{\prime}$ such that
$x\mathrel{\tilde{\phi}}x^{\prime}$.

######  Fact 3.6.

Suppose that $x\not=\emptyset$ and that $\exists
x^{\prime}\in\text{V}^{(\mathbb{B})}:x\mathrel{\tilde{\phi}}x^{\prime}$. Let
$u\in\text{dom}\left({x}\right)$, $u\in\text{dom}\left({x^{\prime}}\right)$
such that $u\mathrel{\tilde{\phi}}u^{\prime}$ and consider
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
witnessing $x\mathrel{\tilde{\phi}}x^{\prime}$.

Trivially,

$\exists\alpha\in\operatorname{On}:\forall\xi>\alpha:\forall
t^{\prime}:=\left[u^{\prime}\cup\left\\{\left\langle\hat{\xi},0\right\rangle\right\\}\right]\rightarrow\left\llbracket
t^{\prime}=u^{\prime}\right\rrbracket=1$

Simply because we are adding some object which was not in the domain of
$u^{\prime}$ whose value under $t$ will be $0$, and in the equality, the $0$
will be in the antecedent of the implication.

So, for each ordinal bigger than $\alpha$, we obtain a different set which is
equal to $u^{\prime}$ with “probability” $1$, and thus, $x$ must have a proper
class of elements $y$ such that $x\mathrel{\tilde{\phi}}y$.

Joining the previous results, we have:

$\forall x\in\text{V}^{(\mathbb{A})}:x\not=\emptyset\rightarrow([\forall
u\in\text{dom}\left({x}\right):\exists
u^{\prime}:u\mathrel{\tilde{\phi}}u^{\prime}]\rightarrow\exists
x^{\prime}:x\mathrel{\tilde{\phi}}x^{\prime})$

As the consequent is true when $x=\emptyset$ — for
$\emptyset\mathrel{\tilde{\phi}}\emptyset$ — we have:

$\forall x\in\text{V}^{(\mathbb{A})}:[\forall
u\in\text{dom}\left({x}\right):\exists
u^{\prime}:u\mathrel{\tilde{\phi}}u^{\prime}]\rightarrow\exists
x^{\prime}:x\mathrel{\tilde{\phi}}x^{\prime}$

By regularity:

$\forall x\in\text{V}^{(\mathbb{A})}:\exists
x^{\prime}:x\mathrel{\tilde{\phi}}x^{\prime}$

∎

Alternatively, we could suppose in the Definition 3.1 the that $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$ if, and only if, there exists
a witness
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
as in the original definition, and, for all $u\in\text{dom}\left({x}\right)$,
there exists $u^{\prime}\in\text{V}^{(\mathbb{H}^{\prime})}$ such that
$\left\langle u,u^{\prime}\right\rangle\in\tilde{f}_{\varrho(x)}$ and
$\left\llbracket\varepsilon(u)=u^{\prime}\right\rrbracket^{\prime}=1^{\prime}$.

We choose the first condition mentioned above to our final definition, however
all are equivalent in the quotient by $\equiv$.

Definition 3.1 (complement) Adding to the original definition, we also suppose
that if $\left\langle x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$ (that
is, there exists a witness for that) and $\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket^{\prime}=1^{\prime}$, then $\left\langle
x,y^{\prime}\right\rangle\in\tilde{f}_{\alpha}$.

######  Remark.

We observe that $\text{V}^{(\mathbb{H})}$ is a proper class (for
$\mathbb{H}\neq\\{0\\}$), since there exists an injection
$V\rightarrowtail\text{V}^{(\mathbb{H})}$. Hence it can be shown that, for all
$x\in\text{V}^{(\mathbb{H})}$,
$\left\\{y\in\text{V}^{(\mathbb{H})}\mid\left\llbracket
x=y\right\rrbracket=1\right\\}$ is a proper class. Indeed, for all
$\Sigma\subseteq\text{V}^{(\mathbb{H})}$ such that
$\Sigma\cap\text{dom}\left({x}\right)=\emptyset$, we may define
$y_{\Sigma}:\text{dom}\left({x}\right)\cup\Sigma\to\mathbb{H}$ as:

$y_{\Sigma}(u)=\begin{cases}x(u)&\text{, if }u\in\text{dom}\left({x}\right)\\\
0&\text{, if }u\in\Sigma\end{cases}$

so that $\left\llbracket x=y_{\Sigma}\right\rrbracket=1$.

Finally, we show that $\tilde{f}_{\alpha}$ does actually have the desired
domain; the argument is similar to the one used above to prove the injective
case.

######  Proposition 3.7.

For all $\alpha\in\operatorname{On}$,
$\text{dom}\left({\tilde{f}_{\alpha}}\right)=\text{V}^{(\mathbb{H})}_{\alpha}$
(and its image is closed by $\equiv$).

###### Proof.

By induction: suppose that, for all $\beta\in\operatorname{On}$, with
$\beta<\alpha$,
$\text{dom}\left({\tilde{f}_{\beta}}\right)=\text{V}^{(\mathbb{H})}_{\beta}$.
Let $x\in\text{V}^{(\mathbb{H})}_{\alpha}$, and notice that, for all
$u\in\text{dom}\left({x}\right)\subseteq\text{V}^{(\mathbb{H})}_{\varrho(x)}$,
the image of $\tilde{f}_{\varrho(x)}(\\{u\\})$ is a proper class, since it is
non-empty and closed by $\equiv$ (by definition). Therefore, using the axiom
of replacement, we may define an injection
$\varepsilon:\text{dom}\left({x}\right)\rightarrowtail\text{V}^{(\mathbb{H}^{\prime})}$
satisfying $\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}_{\varrho(x)}$, which we may restrict
to a bijection
$\tau:\text{dom}\left({x}\right)\to\varepsilon(\text{dom}\left({x}\right))$.
Hence, just take $x^{\prime}\in\text{V}^{(\mathbb{H}^{\prime})}$ as
$x^{\prime}:\varepsilon(\text{dom}\left({x}\right))\to\mathbb{H}^{\prime}$
given by $x^{\prime}\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=f\circ
x\circ\tau^{-1}$, so that $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$, and thus
$\text{dom}\left({\tilde{f}_{\alpha}}\right)=\text{V}^{(\mathbb{H})}_{\alpha}$.
∎

Note, therefore, that with this new definition for all
$x\in\text{V}^{(\mathbb{H})}_{\alpha}$ there exists
$x^{\prime}\in\text{V}^{(\mathbb{H}^{\prime})}$ such that $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}_{\alpha}$ is witnessed by a bijection
$\tau:\text{dom}\left({x}\right)\to\text{dom}\left({x^{\prime}}\right)$ (not
only a surjection). In fact, we could have assumed the existence of a
bijective witness in the definition of $\tilde{f}_{\alpha}$, and again that
would be equivalent to the other possible definitions in the quotient by
“$\left\llbracket\cdot=\cdot\right\rrbracket=1$” equivalence relation.

###  3.2 Semantical preservation results

######  Theorem 3.8.

For all $\left\langle x,x^{\prime}\right\rangle,\left\langle
y,y^{\prime}\right\rangle,\left\langle z,z^{\prime}\right\rangle\in\tilde{f}$,

$f\left(\left\llbracket y\in
x\right\rrbracket\right)\leq^{\prime}\left\llbracket y^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\qquad\text{ and }\qquad
f\left(\left\llbracket x=z\right\rrbracket\right)\leq^{\prime}\left\llbracket
x^{\prime}=z^{\prime}\right\rrbracket^{\prime}$

###### Proof.

The proof is by induction on the well-founded relation

$\left\langle u,x\right\rangle\prec\left\langle v,y\right\rangle\iff(u=v\text{
and }x\in\text{dom}\left({y}\right))\text{ or
}(u\in\text{dom}\left({v}\right)\text{ and }x=y)$

Let
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
satisfy the conditions of 3.1. Then:

$\displaystyle f\left(\left\llbracket y\in x\right\rrbracket\right)$
$\displaystyle=f\left(\bigvee\limits_{u\in\text{dom}\left({x}\right)}x(u)\wedge\left\llbracket
u=y\right\rrbracket\right)$ (by definition)
$\displaystyle=\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\wedge^{\prime}f\left(\left\llbracket
u=y\right\rrbracket\right)$ $\displaystyle\left(\text{since $f$ preserves
$\wedge,\bigvee$}\right)$
$\displaystyle\leq\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\wedge^{\prime}\left\llbracket\varepsilon(u)=y^{\prime}\right\rrbracket$
$\displaystyle\left(\text{induction hypothesis $\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}$)}\right)$
$\displaystyle=\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}x^{\prime}(\varepsilon(u))\wedge^{\prime}\left\llbracket\varepsilon(u)=y^{\prime}\right\rrbracket$
$\displaystyle\left(\text{using that $\left\langle
x,x^{\prime}\right\rangle,\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}$}\right)$
$\displaystyle=\bigvee\limits_{u^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}x^{\prime}(u^{\prime})\wedge^{\prime}\left\llbracket
u^{\prime}=y^{\prime}\right\rrbracket$ (since $\varepsilon$ is surjective)
$\displaystyle=\left\llbracket y^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}$ (by definition)

Now, since $\mathbb{H}$ is a Heyting algebra, note that the fact that $f$
preserves meets implies that $f$ is increasing, and also implies that $f(a\to
b)\leq f(a)\to f(b)$, for all $a,b\in\mathbb{H}$. With that, let
$\tau:\text{dom}\left({z}\right)\twoheadrightarrow\text{dom}\left({z^{\prime}}\right)$
satisfy the conditions of 3.1. Then:

$\displaystyle f$ $\displaystyle\left(\left\llbracket
x=z\right\rrbracket\right)=$
$\displaystyle=f\left(\bigwedge\limits_{\begin{subarray}{c}u\in\text{dom}\left({x}\right)\\\
v\in\text{dom}\left({z}\right)\end{subarray}}\left(x(u)\to\left\llbracket u\in
z\right\rrbracket\right)\wedge\left(z(v)\to\left\llbracket v\in
x\right\rrbracket\right)\right)$ (by definition)
$\displaystyle\leq\bigwedge\limits_{\begin{subarray}{c}u\in\text{dom}\left({x}\right)\\\
v\in\text{dom}\left({z}\right)\end{subarray}}^{\hskip
18.0pt\prime}f\left(x(u)\to\left\llbracket u\in
z\right\rrbracket\right)\wedge^{\prime}f\left(z(v)\to\left\llbracket v\in
x\right\rrbracket\right)$ ($f$ is increasing)
$\displaystyle\leq\bigwedge\limits_{\begin{subarray}{c}u\in\text{dom}\left({x}\right)\\\
v\in\text{dom}\left({z}\right)\end{subarray}}^{\hskip
18.0pt\prime}\left(f(x(u))\to^{\prime}f\left(\left\llbracket u\in
z\right\rrbracket\right)\right)\wedge^{\prime}\left(f(z(v))\to^{\prime}f\left(\left\llbracket
v\in x\right\rrbracket\right)\right)$ (comments above)
$\displaystyle\leq\bigwedge\limits_{\begin{subarray}{c}u\in\text{dom}\left({x}\right)\\\
v\in\text{dom}\left({z}\right)\end{subarray}}^{\hskip
18.0pt\prime}\left(f(x(u))\to^{\prime}\left\llbracket\varepsilon(u)\in
z^{\prime}\right\rrbracket^{\prime}\right)\wedge^{\prime}\left(f(z(v))\to^{\prime}\left\llbracket\tau(v)\in
x^{\prime}\right\rrbracket^{\prime}\right)$ (comments below)
$\displaystyle=\bigwedge\limits_{\begin{subarray}{c}u\in\text{dom}\left({x}\right)\\\
v\in\text{dom}\left({z}\right)\end{subarray}}^{\hskip
18.0pt\prime}\left(x^{\prime}(\varepsilon(u))\to^{\prime}\left\llbracket\varepsilon(u)\in
z^{\prime}\right\rrbracket^{\prime}\right)\wedge^{\prime}\left(z^{\prime}(\tau(v))\to^{\prime}\left\llbracket\tau(v)\in
x^{\prime}\right\rrbracket^{\prime}\right)$ (elements of $\tilde{f}$)
$\displaystyle=\bigwedge\limits_{\begin{subarray}{c}u^{\prime}\in\text{dom}\left({x^{\prime}}\right)\\\
v^{\prime}\in\text{dom}\left({z^{\prime}}\right)\end{subarray}}^{\hskip
18.0pt\prime}\left(x^{\prime}(u^{\prime})\to^{\prime}\left\llbracket
u^{\prime}\in
z^{\prime}\right\rrbracket^{\prime}\right)\wedge^{\prime}\left(z^{\prime}(v^{\prime})\to^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}\right)$ ($\varepsilon,\tau$
are surjections) $\displaystyle=\left\llbracket
x^{\prime}=z^{\prime}\right\rrbracket^{\prime}$ (by definition)

In the fourth step, we use that the implication is increasing in the second
coordinate, and that by the induction hypothesis we have:

$f\left(\left\llbracket u\in
z\right\rrbracket\right)\leq\left\llbracket\varepsilon(u)\in
z^{\prime}\right\rrbracket^{\prime}\quad\text{ and }\quad
f\left(\left\llbracket v\in
x\right\rrbracket\right)\leq\left\llbracket\tau(v)\in
x^{\prime}\right\rrbracket^{\prime}$

∎

This result easily extends to positive formulas (with only $\wedge,\vee$) with
bounded quantifiers (of the form $\exists u\in x$ and $\forall u\in x$), using
that corollary 1.18 from [Bel05] gives us that:

$\left\llbracket\exists u\in x\
\varphi(u)\right\rrbracket=\bigvee\limits_{u\in\text{dom}\left({x}\right)}x(u)\wedge\left\llbracket\varphi(u)\right\rrbracket$
$\left\llbracket\forall u\in x\
\varphi(u)\right\rrbracket=\bigwedge\limits_{u\in\text{dom}\left({x}\right)}x(u)\to\left\llbracket\varphi(u)\right\rrbracket$

######  Corollary 3.9.

Let $\varphi$ be a positive formula with bounded quantifiers. Then, for all
$\left\langle a_{1},a_{1}^{\prime}\right\rangle,...,\left\langle
a_{n},a_{n}^{\prime}\right\rangle\in\tilde{f}$, we have:

$f\left(\left\llbracket\varphi(a_{1},...,a_{n})\right\rrbracket\right)\leq^{\prime}\left\llbracket\varphi(a_{1}^{\prime},...,a_{n}^{\prime})\right\rrbracket^{\prime}$

###### Proof.

By induction in the complexity of the formula. The initial case, for atomic
sentences, was shown in the previous theorem, and the cases with $\wedge$ and
$\vee$ are immediate from the fact that $f$ preserves finite meets and joins.
For quantifiers, the proof is similar last theorem’s proof. Let $\left\langle
x,x^{\prime}\right\rangle\in\tilde{f}$ with witness
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$.
Then:

$\displaystyle f\left(\left\llbracket\exists u\in x\
\varphi(u)\right\rrbracket\right)$
$\displaystyle=f\left(\bigvee\limits_{u\in\text{dom}\left({x}\right)}x(u)\wedge\left\llbracket\varphi(u)\right\rrbracket\right)$
(by definition)
$\displaystyle=\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\wedge^{\prime}f\left(\left\llbracket\varphi(u)\right\rrbracket\right)$
$\displaystyle\left(\text{since $f$ preserves $\wedge,\bigvee$}\right)$
$\displaystyle\leq\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\wedge^{\prime}\left\llbracket\varphi(\varepsilon(u))\right\rrbracket$
$\displaystyle\left(\text{by hypothesis and $\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}$)}\right)$
$\displaystyle=\bigvee\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}x^{\prime}(\varepsilon(u))\wedge^{\prime}\left\llbracket\varphi(\varepsilon(u))\right\rrbracket$
$\displaystyle\left(\text{using that $\left\langle
x,x^{\prime}\right\rangle,\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}$}\right)$
$\displaystyle=\bigvee\limits_{u^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}x^{\prime}(u^{\prime})\wedge^{\prime}\left\llbracket\varphi(u^{\prime})\right\rrbracket$
(since $\varepsilon$ is surjective) $\displaystyle=\left\llbracket\exists
u^{\prime}\in x^{\prime}\ \varphi(u^{\prime})\right\rrbracket^{\prime}$ (by
definition)

Similarly, we have

$\displaystyle f\left(\left\llbracket\forall u\in x\
\varphi(u)\right\rrbracket\right)$
$\displaystyle=f\left(\bigwedge\limits_{u\in\text{dom}\left({x}\right)}x(u)\to\left\llbracket\varphi(u)\right\rrbracket\right)$
(by definition)
$\displaystyle\leq\bigwedge\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f\left(x(u)\to\left\llbracket\varphi(u)\right\rrbracket\right)$
(since $f$ is increasing)
$\displaystyle\leq\bigwedge\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\to^{\prime}f\left(\left\llbracket\varphi(u)\right\rrbracket\right)$
$\displaystyle\left(\text{since $f(a\to b)\leq f(a)\to f(b)$}\right)$
$\displaystyle\leq\bigwedge\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}f(x(u))\to^{\prime}\left\llbracket\varphi(\varepsilon(u))\right\rrbracket^{\prime}$
(induction hypothesis)
$\displaystyle=\bigwedge\limits_{u\in\text{dom}\left({x}\right)}^{\hskip
18.0pt\prime}x^{\prime}(\varepsilon(u))\to^{\prime}\left\llbracket\varphi(\varepsilon(u))\right\rrbracket^{\prime}$
(using that $\left\langle x,x^{\prime}\right\rangle\in\tilde{f}$)
$\displaystyle=\bigwedge\limits_{u^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}x^{\prime}(u^{\prime})\to^{\prime}\left\llbracket\varphi(u^{\prime})\right\rrbracket^{\prime}$
(since $\varepsilon$ is surjective) $\displaystyle=\left\llbracket\forall
u^{\prime}\in x^{\prime}\ \varphi(u^{\prime})\right\rrbracket^{\prime}$ (by
definition)

∎

###  3.3 Functorial properties

Another consequence of the previous theorem is that, if $\left\llbracket
x=z\right\rrbracket=1_{H}$, then, since $1_{H}=\bigwedge\emptyset$, we obtain:

$f\left(\left\llbracket
x=z\right\rrbracket\right)=f(1_{H})=1_{H^{\prime}}\leq\left\llbracket
x^{\prime}=z^{\prime}\right\rrbracket^{\prime}$

that is, $\left\llbracket
x^{\prime}=z^{\prime}\right\rrbracket^{\prime}=1_{H^{\prime}}$. Therefore,
when we take the quotient by $\equiv$, the semi-function $\tilde{f}$ defines
an object mapping
$\overline{f}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$.

######  Proposition 3.10.

  1. 1.

$\overline{id_{\mathbb{H}}}=id_{\mathbf{Set}^{\left(\mathbb{H}\right)}}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}\right)}$;

  2. 2.

if $f^{\prime}:\mathbb{H}^{\prime}\to\mathbb{H}^{\prime\prime}$ preserves
finite meets and arbitrary joins, then
$\overline{f^{\prime}}\circ\overline{f}=\overline{f^{\prime}\circ
f}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime\prime}\right)}$.

###### Proof.

  1. 1.

we show that, for all $\alpha\in\operatorname{On}$, if $\left\langle
x,y^{\prime}\right\rangle\in(\widetilde{id_{\mathbb{H}}})_{\alpha}$, then
$\left\llbracket x=y^{\prime}\right\rrbracket=1$. Suppose, by induction, that
this is the case for all $\beta<\alpha$, and let
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
(with $\left\llbracket x^{\prime}=y^{\prime}\right\rrbracket=1$) witness
$\left\langle
x,y^{\prime}\right\rangle\in(\widetilde{id_{\mathbb{H}}})_{\alpha}$. Then,
$x^{\prime}\circ\varepsilon=id_{\mathbb{H}}\circ x=x$, and for all
$u\in\text{dom}\left({x}\right)$, $\left\langle
u,\varepsilon(x)\right\rangle\in(\widetilde{id_{\mathbb{H}}})_{\varrho(x)}$,
thereby $\left\llbracket\varepsilon(u)=u\right\rrbracket=1$ (using the
induction hypothesis). Thus, for all $u\in\text{dom}\left({x}\right)$, since
$\varepsilon$ is surjective we have:

$x(u)=x^{\prime}(\varepsilon(u))=x^{\prime}(\varepsilon(u))\wedge\left\llbracket\varepsilon(u)=u\right\rrbracket\leq\bigvee\limits_{w^{\prime}\in\text{dom}\left({x^{\prime}}\right)}x^{\prime}(w^{\prime})\wedge\left\llbracket
w^{\prime}=u\right\rrbracket=\left\llbracket u\in x^{\prime}\right\rrbracket$

Similarly, for all $v^{\prime}\in\text{dom}\left({x^{\prime}}\right)$, there
exists $v\in\text{dom}\left({x}\right)$ such that $\varepsilon(v)=v^{\prime}$,
and

$x^{\prime}(v^{\prime})=x^{\prime}(\varepsilon(v))=x(v)=x(v)\wedge\left\llbracket\varepsilon(v)=v\right\rrbracket\leq\bigvee\limits_{w\in\text{dom}\left({x}\right)}x(w)\wedge\left\llbracket
w=v^{\prime}\right\rrbracket=\left\llbracket v^{\prime}\in x\right\rrbracket$

Now, observe that $x(u)\leq\left\llbracket u\in x^{\prime}\right\rrbracket$
if, and only if, $1\leq x(u)\to\left\llbracket u\in
x^{\prime}\right\rrbracket$, for all $u\in\text{dom}\left({x}\right)$; that
is, $\bigwedge\limits_{u\in\text{dom}\left({x}\right)}x(u)\to\left\llbracket
u\in x^{\prime}\right\rrbracket=1$. Analogously,
$x^{\prime}(v^{\prime})\leq\left\llbracket v^{\prime}\in
x^{\prime}\right\rrbracket$ for all
$v^{\prime}\in\text{dom}\left({x^{\prime}}\right)$ is equivalent to
$\bigwedge\limits_{v^{\prime}\in\text{dom}\left({x^{\prime}}\right)}x^{\prime}(v^{\prime})\to\left\llbracket
v^{\prime}\in x\right\rrbracket=1$. Therefore:

$\left\llbracket
x=x^{\prime}\right\rrbracket=\bigwedge\limits_{u\in\text{dom}\left({x}\right)}\left(x(u)\to\left\llbracket
u\in
x^{\prime}\right\rrbracket\right)\wedge\bigwedge\limits_{v^{\prime}\in\text{dom}\left({x^{\prime}}\right)}\left(x^{\prime}(v^{\prime})\to\left\llbracket
v^{\prime}\in x\right\rrbracket\right)=1$

Finally, since $\left\llbracket x=x^{\prime}\right\rrbracket=1=\left\llbracket
x^{\prime}=y^{\prime}\right\rrbracket$, we may conclude that $\left\llbracket
x=y^{\prime}\right\rrbracket=1$, as desired.

Now, by the definition of $\equiv$, $\left\llbracket
x=y^{\prime}\right\rrbracket=1$ if, and only if, $[x]=[y^{\prime}]$. As a
result, taking the quotient,
$\left\langle[x],[y^{\prime}]\right\rangle\in\overline{id_{\mathbb{H}}}$ if,
and only if, $[x]=[y^{\prime}]$, hence $\overline{id_{\mathbb{H}}}$ is the
identity in $\mathbf{Set}^{\left(\mathbb{H}\right)}$.

  2. 2.

Let
$\left\langle[x],[z^{\prime\prime}]\right\rangle\in\overline{f^{\prime}}\circ\overline{f}$,
_i. e._ , there exists $[y^{\prime}]\in\mathbf{Set}^{\left(\mathbb{H}\right)}$
such that $\left\langle[x],[y^{\prime}]\right\rangle\in\overline{f}$ and
$\left\langle[y^{\prime}],[z^{\prime\prime}]\right\rangle\in\overline{f^{\prime}}$.
Consider
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$,
with $x^{\prime}\in[y^{\prime}]$, a witness of
$\left\langle[x],[y^{\prime}]\right\rangle\in\overline{f}$, and
$\varepsilon^{\prime}:\text{dom}\left({x^{\prime}}\right)\twoheadrightarrow\text{dom}\left({y^{\prime\prime}}\right)$,
with $y^{\prime\prime}\in[z^{\prime\prime}]$, a witness of
$\left\langle[y^{\prime}],[z^{\prime\prime}]\right\rangle=\left\langle[x^{\prime}],[z^{\prime\prime}]\right\rangle\in\overline{f^{\prime}}$.
Then,
$\varepsilon^{\prime}\circ\varepsilon:\text{dom}\left({x}\right)\to\text{dom}\left({y^{\prime\prime}}\right)$
witnesses
$\left\langle[x],[z^{\prime\prime}]\right\rangle\in\overline{f^{\prime}\circ
f}$. That is, we have shown that
$\overline{f^{\prime}}\circ\overline{f}\subseteq\overline{f^{\prime}\circ f}$,
and since both are functions, we obtain
$\overline{f^{\prime}}\circ\overline{f}=\overline{f^{\prime}\circ f}$.

∎

At last, using that $f\left(\left\llbracket y\in
x\right\rrbracket\right)\leq^{\prime}\left\llbracket y^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}$, it can be shown that, if
$\left\llbracket\text{fun}\left({h:x\to y}\right)\right\rrbracket=1$, then
$\left\llbracket\text{fun}\left({\tilde{f}(h):\tilde{f}(x)\to\tilde{f}(y)}\right)\right\rrbracket=1^{\prime}$,
and:

$\tilde{f}(id_{x})=id_{\tilde{f}(x)}:\tilde{f}(x)\to\tilde{f}(x)\quad\text{
and
}\quad\left\llbracket\text{fun}\left({\tilde{f}(id_{x}):\tilde{f}(x)\to\tilde{f}(x)}\right)\right\rrbracket^{\prime}=1^{\prime}$

Besides, if $\left\llbracket\text{fun}\left({g:y\to
z}\right)\right\rrbracket=1$, then:

$\tilde{f}(g\circ
h)=\tilde{f}(g)\circ\tilde{f}(h):\tilde{f}(x)\to\tilde{f}(z)\quad\text{ and
}\quad\left\llbracket\text{fun}\left({\tilde{f}(g\circ
h):\tilde{f}(x)\to\tilde{f}(z)}\right)\right\rrbracket^{\prime}=1^{\prime}$

That is, by taking the quotient,
$\overline{f}:\mathbf{Set}^{\left(\mathbb{H}\right)}\to\mathbf{Set}^{\left(\mathbb{H}^{\prime}\right)}$
actually defines a functor.

As we saw in the first section, a $\left(\wedge,\bigvee\right)$-preserving
function between Heyting algebras induces a functor between the corresponding
sheaf topos which preserves finite limits and arbitrary colimits (the left
adjoint of a geometric morphism). More precisely, using the natural
equivalences
$\mathbb{H}\text{-}\mathbf{Set}\simeq\mathbf{Sh}\left(\mathbb{H}\right)$ and
$\mathbb{H}^{\prime}\text{-}\mathbf{Set}\simeq\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$,
such a function $f:\mathbb{H}\to\mathbb{H}^{\prime}$ gives rise to a function
$\varphi_{f}:\mathbb{H}\text{-}\mathbf{Set}\to\mathbb{H}^{\prime}\text{-}\mathbf{Set}$
given by: where $f\circ\phi:X\times Y\to\mathbb{H}^{\prime}$. Thus, we
investigate how $\tilde{f}$ may induce a morphism of
$\mathbb{H}^{\prime}$-sets.

######  Proposition 3.11.

Let $\left\langle x,x^{\prime}\right\rangle\in\tilde{f}$ with
$\varepsilon:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
as witness. Consider the function
$\varepsilon^{H^{\prime}}:\text{dom}\left({x}\right)\times\text{dom}\left({x^{\prime}}\right)\to\mathbb{H}^{\prime}$
given by:

$\varepsilon^{H^{\prime}}(u,v^{\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=f\left(\left\llbracket
u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime},\text{ for all }\left\langle
u,v^{\prime}\right\rangle\in\text{dom}\left({x}\right)\times\text{dom}\left({x^{\prime}}\right)$

Then, $\varepsilon^{H^{\prime}}$ defines a morphism of $\mathbb{H}$-sets
$\varepsilon^{H^{\prime}}:(\text{dom}\left({x}\right),f\circ\delta_{x})\to(\text{dom}\left({x^{\prime}}\right),\delta_{x^{\prime}})$
which does not depend on the choice of witness, where

$\delta_{x}(u,v)\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\llbracket
u\in x\right\rrbracket\wedge\left\llbracket u=v\right\rrbracket,\text{ for all
}u,v\in\text{dom}\left({x}\right)$
$\delta_{x^{\prime}}(u^{\prime},v^{\prime})\mathrel{\hbox
to0.0pt{\raisebox{1.29167pt}{$\cdot$}\hss}\raisebox{-1.29167pt}{$\cdot$}}=\left\llbracket
u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}=v^{\prime}\right\rrbracket^{\prime},\text{ for all
}u^{\prime},v^{\prime}\in\text{dom}\left({x^{\prime}}\right)$

Note that $\delta_{x}$ and $\delta_{x^{\prime}}$ are exactly the ones used in
the equivalence
$\mathbb{H}\text{-}\mathbf{Set}\simeq\mathbf{Set}^{\left(\mathbb{H}\right)}$
because, since $\left\llbracket u\in x\right\rrbracket\wedge\left\llbracket
u=v\right\rrbracket\leq\left\llbracket v\in x\right\rrbracket$, we have:

$\left\llbracket u\in x\right\rrbracket\wedge\left\llbracket
u=v\right\rrbracket\wedge\left\llbracket v\in
x\right\rrbracket=\left\llbracket u\in x\right\rrbracket\wedge\left\llbracket
u=v\right\rrbracket$

###### Proof.

We verify the four conditions that define a morphism of $\mathbb{H}$-sets. Let
$u,v\in\text{dom}\left({x}\right)$ and
$u^{\prime},v^{\prime}\in\text{dom}\left({x^{\prime}}\right)$.

  1. 1.

$\delta_{x^{\prime}}(u^{\prime},v^{\prime})\wedge^{\prime}\varepsilon^{H^{\prime}}(u,v^{\prime})\leq\varepsilon^{H^{\prime}}(u,u^{\prime})$.
Indeed,

$\displaystyle\delta_{x^{\prime}}$
$\displaystyle(u^{\prime},v^{\prime})\wedge^{\prime}\varepsilon^{H^{\prime}}(u,v^{\prime})=$
$\displaystyle=\left\llbracket u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}f\left(\left\llbracket
u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=\varepsilon^{H^{\prime}}(u,u^{\prime})$

  2. 2.

$(f\circ\delta_{x})(u,v)\wedge^{\prime}\varepsilon^{H^{\prime}}(u,v^{\prime})\leq\varepsilon^{H^{\prime}}(v,v^{\prime})$.
Indeed,

$\displaystyle(f$
$\displaystyle\circ\delta_{x})(u,v)\wedge^{\prime}\varepsilon^{H^{\prime}}(u,v^{\prime})=$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\wedge\left\llbracket
u=v\right\rrbracket\right)\wedge^{\prime}f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket v\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=\varepsilon(v)\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket v\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(v)\in
v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=\varepsilon^{H^{\prime}}(v,v^{\prime})$

  3. 3.

$\varepsilon^{H^{\prime}}(u,u^{\prime})\wedge\varepsilon^{H^{\prime}}(u,v^{\prime})\leq\delta_{x^{\prime}}(u^{\prime},v^{\prime})$.
Indeed,

$\displaystyle\varepsilon^{H^{\prime}}$
$\displaystyle(u,u^{\prime})\wedge\varepsilon^{H^{\prime}}(u,v^{\prime})=$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}$ $\displaystyle\hskip
182.09746pt\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket
u^{\prime}=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle\leq\left\llbracket v^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}=v^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=\delta_{x^{\prime}}(u^{\prime},v^{\prime})$

  4. 4.

$\bigvee\limits_{w^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}\varepsilon^{H^{\prime}}(u,w^{\prime})=(f\circ\delta_{x})(u,u)$.
Indeed,

     * •

for all $w^{\prime}\in\text{dom}\left({x^{\prime}}\right)$, using that $f$
preserves $1$, we have:

$\displaystyle\varepsilon^{H^{\prime}}(u,w^{\prime})$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=w^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
w^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}1_{H^{\prime}}=f\left(\left\llbracket
u\in x\right\rrbracket\right)\wedge^{\prime}f(1_{H})$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}f\left(\left\llbracket u\in
u\right\rrbracket\right)=f\left(\left\llbracket u\in
x\right\rrbracket\wedge\left\llbracket u=u\right\rrbracket\right)$
$\displaystyle=(f\circ\delta_{x})(u,u)$

thus,
$\bigvee\limits_{w^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}\varepsilon^{H^{\prime}}(u,w^{\prime})\leq(f\circ\delta_{x})(u,u)$;

     * •

on the other hand, since
$\varepsilon(u)\in\text{dom}\left({x^{\prime}}\right)$,

$\displaystyle\bigvee\limits_{w^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}\varepsilon^{H^{\prime}}(u,w^{\prime})$
$\displaystyle\geq\varepsilon^{H^{\prime}}\left\langle
u,\varepsilon(u)\right\rangle=$ $\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=\varepsilon(u)\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(u)\in
x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle=f\left(\left\llbracket
u\in
x\right\rrbracket\right)\wedge^{\prime}1_{H^{\prime}}\wedge^{\prime}\left\llbracket\varepsilon(u)\in
x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle=f\left(\left\llbracket
u\in x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)\in
x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\geq f\left(\left\llbracket
u\in x\right\rrbracket\right)\wedge^{\prime}f\left(\left\llbracket u\in
x\right\rrbracket\right)=f\left(\left\llbracket u\in x\right\rrbracket\right)$
$\displaystyle=f\left(\left\llbracket u\in x\right\rrbracket\wedge
1_{H}\right)=f\left(\left\llbracket u\in
x\right\rrbracket\wedge\left\llbracket u=u\right\rrbracket\right)$
$\displaystyle=(f\circ\delta_{x})(u,u)$

Therefore,
$\bigvee\limits_{w^{\prime}\in\text{dom}\left({x^{\prime}}\right)}^{\hskip
18.0pt\prime}\varepsilon^{H^{\prime}}(u,w^{\prime})\geq(f\circ\delta_{x})(u,u)$.

Finally, note that this result does not depends on the choice of witness: let
$\left\langle
u,v^{\prime}\right\rangle\in\text{dom}\left({x}\right)\times\text{dom}\left({x^{\prime}}\right)$
and
$\tau:\text{dom}\left({x}\right)\twoheadrightarrow\text{dom}\left({x^{\prime}}\right)$
be a witness of $\left\langle x,x^{\prime}\right\rangle\in\tilde{f}$. Then,
since $u\in\text{dom}\left({x}\right)$, we have $\left\langle
u,\varepsilon(u)\right\rangle\in\tilde{f}$ e $\left\langle
u,\tau(u)\right\rangle\in\tilde{f}$; and since $1=\left\llbracket
u=u\right\rrbracket$, the previous theorem gives us:

$1^{\prime}=f(1)=f\left(\left\llbracket
u=u\right\rrbracket\right)\leq\left\llbracket\tau(u)=\varepsilon(u)\right\rrbracket^{\prime}$

Thus,

$\displaystyle\varepsilon^{H^{\prime}}(u,v^{\prime})$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}=$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}1_{H^{\prime}}\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\tau(u)=\varepsilon(u)\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\tau(u)=v^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
v^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=\tau^{H^{\prime}}(u,v^{\prime})$

thereby
$\varepsilon^{H^{\prime}}(u,v^{\prime})\leq\tau^{H^{\prime}}(u,v^{\prime})$.
The proof that
$\tau^{H^{\prime}}(u,v^{\prime})\leq\varepsilon^{H^{\prime}}(u,v^{\prime})$ is
analogous. ∎

######  Remark.

The idea now would be to show that such morphisms $\varepsilon^{H^{\prime}}$
are isomorphisms, which could be used to build a natural isomorphism between
$\overline{f}$ and $\varphi_{f}$. To show that, a possibility would be to use
the characterization of monomorphisms and epimorphisms in
$\mathbb{H}\text{-}\mathbf{Set}$ (see [Bor08c], propositions 2.8.8 e 2.8.7),
that is, to show that for all $u,v\in\text{dom}\left({x}\right)$ and
$u^{\prime}\in\text{dom}\left({x^{\prime}}\right)$:

  * •

$\varepsilon^{H^{\prime}}(u,u^{\prime})\wedge\varepsilon^{H^{\prime}}(v,u^{\prime})\leq(f\circ\delta_{x})(u,v)$
(which is equivalent to $\varepsilon^{H^{\prime}}$ being monic);

  * •

$\bigvee\limits_{w\in\text{dom}\left({x}\right)}\varepsilon^{H^{\prime}}(w,u^{\prime})=\delta_{x^{\prime}}(u^{\prime},u^{\prime})$
(which is equivalent to $\varepsilon^{H^{\prime}}$ being epic);

and, since $\mathbb{H}\text{-}\mathbf{Set}$ is a topos,
$\varepsilon^{H^{\prime}}$ would be an isomorphism.

Now, expanding the definitions,

$\displaystyle\varepsilon^{H^{\prime}}$
$\displaystyle(u,u^{\prime})\wedge\varepsilon^{H^{\prime}}(v,u^{\prime})=$
$\displaystyle=f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}f\left(\left\llbracket v\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(v)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\leq
f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(v)=u^{\prime}\right\rrbracket^{\prime}$
$\displaystyle\leq f\left(\left\llbracket u\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(u)=\varepsilon(v)\right\rrbracket^{\prime}$
$\displaystyle\qquad\text{ and we want to show that }\leq
f\left(\left\llbracket u\in x\right\rrbracket\wedge\left\llbracket
u=v\right\rrbracket\right)=(f\circ\delta_{x})(u.v)$
$\displaystyle\bigvee\limits_{w\in\text{dom}\left({x}\right)}\varepsilon^{H^{\prime}}(w,u^{\prime})$
$\displaystyle=\bigvee\limits_{w\in\text{dom}\left({x}\right)}f\left(\left\llbracket
w\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(w)=u^{\prime}\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket
u^{\prime}\in x^{\prime}\right\rrbracket^{\prime}$
$\displaystyle=\bigvee\limits_{w\in\text{dom}\left({x}\right)}f\left(\left\llbracket
w\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(w)=\varepsilon(t)\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(t)\in
x^{\prime}\right\rrbracket^{\prime}\text{($\varepsilon$ is surjective)}$
$\displaystyle\geq f\left(\left\llbracket t\in
x\right\rrbracket\right)\wedge^{\prime}\left\llbracket\varepsilon(t)=\varepsilon(t)\right\rrbracket^{\prime}\wedge^{\prime}\left\llbracket\varepsilon(t)\in
x^{\prime}\right\rrbracket^{\prime}$ $\displaystyle\text{ and we want to show
that }=\left\llbracket u^{\prime}\in
x^{\prime}\right\rrbracket^{\prime}=\delta_{x^{\prime}}(u^{\prime},u^{\prime})$

(the other inequality for the epimorphism condition is trivial, because of the
meet’s properties).

These inequalities can be achieved whenever $f$ preserves meets and preserves
strictly the values of atomic formulas that is: if $\left\langle
x,x^{\prime}\right\rangle,\left\langle y,y^{\prime}\right\rangle,\left\langle
z,z^{\prime}\right\rangle\in\tilde{f}$, then

$f\left(\left\llbracket x\in y\right\rrbracket\right)=\left\llbracket
x^{\prime}\in y^{\prime}\right\rrbracket^{\prime}\qquad\qquad
f\left(\left\llbracket x=z\right\rrbracket\right)=\left\llbracket
x^{\prime}=z^{\prime\prime}\right\rrbracket^{\prime}$

Therefore, observing the proof of the aforementioned theorem, note that we may
obtain these inequalities (and, thus, that $\varepsilon^{\mathbb{H}^{\prime}}$
is iso) at least in the case that $f:\mathbb{H}\to\mathbb{H}^{\prime}$
preserves (strictly) the implication and both arbitrary meets and joins. With
that hypothesis, we could also adapt the corollary to the theorem to obtain
the strict preservation of $\mathbb{H}$-values of all formulas with bounded
quantifiers.

##  4 Final Remarks and Future Works

######  Remark.

The categorial and semantical correspondences between local set theories (=
toposes, see [Bel88]) and cumulative (constructions in) set theories has been
studied since the late 1970’s : [Fou80], [Hay81], [BS92], [Shu10], [Yam18]. It
will be interesting to determine in what level this semantical correspondence
is compatible with the change of basis given by a locale morphism
$f:\mathbb{H}\to\mathbb{H}^{\prime}$.
Possible extensions of this correspondence to other kinds of categories
associated to other complete lattices (eventually endowed with and additional
structure [LT15]) could gives us a clue of what are the “right semantical
notions” of the less structured side of the correspondence (i.e., the
cumulative construction), since the notion of $\mathbb{H}$-set can be extended
to more general algebras ([Men19]).

######  Remark.

In a different direction, another aspect that should be analysed is if the
“lifting property” through
$\text{V}^{(\mathbb{H})}\twoheadrightarrow\mathbf{Sh}\left(\mathbb{H}\right)$
also holds for other natural topoi morphisms as the logical functors. Since
logical functors and (the left part of) geometric morphism coincide only
trivially (i.e. iff when both are equilavences of categories), this will be in
fact a new direction to pursue.

Note that the “conceptual orthogonality” between the two kind of functors
$\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$
occurs already in the algebraic level of arrows
$\mathbb{H}\to\mathbb{H}^{\prime}$. More precisely, given a non trivial
complete Boolean algebra $(\mathbb{B},\leq)$ and the unique injective morphism
$i:\mathbf{2}\hookrightarrow\mathbb{B}$ (where $\mathbf{2}=\\{0,1\\}$), we get
three kind of morphisms $\mathbb{B}\to\mathbf{2}$:

  * •

$l:\mathbb{B}\to\mathbf{2}$ is the left adjoint of $i$ (given by
$l(x)=0\Leftrightarrow x=0$): it preserves only the suprema;

  * •

$r:\mathbb{B}\to\mathbf{2}$ is the right adjoint of $i$ (given by
$r(x)=1\Leftrightarrow x=1$ it preserves only the infima;

  * •

$U:\mathbb{B}\to\mathbf{2}$ is the quotient by an ultrafilter $U$, that
preserves $0$, $1$, negation, implication, finite sups and finite infs.

On the other hand, note that a logical functor
$\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$
induces a Heyting algebra morphism $\mathbb{H}\to\mathbb{H}^{\prime}$ (since
$\mathbb{H}\cong Subobj(\mathbf{1})$). Therefore, seems to be natural try to
establish a correspondence between other kind of morphisms
$\mathbb{H}\to\mathbb{H}^{\prime}$ and the logical functors
$\mathbf{Sh}\left(\mathbb{H}\right)\to\mathbf{Sh}\left(\mathbb{H}^{\prime}\right)$
and ask how they are related to some alternative notion of induced arrow
$\text{V}^{(\mathbb{H})}\to\text{V}^{(\mathbb{H}^{\prime})}$.

In particular, it will be natural consider the connections between the various
“forcing relations” (according the previous remark), classical and
intuitionistic, related to the canonical morphisms between complete Boolean
algebras associated to a complete Heyting algebra
$Reg(\mathbb{H})\hookrightarrow\mathbb{H}$ and
$\mathbb{H}\twoheadrightarrow\displaystyle\frac{\mathbb{H}}{\langle
x\leftrightarrow\neg\neg x\rangle}$.

## References

  * [Bel05] John L. Bell. Set theory: Boolean-valued models and independence proofs. 3rd ed. Oxfor Logic Guides, vol. 47. Oxford, United Kingdom: Clarendon Press, 2005.
  * [Bel88] John L. Bell. Toposes and local set theories: an introduction. Oxford Logic Guides, vol. 14. Oxford, United Kingdom: Clarendon Press, 1988.
  * [Bor08a] Francis Borceux. Handbook of Categorical Algebra. Vol. 1. Encyclopedia of mathematics and its applications, vol. 50. Cambridge, United Kingdom: Cambridge University Press, 2008.
  * [Bor08c] Francis Borceux. Handbook of Categorical Algebra. Vol. 3. Encyclopedia of mathematics and its applications, vol. 52. Cambridge, United Kingdom: Cambridge University Press, 2008.
  * [BS92] Andreas R. Blass and Andre Scedrov. “Complete topoi representing models of set theory”. In: Annals of Pure and Applied Logic 57 (1992), pp. 1–26. doi: https://doi.org/10.1016/0168-0072(92)90059-9.
  * [Fou80] Michael P. Fourman. “Sheaf models for set theory”. In: Annals of Pure and Applied Logic 19 (1980), pp. 91–101. doi: https://doi.org/10.1016/0022-4049(80)90096-1.
  * [Gui13] Fiorella Guichardaz. “Limits of Boolean algebras and Boolean valued models”. MA thesis. Universitá degli studi di Torino, 2013.
  * [Hay81] Susumu Hayashi. “On set theories in toposes”. In: Logic Symposia Hakone 1979, 1980. Ed. by Gert H. Müller, Gaisi Takeuti, and Tosiyuki Tugué. Lecture Notes in Mathematics, vol. 891. Heidelberg, Germany: Springer-Verlag, 1981. Chap. 2, pp. 23–29.
  * [Jec03] Thomas J. Jech. Set Theory.: The third millennium edition, revised and expanded. Springer Monographs in Mathematics. Heidelberg, Germany: Springer-Verlag, 2003.
  * [Kun11] Kenneth Kunen. Set Theory. Studies in Logic, vol. 34. London, United Kingdom: College Publications, 2011.
  * [Lan98] Saunders Mac Lane. Categories for the Working Mathematician. 2nd ed. Graduate texts in mathematics, vol. 5. New York, United States: Springer-Verlag, 1998.
  * [LT15] Benedikt Löwe and Sourav Tarafder. “Generalized algebra-valued models of set theory”. In: The Review of Symbolic Logic 8 (2015), pp. 192–205. doi: https://doi.org/10.1017/S175502031400046X.
  * [Men19] Caio A. Mendes. “Sheaf-like categories and applications”. In private communication. 2019.
  * [Shu10] Michael A. Shulman. “Stack semantics and the comparison of material and structural set theories”. In: arXiv e-prints (2010). arXiv: 1004.3802v1.
  * [Yam18] Keita Yamamoto. “Toposes from Forcing for Intuitionistic ZF with Atoms”. In: arXiv e-prints (2018). arXiv: 1702.03399v2.