Kleene Space

A Kleene Space is a H-Set $X$ equipped with a subset $O\subseteq X$ with the following Separation Property:

• For all $x,y:X$, if $x\in O\Leftrightarrow y\in O$, and $x\in O\land y\in O\Rightarrow x=y$, then $x=y$. In other words, equality in $X$ is given by Kleene Equality with respect to $O$.

A Kleene space can also be viewed as a particularly nice Polynomial Functor, where the space of fibres is a H-Proposition (plus the separation axiom). This perspective becomes particularly useful when considering the Continuous Maps of Kleene Spaces.

Examples

The canonical example of a Kleene space is the Partial Map Classifier, where $O$ is the set of defined elements.

The type Maybe is also a Kleene space, with is-just playing the role of the definedness predicate.

Properties

Every Kleene space has a single "undefined" element; this is an immediate consequence of the separation axiom.