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
basic constructions:
strong axioms
further
In dependent type theory, the 0-truncation modality of a type $A$ can be defined by localization of a type $A$ at the circle type $S^1$. This means that a type $A$ is 0-truncated, i.e. a set, if it is $S^1$-local, which means that, in addition to axiom K and uniqueness of identity proofs, there is another way to make the types of a universe into sets: by stipulating that every type is $S^1$-local, or that the canonical function
which takes elements of $A$ to constant functions in $S^1 \to A$, is an equivalence of types. This is (tentatively) called the axiom of circle type localization or the axiom of $S^1$-localization.
Assuming that one has the function $\mathrm{const}_{A, S^1}:A \to (S^1 \to A)$ defined in the dependent type theory, the syntactic rules for the axiom of $S^1$-localization in a universe $\mathcal{U}$ is given by:
There is also a definitional version of $S^1$-localization which says that $\mathrm{const}_{A, S^1}$ is a definitional isomorphism:
One can prove axiom K (positive copy induction rules) from the axiom of circle type localization (negative copy inference rules):
Suppose that every type $A$ is definitionally $S^1$-local.
Then definitional axiom K holds: given any type $A$, and any type family $C(p)$ indexed by loops $p:S^1 \to A$ in $A$, and given any dependent function $t:\prod_{x:A} C(\lambda i:S^1.x)$ which says that for all elements $x:A$, there is an element of the type defined by substituting the constant loop of $x:A$ into $C$, $C(\lambda i:S^1.x)$, one can construct a dependent function $K_A(t):\prod_{z:S^1 \to A} C(z)$ such that for all $x:A$, $K_A(t, \lambda i:S^1.x) \equiv t(x):C(\lambda i:S^1.x)$.
$K_A(t)$ is defined to be
and by the computation rules of loop types as negative copies, one has that for all $x:A$,
and so by definition of $\mathrm{ind}_{S^1 \to A}(t)$ and the judgmental congruence rules for substitution, one has
One has the following analogies between localization at a specific type and the type theoretic letter rule that it proves:
localization rule | type theoretic letter rule |
---|---|
$\mathbb{I}$-localization | J-rule |
$S^1$-localization | K-rule |
Since the boolean domain $\mathbb{2}$ is $S^1$-local, the axiom of $S^1$-localization implies that $S^1$ is compact connected:
Assuming propositional truncation, where $\Omega$ is the type of all $\mathcal{U}$-small propositions with type reflector $T$, and the axiom of $S^1$-localization, if the function $\mathrm{const}_{2, S^1}$ is an equivalence of types, then for all functions $P:S^1 \to \Omega$, if for all $x:S^1$, $T(P(x)) \vee \neg T(P(x))$ is contractible, then either for all $x:S^1$, $T(P(x))$ is contractible, or for all $x:S^1$, $\neg T(P(x))$ is contractible.
If $P:S^1 \to \Omega$ is such that for all $x:S^1$, $T(P(x)) \vee \neg T(P(x))$ is contractible, then there is a function $P':S^1 \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))$. Since $\mathbb{2}$ is $S^1$-local, then, by the axiom of $S^1$-localization, $P'$ is constant, which implies that either for all $x:S^1$, $T(P(x))$ is contractible, or for all $x:S^1$, $\neg T(P(x))$ is contractible. Thus, $S^1$ is compact connected
In spatial type theory, a crisp type $\Xi \vert () \vdash A$ is discrete if the function $(-)_\flat:\flat A \to A$ is an equivalence of types. There is a variant of the above axiom called the axiom of circle type cohesion or axiom $S^1 \flat$, which states that given any crisp type $\Xi \vert () \vdash A \; \mathrm{type}$, $A$ is discrete if and only if $A$ is $S^1$-local, or if $\mathrm{const}_{A, S^1}$ is an equivalence of types.
This allows us to define discreteness for non-crisp types: a type $A$ is discrete if $A$ is $S^1$-local, resulting in a flavor of cohesive homotopy type theory where the shape modality is the 0-truncation modality. This rule is equivalent to the axiom of circle type localization if every type is discrete.
Last revised on December 31, 2023 at 17:59:33. See the history of this page for a list of all contributions to it.