Matthew Doty - That's really interesting! With a little reading I now see this: if we have a poset \\(A\\) with the whole chain of adjunctions
\, \setminus \, \dashv \, \vee \, \dashv \Delta \dashv \, \wedge \dashv\, \to
with \\((A,\wedge,\top)\\) giving a cartesian category and \\((A,\vee,\bot)\\) giving a cocartesian category, then \\(A\\) becomes both a [Heyting algebra](https://ncatlab.org/nlab/show/Heyting+algebra) and a [co-Heyting algebra](https://ncatlab.org/nlab/show/Heyting+algebra). Together these give a **bi-Heyting algebra**. The nLab writes:
> A **co-Heyting algebra** is a bounded distributive lattice \\(L\\) equipped with a binary **subtraction** operation \\( \backslash : L\times L\to L \\) such that \\(x\backslash y\leq z\\) iff \\(x\leq y\vee z\\).
> (Existence of \\(\backslash\\) amounts to an adjunction \\( \backslash y\,\dashv\, y\vee \\) and the existence of a left adjoint implies that \\(y\vee \\) preserves limits \\(\wedge\\) hence the assumption of distributivity in the definition is redundant and has been put in for emphasis only.)
> A **bi-Heyting algebra** is a bounded distributive lattice \\(L\\) that carries a Heyting algebra structure with implication \\(\to\\) and a co-Heyting algebra structure with subtraction \\(\backslash\\).
_However_, it seems there are bi-Heyting algebras that aren't Boolean algebras! I don't know what rule they lack, but the nLab writes:
> Co-Heyting algebras were initially called **Brouwerian algebras**. Bi-Heyting algebras were introduced and studied in a series of papers by Cecylia Rauszer in the 1970s who called them **semi-Boolean algebras** which suggests to view them as a generalization of Boolean algebras.
and it says a Boolean algebra is a "degenerate example" of a bi-Heyting algebra. So: how do bi-Heyting algebras differ? Time to read the works of Cecylia Rauszer! They seem like a natural concept.