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:
There is also a definitional version of -localization which says that 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 is definitionally -local.
Then definitional axiom K holds: given any type , and any type family indexed by loops in , and given any dependent function which says that for all elements , there is an element of the type defined by substituting the constant loop of into , , one can construct a dependent function such that for all , .
is defined to be
and by the computation rules of loop types as negative copies, one has that for all ,
and so by definition of 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 |
---|---|
-localization | J-rule |
-localization | K-rule |
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 December 31, 2023 at 17:59:33. See the history of this page for a list of all contributions to it.