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.
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.
Boolean toposes are bi-Heyting since their subobject lattices are Boolean algebras which are self-dual Heyting algebras.
Presheaf toposes and their essential subtoposes.
A Grothendieck topos is bi-Heyting when finite unions distribute over arbitrary intersections:
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$
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.
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.
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$
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:
William Lawvere, Introduction , pp.1-16 in Lawvere, Schanuel (eds.), Categories in Continuum Physics, Springer LNM 1174 1986.
William Lawvere, Intrinsic Co-Heyting Boundaries and the Leibniz Rule in Certain Toposes , pp.279-281 in A. Carboni, M. Pedicchio, G. Rosolini (eds.) , Category Theory - Proceedings of the International Conference held in Como 1990, LNM 1488 Springer Heidelberg 1991.
Gonzalo E. Reyes, Houman Zolfaghari, Bi-Heyting Algebras, Toposes and Modalities, J. Phi. Logic 25 (1996) pp.25-43.
Last revised on March 28, 2020 at 02:08:50. See the history of this page for a list of all contributions to it.