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
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
Axioms of cohesion are certain axioms added to any spatial type theory in order to define the shape modality for cohesive homotopy type theory. In particular, the axiom of real cohesion plays a role in defining real-cohesive homotopy type theory (the setting for classical homotopy theory and algebraic topology), and the axiom of affine cohesion plays a role in defining -cohesive homotopy type theory (the setting for -homotopy theory), where the affine line plays the role that does in real-cohesive homotopy type theory. Affine cohesion could hypothetically also be used in defining a cohesive version of Mitchell Riley‘s bunched linear homotopy type theory (the setting for stable homotopy theory) for the purposes of doing motivic homotopy theory.
We assume the presentation of spatial type theory using crisp term judgments in addition to the usual (cohesive) type and term judgments and , as well as context judgments where is a list of crisp term judgments, and is a list of cohesive term judgments. A crisp type is a type in the context , where is the empty list of cohesive term judgments. We also assume identity types, the sharp modality, and the flat modality.
Given a type , let us define to be the type of all constant functions in :
There is an equivalence between the type and the type of functions from the unit type to . Given types and and a function , type is -local if the function is an equivalence of types.
A crisp type is discrete if the function is an equivalence of types.
The axiom of cohesion for type states that there is a crisp type such that given any crisp type , is discrete if and only if is -local, or equivalently, if is an equivalence of types.
This allows us to define discreteness for non-crisp types: a type is discrete if is -local, or equivalently, if is an equivalence of types.
Another consequence is that the shape of is contractible.
Assuming a type and the axiom of -cohesion, the shape of is contractible.
The type is inhabited by , so it remains to show that for all , . Since is discrete, so is the identity type , which means by -induction, it suffices to prove for all . But this is true from the third introduction rule for .
In addition, if the type of booleans is discrete, then is compact connected:
Assuming a type , a type of all propositions with type reflector , and the axiom of -cohesion, if the function is an equivalence of types, then for all functions , if for all , is contractible, then either for all , is contractible, or for all , is contractible.
If is such that for all , is contractible, then there is a function into the booleans type with and . But if is discrete, then by -cohesion is constant, which implies that either for all , is contractible, or for all , is contractible. Thus, is compact connected if is discrete.
There are a number of axioms which in general could be called an axiom of cohesion for type . The most general such axiom of cohesion is called stable local connectedness or axiom C0, which imposes no other restrictions on . If we additionally assume that the type is pointed with point , then the axiom becomes punctual local connectedness or axiom C1, and if we additionally assume that the type is a non-trivial bi-pointed set, with points , , and witnesses and , then the axiom becomes contractible codiscreteness or axiom C2. If we additionally assume that the type is a Dedekind complete Archimedean ordered lattice field (and usually written as ), then the axiom becomes real cohesion or axiom -flat.
Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Mike Shulman, Homotopy type theory: the logic of space, New Spaces in Mathematics: Formal and Conceptual Reflections, ed. Gabriel Catren and Mathieu Anel, Cambridge University Press, 2021 (arXiv:1703.03007, doi:10.1017/9781108854429)
Last revised on January 25, 2023 at 16:30:38. See the history of this page for a list of all contributions to it.