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 such that the lattice of subobjects is a bi-Heyting algebra for every object 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 _ and implies by the adjoint functor theorem the existence of a left adjoint _ which provides the co-Heyting algebra structure.
Let be a Grothendieck topos with generating set . Then is bi- Heyting precisely iff the lattice of subobjects of is a bi-Heyting algebra for all .
cf. Borceux-Bourn-Johnstone p.350.
Let be a surjective essential geometric morphism between Grothendieck toposes. If is bi-Heyting so is .
cf. Borceux-Bourn-Johnstone p.351.
Let be a small category. Then is bi-Heyting.
Proof. Let be the discrete category on the objects of . The inclusion induces a surjective essential geometric morphism and the first of these is Booelan hence bi-Heyting. By prop. follows the claim.
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.