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 can be defined by localization of a type at the circle type . This means that a type is 0-truncated, i.e. a set, if it is -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 -local, or that the canonical function , which takes elements of to constant functions in , is an equivalence of types. This is (tentatively) called the axiom of circle type localization or the axiom of -localization.
Assuming that one has the function defined in the dependent type theory, the syntactic rules for the axiom of -localization in a universe is given by:
Since the boolean domain is -local, the axiom of -localization implies that is compact connected:
Assuming propositional truncation, where is the type of all -small propositions with type reflector , and the axiom of -localization, 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 . Since is -local, then, by the axiom of -localization, is constant, which implies that either for all , is contractible, or for all , is contractible. Thus, is compact connected
In spatial type theory, a crisp type is discrete if the function is an equivalence of types. There is a variant of the above axiom called the axiom of circle type cohesion or axiom , which states that given any crisp type , is discrete if and only if is -local, or if is an equivalence of types.
This allows us to define discreteness for non-crisp types: a type is discrete if is -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 May 21, 2023 at 12:55:53. See the history of this page for a list of all contributions to it.