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).
We assume the presentation of spatial type theory using crisp term judgments $a::A$ in addition to the usual (cohesive) type and term judgments $A \; \mathrm{type}$ and $a:A$, as well as context judgments $\Xi \vert \Gamma \; \mathrm{ctx}$ where $\Xi$ is a list of crisp term judgments, and $\Gamma$ is a list of cohesive term judgments. A crisp type is a type in the context $\Xi \vert ()$, where $()$ is the empty list of cohesive term judgments. We also assume identity types, the sharp modality, and the flat modality.
Given a type $A$, let us define $\mathrm{const}_{A, R}:A \to (R \to A)$ to be the type of all constant functions in $R$:
There is an equivalence $\mathrm{const}_{A, 1}:A \simeq (1 \to A)$ between the type $A$ and the type of functions from the unit type $1$ to $A$. Given types $B$ and $C$ and a function $F:(B \to A) \to (C \to A)$, type $A$ is $F$-local if the function $F:(B \to A) \to (C \to A)$ is an equivalence of types.
A crisp type $\Xi \vert () \vdash A$ is discrete if the function $(-)_\flat:\flat A \to A$ is an equivalence of types.
The axiom of cohesion for type $R$ states that there is a crisp type $\Xi \vert () \vdash R \; \mathrm{type}$ such that given any crisp type $\Xi \vert () \vdash A \; \mathrm{type}$, $A$ is discrete if and only if $A$ is $(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, R})$-local, or equivalently, if $\mathrm{const}_{A, R}$ is an equivalence of types.
This allows us to define discreteness for non-crisp types: a type $A$ is discrete if $A$ is $(\mathrm{const}_{A, 1}^{-1} \circ \mathrm{const}_{A, R})$-local, or equivalently, if $\mathrm{const}_{A, R}$ is an equivalence of types.
Another consequence is that the shape of $R$ is contractible.
Assuming a type $R$ and the axiom of $R$-cohesion, the shape of $R$ is contractible.
The type $R$ is inhabited by $\kappa_R(\sigma_R)$, so it remains to show that for all $x:\esh R$, $x =_{\esh R} \kappa_R(\sigma_R)$. Since $\esh R$ is discrete, so is the identity type $x =_{\esh R} \kappa_R(\sigma_R)$, which means by $\esh$-induction, it suffices to prove $\sigma_R(x) =_{\esh R} \kappa_R(\sigma_R)$ for all $x:\esh R$. But this is true from the third introduction rule for $\esh R$.
In addition, if the type of booleans $\mathbb{2}$ is discrete, then $R$ is compact connected:
Assuming a type $R$, a type of all propositions $\Omega$ with type reflector $T$, and the axiom of $R$-cohesion, if the function $\mathrm{const}_{2, R}$ is an equivalence of types, then for all functions $P:R \to \Omega$, if for all $x:R$, $T(P(x)) \vee \neg T(P(x))$ is contractible, then either for all $x:R$, $T(P(x))$ is contractible, or for all $x:R$, $\neg T(P(x))$ is contractible.
If $P:R \to \Omega$ is such that for all $x:R$, $T(P(x)) \vee \neg T(P(x))$ is contractible, then there is a function $P':R \to \mathbb{2}$ into the booleans type $\mathbb{2}$ with $\delta_{P'}^{1_2}(x):(P'(x) = 1_2)) \simeq T(P(x))$ and $\delta_{P'}^{0_2}(x):(P'(x) = 0_2)) \simeq \neg T(P(x))$. But if $\mathbb{2}$ is discrete, then by $R$-cohesion $P'$ is constant, which implies that either for all $x:R$, $T(P(x))$ is contractible, or for all $x:R$, $\neg T(P(x))$ is contractible. Thus, $R$ is compact connected if $\mathbb{2}$ is discrete.
There are a number of axioms which in general could be called an axiom of cohesion for type $R$. The most general such axiom of cohesion is called stable local connectedness or axiom C0, which imposes no other restrictions on $R$. If we additionally assume that the type $R$ is pointed with point $0:R$, then the axiom becomes punctual local connectedness or axiom C1, and if we additionally assume that the type $R$ is a non-trivial bi-pointed set, with points $0:R$, $1:R$, and witnesses $\tau_0:\mathrm{isSet}(R)$ and $\mathrm{nontriv}:(0 =_{R} 1) \to \emptyset$, then the axiom becomes contractible codiscreteness or axiom C2. If we additionally assume that the type $R$ is a Dedekind complete Archimedean ordered lattice field (and usually written as $\mathbb{R}$), then the axiom becomes real cohesion or axiom $\mathbb{R}$-flat.
number/symbol | name | associated shape modality | additional requirements |
---|---|---|---|
$C_0$ | cohesion/stable local connectedness | localization at a type $R$ | |
$C_1$ | punctual cohesion/punctual local connectedness | localization at a pointed type $R$ | |
$C_2$ | contractible codiscreteness | localization at a non-trivial bi-pointed h-set $R$ | |
discrete cohesion | localization at a contractible type $R$ | ||
compact connectedness | localization at a type $R$ | the type of booleans $\mathbb{2}$ is discrete | |
continuum cohesion | localization at a Hausdorff space $R$ | $\mathbb{2}$ is discrete. | |
metric continuum cohesion | localization at a metric space $R$ | $\mathbb{2}$ is discrete. | |
$\mathbb{R} \flat$ | real cohesion | localization at the real numbers $\mathbb{R}$ | A higher coinductive type representing the homotopy terminal Archimedean ordered field $\mathbb{R}$ |
$\mathbb{R} \flat$ | real cohesion (impredicative) | localization at the impredicative Dedekind real numbers or generalized Cauchy real numbers $\mathbb{R}$ | A type of all propositions $\Omega$ |
$\mathbb{R}_{U} \flat$ | locally $U$-small real cohesion | localization at the $U$-Dedekind real numbers or $U$-generalized Cauchy real numbers $\mathbb{R}_U$ | A Tarski universe $(U, T)$ |
unit interval cohesion | localization at the unit interval $[0, 1]$ | a higher coinductive type representing the homotopy terminal dyadic interval coalgebra. | |
$U$-small unit interval cohesion | localization at the $U$-small unit interval $[0, 1]_\mathbb{U}$ | A Tarski universe $(U, T)$. | |
smooth cohesion | localization at a local Artin $\mathbb{R}$-algebra | A local Artin $\mathbb{R}$-algebra $R$ | |
$S^1 \flat$ | circle type cohesion | localization at the circle type | The circle type $S^1$ |
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 June 22, 2024 at 17:48:03. See the history of this page for a list of all contributions to it.