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).
Given a type , the axiom of -cohesion or axiom C0 such that every crisp type is discrete if and only if every function from into is a constant function. is a modality which takes types in the crisp mode to its corresponding discrete type in the cohesive mode, and a discrete type in the cohesive mode is one for which the canonical function is an equivalence of types.
The axiom of -cohesion allows us to define discreteness for non-crisp types. Given a type , let us define to be the type of all constant functions in :
Type is -null if the function is an equivalence of types.
Assuming the axiom of -cohesion, type is discrete if is -null.
Another consequence is that the shape of is contractible, i.e. the axiom of strong connectedness
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 .
Shulman 2018 showed that axiom C0 implies that every function from into a discrete type is a constant function; conversely, if every function from to a discrete type is constant, then it holds for the discrete types which are in the image of the modality. Finally, Aberlé 2024 proved that the axiom of strong connectedness holds if and only if every function from into a discrete type is a constant function
The boolean domain is discrete.
Theorem 6.19 of Shulman 18 says that the unit type is crisply discrete, and theorem 6.21 of Shulman 18 says that the sum type of two crisply discrete types is itself crisply discrete. Since the boolean domain is the sum type of two copies of the unit type, the boolean domain is crisply discrete, thus discrete.
Since the boolean domain is discrete, then the type is compact connected:
Assuming the axiom of -cohesion, if the function is an equivalence of types, then for all -indexed families of mere propositions , if for all , is contractible, then either for all , is contractible, or for all , is contractible.
If the family of mere propositions is such that for all , is contractible, then there is a function into the boolean domain with and . But since is discrete, then by -cohesion is constant, which implies that either for all , and thus is contractible, or for all , and thus is contractible. Thus, is compact connected.
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)
C.B. Aberlé, Parametricity via Cohesion [arXiv:2404.03825]
Last revised on August 27, 2024 at 08:28:45. See the history of this page for a list of all contributions to it.