# nLab Heyting prealgebra

Contents

## In higher category theory

category theory

#### Limits and colimits

limits and colimits

(0,1)-category

(0,1)-topos

# Contents

## Definition

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. See principle of equivalence.

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.

## Examples

• The propositions in a logic naturally form a Heyting prealgebra under entailment.

One can take the quotient under bi-entailment to get a poset and a Heyting algebra, or (as discussed above) one can say that bi-entailment is the only relevant notion of equality so that the preorder is really already a poset. But if one wants to simultaneously talk about the syntactic equality of terms, then there will be unequal terms that entail each other, and so one has only a Heyting prealgebra.

## References

Section 4.1 of:

Last revised on April 17, 2024 at 17:59:38. See the history of this page for a list of all contributions to it.