Matthew: here's an interesting paper on bi-Heyting algebras:

* Francesco Ranzato, [A new characterization of complete Heyting and co-Heyting algebras](https://arxiv.org/abs/1504.03919).

I think it goes like this, though I'm confused about a few points:

Take any lattice that is both **complete** (any subset has a meet), **cocomplete** (any subset has a join), and **completely distributive** (roughly: any meet of joins is a join of meets; see the paper for details). Then it's both a Heyting and co-Heyting algebra.

Ranzato continues:

> It turns out that the class of completely distributive complete lattices is strictly contained in the class of complete Heyting and co-Heyting algebras. Clearly, any completely distributive lattice is a complete Heyting and co-Heyting algebra. On the other hand, this containment turns out to be strict, as shown by the following counterexample.

Part of what's confusing is that nobody should ever say "complete Heyting and co-Heyting algebra" without making it clear, at least the first time, whether "complete" modifies both "Heyting" _and_ "co-Heyting", or just one.

Another part of what's confusing is that the counterexample is a Boolean algebra that's not a complete Boolean algebra!

* Francesco Ranzato, [A new characterization of complete Heyting and co-Heyting algebras](https://arxiv.org/abs/1504.03919).

I think it goes like this, though I'm confused about a few points:

Take any lattice that is both **complete** (any subset has a meet), **cocomplete** (any subset has a join), and **completely distributive** (roughly: any meet of joins is a join of meets; see the paper for details). Then it's both a Heyting and co-Heyting algebra.

Ranzato continues:

> It turns out that the class of completely distributive complete lattices is strictly contained in the class of complete Heyting and co-Heyting algebras. Clearly, any completely distributive lattice is a complete Heyting and co-Heyting algebra. On the other hand, this containment turns out to be strict, as shown by the following counterexample.

Part of what's confusing is that nobody should ever say "complete Heyting and co-Heyting algebra" without making it clear, at least the first time, whether "complete" modifies both "Heyting" _and_ "co-Heyting", or just one.

Another part of what's confusing is that the counterexample is a Boolean algebra that's not a complete Boolean algebra!