An ultrafilter is a Boolean homomorphism from predicates to truth values.

Evaluation of predicates at a single point yields the so-called principal ultrafilters.

Ultrafilters are functorial on the category GStone.

Predicate transformers between Representations of Stone spaces encode ordinary functions. This mapping is the morphism part of the spectrum functor.

Find the point at which the ultrafilter is fixed.

Attempts to transform a predicate to a Predicate representation. This will not work if the predicate inspects both parts of a tuple. For simple pattern matches, it works:

>>> isJust (toPattern ((either id (LT==).fst) :: (Either Bool Ordering,()) -> Bool))
True

A Stone space is isomorphic to the space of its ultrafilters. gpoint is inverse to principalUltrafilter. Stone spaces are totally disconnected, hence the Eq superclass. Further, every Stone space is topologically compact, whence it is decidable whether the extent of a predicate covers the entire space. The function covers is a meet-semilattice homomorphism and its logical negation deletes is a join-semilattice homomorphism.

Observe that there are types with ultrafilters that are not principal. Their existence is guaranteed by the Ultrafilter Lemma, which is a consequence of the Prime Ideal Theorem. Notably, consider total predicates p :: Integer -> Bool. Define the filter

f p = ∃ n. ∀ m ≥ n. p m

This collects all predicates that are eventually true for sufficiently large numbers. Obviously for every number n the predicate p = (n ==) is not part of the filter f, whence any ultrafilter containing f can not be principal at any number. But by the Ultrafilter Lemma, f is indeed contained in some ultrafilter.

True if the predicate holds for all elements of the spectrum.

True if the negation of the predicate covers.