synthetic topology


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type

falseinitial objectempty type

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language


homotopy levels



topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory


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 of part of mathematics. In this case topology. This is closely related to topology via logic and abstract 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.


Martin Escardo has given the following translations between the two fields;

general topologytype theory
continuous functionfunction
clopen setdecidable set
open setsemi-decidable set
closed setset with semi-decidable complement
discrete spacetype with decidable equality
Hausdorff spacetype with semi-decidable inequality
convergent sequencemap out of \mathbb{N}_\infty (see below)
compact setexhaustively 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 hset?, whereas discrete spaces don’t need to be hsets).


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 infinity non-decreasing binary sequences) really does get interpreted semantically as the “generic convergent sequence”.


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


Last revised on March 1, 2017 at 16:57:02. See the history of this page for a list of all contributions to it.