Context
Topology
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Introduction
Basic concepts
-
open subset, closed subset, neighbourhood
-
topological space, locale
-
base for the topology, neighbourhood base
-
finer/coarser topology
-
closure, interior, boundary
-
separation, sobriety
-
continuous function, homeomorphism
-
uniformly continuous function
-
embedding
-
open map, closed map
-
sequence, net, sub-net, filter
-
convergence
-
categoryTop
Universal constructions
Extra stuff, structure, properties
-
nice topological space
-
metric space, metric topology, metrisable space
-
Kolmogorov space, Hausdorff space, regular space, normal space
-
sober space
-
compact space, proper map
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
-
compactly generated space
-
second-countable space, first-countable space
-
contractible space, locally contractible space
-
connected space, locally connected space
-
simply-connected space, locally simply-connected space
-
cell complex, CW-complex
-
pointed space
-
topological vector space, Banach space, Hilbert space
-
topological group
-
topological vector bundle, topological K-theory
-
topological manifold
Examples
-
empty space, point space
-
discrete space, codiscrete space
-
Sierpinski space
-
order topology, specialization topology, Scott topology
-
Euclidean space
-
cylinder, cone
-
sphere, ball
-
circle, torus, annulus, Moebius strip
-
polytope, polyhedron
-
projective space (real, complex)
-
classifying space
-
configuration space
-
path, loop
-
mapping spaces: compact-open topology, topology of uniform convergence
-
Zariski topology
-
Cantor space, Mandelbrot space
-
Peano curve
-
line with two origins, long line, Sorgenfrey line
-
K-topology, Dowker space
-
Warsaw circle, Hawaiian earring space
Basic statements
Theorems
Analysis Theorems
topological homotopy theory
Type theory
Contents
Idea
Traditionally, in mathematics and in formal topology the cover is a relation between elements of a poset and subtypes of . However, that definition is impredicative, since it requires quantifiying over subtypes. There is another definition of a cover as a relation between elements of and dependent pairs consisting of an -small index type and an embedding of types from into . However, this definition requires an existing type universe in the type theory, and not all foundations of mathematics have type universes. Nonetheless, one could annotate the cover relation using the index type of the family , in the same way that one annotates the identity types of a type with the index type in the absence of type universes. This results in a type family between elements and embeddings for every single type , and is akin to using the stack semantics of the type theory.
Definition
Ayberk Tosun in Tosun 2020 defined a formal topology as a poset with families of types , and a dependent function
such that
- for all , , and ,
- for all and , implies that for all one can construct such that for all , one can construct such that .
If one has a type universe , then the locally -small inductive cover relation is given by
If one doesn’t have type universes, then given a type , the inductive cover relation for is a higher inductive type family between elements and embeddings of types generated by the constructors
Families of types are equivalently functions , so one can express the above definition in terms of single types. A formal topology is a poset with a set , a function , a set with a function and a function , such that
- for all ,
- for all and , if , then for all , implies that one can construct a such that implies that for all , implies that one can construct a such that implies .
If one has a type universe , then the locally -small inductive cover relation is given by
If one doesn’t have type universes, then given given a type , the cover relation for is a higher inductive type family between elements and embeddings of types generated by the constructors
For the real numbers
For covers over the real numbers, one can use a generalized defintion and simply work with pairs of ratonal numbers numbers and arbitrary functions instead of embeddings.
We first define the following relations and operations on pairs of rational numbers:
The inductive covers are generated by the following inference rules:
Formation rules for inductive covers:
Introduction rules for inductive covers:
Elimination rules for inductive covers:
…
Computation rules for inductive covers:
…
Properties
The Heine-Borel theorem holds for inductive covers.
Every inductive cover on the real numbers is a pointwise cover on the real numbers. Assuming excluded middle, every pointwise cover is an inductive cover.
See also
References