nLab synthetic topology

Idea

Synthetic topology, like synthetic domain theory, synthetic differential geometry, and synthetic computability, are part of synthetic mathematics. It uses the internal logic of a topos to develop a part of mathematics. In this case topology. This is closely related to topology via logic and abstract Stone duality. One example of synthetic topology is synthetic Stone duality.

The formal system of type theory has semantics in many categories, and in particular in many categories of “spaces”. Thus types may be regarded not just as sets but as topological objects. Interestingly, a good deal of this “topology” can be detected intrinsically in type theory, often corresponding to the possible failure of principles of classical mathematics.

Dictionary

Martín Escardó has given the following translations between the two fields:

general topology	type theory
space	type
continuous function	function
clopen set	decidable set
open set	semi-decidable? set
closed set	set with semi-decidable complement
discrete space	type with decidable equality
Hausdorff space	type with semi-decidable inequality
convergent sequence	map out of $\mathbb{N}_\infty$ (see below)
compact set	exhaustively searchable set, in a finite number of steps

It should be stressed that the concepts on the right are not the only ways to represent the topological concepts on the left in type theory. For instance, in cohesive homotopy type theory there is a notion of “discrete space” that has nothing to do with decidable equality (in particular, in homotopy type theory a type with decidable equality is necessarily an h-set, whereas discrete spaces don’t need to be h-sets).

Semantics

There are many different topological semantics for type theory, but one which seems especially closely related to the above dictionary is the topological topos. For instance, in that case the internally defined set $\mathbb{N}_\infty$ (the set of infinite decreasing binary sequences) really does get interpreted semantically as “the generic convergent sequence”.

Implementation

Many of the results that have originated from this view have been implemented in an Agda library.

Related pages

• dominance
• open subset
• overt space
• synthetic Stone duality

References

• Martín Escardó, Synthetic topology of data types and classical spaces, 2004 (pdf)

• Martín Escardó, The topology of seemingly impossible functional programs, 2012 (pdf, almost same presentation with minor changes pdf)

• Andrej Bauer, Davorin Lešnik, Metric Spaces in Synthetic Topology, 2010 (pdf)

• Davorin Lešnik, Synthetic Topology and Constructive Metric Spaces, PhD, 2010 (arXiv:2104.10399)

• Davorin Lešnik, Unified Approach to Real Numbers in Various Mathematical Settings, 2014 (arXiv:1402.6645)

• Steven Vickers, Locales and toposes as spaces, 2007 (pdf)

• Felix Cherubini, Thierry Coquand, Freek Geerligs, Hugo Moeneclaey, A Foundation for Synthetic Stone Duality (arXiv:2412.03203)