nLab dominance




In synthetic topology done as a branch of constructive mathematics, a dominance is a set Σ\Sigma that functions as an analogue of the Sierpinski space. In particular, it allows us to define synthetically a notion of open subset: Σ\Sigma is a subset of the set of truth values Ω\Omega, and a subset of a set AA is called “open” if its classifying map AΩA\to \Omega lands in Σ\Sigma.

The name dominance is meant to evoke that the set is used to define the domains of a class of partial functions. I.e., in synthetic topology the partial functions whose domain is an open set and in synthetic computability theory the domains of partial computable functions.


Let Ω\Omega be the set of truth values. A dominance is a subset ΣΩ\Sigma\subseteq \Omega such that

  1. Σ\top \in \Sigma, and
  2. If UΣU\in\Sigma and PΩP\in\Omega and U(PΣ)U\Rightarrow (P\in \Sigma), then UPΣU\wedge P \in \Sigma.

The second condition implies that Σ\Sigma is closed under binary meets \wedge, and hence is a sub-meet-semilattice of Ω\Omega. In type-theoretic language, the second condition says that Σ\Sigma is closed under dependent sums.

The elements of Σ\Sigma are called open truth values.

In homotopy type theory

In homotopy type theory, every univalent type of propositions is a subtype of the type of all propositions Ω\Omega. A dominance is a univalent type of propositions (Σ,El Σ)(\Sigma, \mathrm{El}_\Sigma) with an element :Σ\top:\Sigma such that

  • El Σ()\mathrm{El}_\Sigma(\top) is a contractible type
  • given a mere proposition PP, for all elements U:ΣU:\Sigma with a function from El Σ(U)\mathrm{El}_\Sigma(U) to the type that PP is essentially Σ\Sigma-small, the product type El Σ(U)×P\mathrm{El}_\Sigma(U) \times P is essentially Σ\Sigma-small.
    ΓPtypeΓp:isProp(P)Γ,U:Σq:(El Σ(U) B:ΣEl Σ(B)P)( C:ΣEl Σ(C)El Σ(U)×P)\frac{\Gamma \vdash P \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(P)}{\Gamma, U:\Sigma \vdash q:\left(\mathrm{El}_\Sigma(U) \to \sum_{B:\Sigma} \mathrm{El}_\Sigma(B) \simeq P\right) \to \left(\sum_{C:\Sigma} \mathrm{El}_\Sigma(C) \simeq \mathrm{El}_\Sigma(U) \times P\right)}

Open subsets

We define a subset UAU\subseteq A of an arbitrary set AA to be open if for each xAx\in A, the proposition “xUx\in U” is an open truth value. The second condition above is equivalent to saying that if UAU\subseteq A is open and also VUV\subseteq U is open, then VAV\subseteq A is open.

Note that for any function f:ABf:A\to B, the preimage of any open set is open, since (xf 1(U))(f(x)U)(x\in f^{-1}(U))\iff (f(x) \in U). Thus, any function is “continuous” with respect to this “intrinsic topology.”

Overt sets

It is hard to get very far without an additional assumption that Σ\Sigma is closed under some joins as well. However, if it were closed under all joins, then it would be all of Ω\Omega, since any PΩP\in \Omega is the join i{|P}\bigvee_{i\in \{\star | P\}} \top.

Given a dominance Σ\Sigma, we say that a set II is overt if Σ\Sigma is closed under II-indexed joins. (This is related to, but not identical to, the notion of overt space.) In general it is reasonable to expect discrete sets to be overt in this sense. In some frameworks such as spatial type theory there is a formal notion of “discrete” and we can actually assert that all discrete sets are overt. Otherwise we can assume that specific sets that we expect to be discrete are overt. For instance, we might assume that:

  • The empty set is overt, i.e. Σ\bot\in\Sigma.
  • Finite sets are overt, i.e. Σ\Sigma is also a sub-join-semilattice of Ω\Omega.
  • The natural numbers are overt, i.e. Σ\Sigma is closed under countable joins in Ω\Omega.


  • The singleton {}\{\top\} is a dominance, for which only singletons are overt.

  • The set {,}\{\bot,\top\} is a dominance. This is the smallest dominance such that the empty set is overt. (In classical mathematics, of course, this and the previous example are the only two dominances, and the theory trivializes.)

  • The set of all truth values of the form n,f(n)=1\exists n, f(n) = 1 for some function f:2f:\mathbb{N}\to \mathbf{2} is often a dominance, though this may not be provable without further assumptions. For instance, this is the case if we assume countable choice or (perhaps) the propositional axiom of choice. When it is a dominance, this is the smallest dominance such that \mathbb{N} is overt; it is called the Rosolini dominance. Equivalently, it is the set of truth values of the form x>0x\gt 0 for some Cauchy real number xx.

  • The set of all truth values of the form x>0x\gt 0 for some Dedekind real number xx is also often a dominance, though this also may not be provable without further assumptions.

See also


  • G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986. pdf

  • Martin Escardo, Topology via higher-order intuitionistic logic., unfinished paper, pdf

  • Martin Escardo, Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004. pdf

  • Andrej Bauer and Davorin Lesnik, Metric Spaces in Synthetic Topology, pdf

Last revised on February 10, 2023 at 20:35:05. See the history of this page for a list of all contributions to it.