Heyting prealgebra

A **Heyting prealgebra** is simply a preorder whose posetal reflection is a Heyting algebra; i.e., it is a preorder which is a bicartesian closed category. In most contexts, there is little need to maintain a difference between Heyting algebras whose carriers are preorders vs. those whose carriers are strictly posets; indeed, in most contexts, there is no need to consider such a distinction to even be meaningful, the only relevant notion of equality being that derived from the preorder structure. However, in contexts where there *is* a separately provided relevant notion of equality on the carrier which is potentially finer-grained than that provided by the preorder structure alone (i.e., in situations where a Heyting algebra carries further structure $x = y$ not necessarily provided simply by $x \leq y \wedge y \leq x$), then it may be worthwhile to track such differences.