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.