Is there such a thing as 'overtification' (dual to compactification)? The dual to the notion of compactness for spaces is overtness. This duality is not manifest in the category of spaces but rather in the quantifiers used to define these notions. 
Is there a process of 'overtification' corresponding to the process of compactification? Since all topological spaces are overt, this would have to be defined over locales instead.
Edit: I've very new to this topic, so I am not well versed. Most of my understanding comes from this Math Overflow answer by Andrej Bauer. I'll mostly reproduce that here, probably more for my benefit than anyone else's.
To define overtness, first we must suitable define compactness in a way that can be nicely dualized. 
If $X$ is a space, let $\mathcal{O}(X)$ be its topology (as a poset) equipped with the Scott topology. Let $\Sigma = \{0,1\}$ be the Sierpinski space, with topology $\{\emptyset, \{1\}, \{0,1\}\}$, which also happens to be the Scott topology on the poset $0 \leq 1$. The Sierpinski space acts as an 'open-set' classifier, meaning that for any open subspace $A \subseteq X$, $\chi^{-1}_A(1) = A$, where $\chi_A$ is the characteristic function 
$$\chi_A(x) = \begin{cases} 1 & \text{if } x \in A \\ 0 & \text{if }x\not\in A \end{cases}$$
Anyway, let's look at the function $\forall_X: \mathcal{O}(X) \rightarrow \Sigma$ defined as
$$\forall_X(U) = \begin{cases} 1 & \text{if } U = X \\ 0 & \text{if } U \neq X \end{cases}$$
This map is the universal quantifier over $X$ (hence the $\forall$ symbol), because its value on a subset $U$ is the truth value of the statement $\forall x \in X .(x \in U)$. It is not too hard to see that this is the right adjoint to the frame map $\mathcal{O}(1) \rightarrow \mathcal{O}(X)$, which is the map induced by the unique map $X \rightarrow 1$. (Note that $\mathcal{O}(1) = \Sigma$)
We then have:
$\textbf{Theorem. }$ A space $X$ is compact if and only if $\forall_X$ is continuous.(This is not obvious to me, but I haven't spent too much time thinking about it)
Anyway, now we are ready to dualize. We just have to look for a $\textit{left}$ adjoint to $\Sigma \rightarrow \mathcal{O}(X)$, which we find in 
$$\exists_X(U) = \begin{cases} 0 & \text{if } U = \emptyset \\ 1 & \text{else} \end{cases}$$
The notation is again inspired by the fact that on a subset $U$ the value of $\exists_X$ is the truth value of the statement $\exists x \in X.(x \in U)$. 
Now we define:
$\textbf{Definition.}$ $X$ is overt if and only if $\exists_X$ is continuous.
'Overtification' would then be a nice or natural way to take a frame/locale and 'make it overt' in the way that compactification can take a space and 'make it compact'. 
If anyone has an further reading suggestions in this area I would gladly welcome them! Thanks.
 A: I wouldn't be surprised at all if this is actually an open research question yet to be explored. It may be one more interesting from a principled perspective rather than any kind of applications, the reason being that compactification is well-behaved process primarily for Hausdorff spaces. The same duality that turns compact into overt turns Hausdorff into discrete, so the expected applicability of a result seems limited.
If we don't demand well-behavedness of compactification, there is a very simple way of embedding any given topological space into a compact one: Just add a (computable) bottom element. Meaning, we are starting with a space $(X,\tau)$, we pick some $\bot \notin X$, and now consider the space $(X\cup\{\bot\},\tau \cup \{X \cup \{\bot\})$. Since the only open set containing $\bot$ already covers the space, this new space is compact (and the original space is an open subspace).
This simple trick dualizes well: Given a space $(X,\tau)$, add a (computable) $\top$ element, i.e. consider $(X \cup \{\top\},\{\emptyset\} \cup \{U \cup \{\top\} \mid \{U \cup \{\top\} \mid U \in \tau\})$. In the new space, any non-empty open set has $\top$ as an element, hence non-emptiness is recognizable, thus the new space is overt (and the original space is a closed subspace).
