Contents

category theory

topos theory

Contents

Idea

A bi-Heyting topos is a topos whose lattices of subobjects carry the structure of a co-Heyting algebra in addition to their normal Heyting algebra structure and thereby permit to model bi-intuitionistic logic.

Definition

A topos $\mathcal{E}$ such that the lattice $sub(X)$ of subobjects is a bi-Heyting algebra for every object $X\in\mathcal{E}$ is called a bi-Heyting topos.

Properties

Proposition

A Grothendieck topos is bi-Heyting when finite unions distribute over arbitrary intersections:

$S\cup (\bigcap_{i\in I} T_i)=\bigcap_{i\in I} (S\cup T_i)\quad .$

Proof. Because this distributivity amounts to the preservation of limits by $T\vee$_ and implies by the adjoint functor theorem the existence of a left adjoint _$\backslash T$ which provides the co-Heyting algebra structure. $\qed$

Proposition

Let $\mathcal{E}$ be a Grothendieck topos with generating set $\{G_i | i\in I\}$. Then $\mathcal{E}$ is bi- Heyting precisely iff the lattice of subobjects of $G_i$ is a bi-Heyting algebra for all $G_i$.

cf. Borceux-Bourn-Johnstone p.350.

Proposition

Let $f:\mathcal{E}\to\mathcal{F}$ be a surjective essential geometric morphism between Grothendieck toposes. If $\mathcal{E}$ is bi-Heyting so is $\mathcal{F}$.

cf. Borceux-Bourn-Johnstone p.351.

Proposition

Let $\mathcal{C}$ be a small category. Then $Set^{\mathcal{C}^{op}}$ is bi-Heyting.

Proof. Let $|\mathcal{C}|$ be the discrete category on the objects of $\mathcal{C}$. The inclusion $i:|\mathcal{C}|\hookrightarrow \mathcal{C}$ induces a surjective essential geometric morphism $Set^{|\mathcal{C}|^{op}}\to Set^{\mathcal{C}^{op}}$ and the first of these is Booelan hence bi-Heyting. By prop. follows the claim. $\qed$

References

Bi-Heyting toposes are explicitly defined in

But their logical possibilities were exploited well before this e.g. in the work of Lawvere, Reyes and collaborators:

Last revised on March 27, 2020 at 22:08:50. See the history of this page for a list of all contributions to it.