In mathematics, especially in order theory, a complete Heyting algebra is a Heyting algebra that is complete as a lattice. Complete Heyting algebras are the objects of three different categories; the category CHey, the category Loc of locales, and its opposite, the category Frm of frames. Although these three categories contain the same objects, they differ in their morphisms, and thus get distinct names. Only the morphisms of CHey are homomorphisms of complete Heyting algebras.

Locales and frames form the foundation of pointless topology, which, instead of building on point-set topology, recasts the ideas of general topology in categorical terms, as statements on frames and locales.

Consider a partially ordered set (P, ≤) that is a complete lattice. Then P is a complete Heyting algebra or frame if any of the following equivalent conditions hold:

The entailed definition of Heyting implication is ${\displaystyle a\to b=\bigvee \{c\mid a\land c\leq b\}.}$

Using a bit more category theory, we can equivalently define a frame to be a cocomplete cartesian closed poset.

The system of all open sets of a given topological space ordered by inclusion is a complete Heyting algebra.

The objects of the category CHey, the category Frm of frames and the category Loc of locales are complete Heyting algebras. These categories differ in what constitutes a morphism:

The relation of locales and their maps to topological spaces and continuous functions may be seen as follows. Let ${\displaystyle f:X\to Y}$ be any map. The power sets P(X) and P(Y) are complete Boolean algebras, and the map ${\displaystyle f^{-1}:P(Y)\to P(X)}$ is a homomorphism of complete Boolean algebras. Suppose the spaces X and Y are topological spaces, endowed with the topology O(X) and O(Y) of open sets on X and Y. Note that O(X) and O(Y) are subframes of P(X) and P(Y). If ${\displaystyle f}$ is a continuous function, then ${\displaystyle f^{-1}:O(Y)\to O(X)}$ preserves finite meets and arbitrary joins of these subframes. This shows that O is a functor from the category Top of topological spaces to Loc, taking any continuous map