nLab bi-Heyting topos

Contents

Context

Category theory

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

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)sub(X) of subobjects is a bi-Heyting algebra for every object XX\in\mathcal{E} is called a bi-Heyting topos.

Examples

Properties

Proposition

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

S( iIT i)= iI(ST i). 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 TT\vee_ and implies by the adjoint functor theorem the existence of a left adjoint _\T\backslash T which provides the co-Heyting algebra structure. \qed

Proposition

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

cf. Borceux-Bourn-Johnstone p.350.

Proposition

Let f: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 𝒞 opSet^{\mathcal{C}^{op}} is bi-Heyting.

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

Remark

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 28, 2020 at 02:08:50. See the history of this page for a list of all contributions to it.