natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit 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
</table>
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
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 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 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
Martín Escardó, Synthetic topology of data types and classical spaces, (pdf)
Martín Escardó, The topology of Seemingly impossible functional programs, (pdf)
Andrej Bauer, Davorin Lešnik, Metric Spaces in Synthetic Topology, (pdf)
Davorin Lešnik, Synthetic Topology and Constructive Metric Spaces,PhD
Davorin Lešnik, Unified Approach to Real Numbers in Various Mathematical Settings, 1402.6645
Steven Vickers, Locales and toposes as spaces, PDF
Last revised on March 1, 2017 at 16:57:02. See the history of this page for a list of all contributions to it.