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
In homotopy type theory, the notion of contractible type is an internalization of the notion of contractible space / (-2)-truncated object.
Contractible types are also called of h-level . They represent the notion true in homotopy type theory.
We work in intensional type theory with dependent sums, dependent products, and identity types,
For a type, let
be the dependent sum in one variable over the dependent product on the other variable of the -dependent identity type .
We say that is a contractible type if is an inhabited type.
In propositions as types language, this can be pronounced as “there exists a point such that every other point is equal to .”
Under the homotopy-theoretic interpretation, it should be thought of as the type of contractions of — since the dependent product describes continuous functions, the paths from to depend continuously on and thus exhibit a contraction of to .
A provably equivalent definition is the product type of with the isProp-type of :
(Here of course we have to use a definition of isProp which doesn’t refer to ).
This now says that is contractible iff is inhabited and an h-proposition.
There is a third definition of a contractible type, provably equivalent to the others.
Let be a pointed type. satisfies singleton induction if for every type family over the dependent function
has a section. A contractible type is a pointed type which satisfies singleton induction.
If the dependent type theory only has rules for identity types and dependent identity types, one could define the isContr modality by the following rules:
Formation rules for isContr types:
Introduction rules for isContr types:
Elimination rules for isContr types:
Computation rules for isContr types:
Uniqueness rules for isContr types:
For any type , the type is an h-proposition. In particular, we can show : if a type is contractible, then its space of contractions is also contractible.
A type is contractible if and only if it is equivalent to the unit type.
A family of elements is an equivalence of types if its family of fiber types is a family of contractible types.
The dependent sum type of a family of contractible types with witnesses is equivalent to the index type itself given by the first pair projection:
This is due to the fact that for any family of types , there is an equivalence
which means that if is contractible, then
is contractible.
We discuss the categorical semantics of contractible types.
Let be a locally cartesian closed category with sufficient structure to intepret all the above type theory. This means that has a weak factorization system with stable path objects, and that acyclic cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.)
In this categorical semantics, the interpretation of a type is a fibrant object , which for short we will just write . The interpretation of the identity type is as the path space object . The interpretation of is the object obtained by taking the dependent product of the path space object along one projection and then forgetting the remaining morphism to .
The interpretation of a term of is precisely a morphism .
Let be a type-theoretic model category. Write for the interpretation of in . Then:
Global points in are in bijection with contraction right homotopies of the object , hence to diagrams in of the form
where is a morphism of the form and where is the path space object of in .
Given a global point , write for the corresponding composite
in . This is an element in the hom set of the slice category over . By the (base change dependent product)-adjunction this is equivalently an element in .
Notice that the pullback is the left morphism in
Therefore a morphism in is equivalently in a diagram of the form
This is by definition a contraction right homotopy of .
Thus if , then is a (right) homotopy equivalence, and hence (since is fibrant) an acyclic fibration.
Conversely, if is a model category, and are cofibrant, and is an acyclic fibration, then is a right homotopy equivalence, and hence has a global element. Thus, in most cases, the existence of a global element of (which is unique up to homotopy, since is an h-proposition) is equivalent to being an acyclic fibration.
More generally, we may apply this locally. Suppose that is a fibration, which we can regard as a dependent type
Then we have a dependent type
represented by a fibration . By applying the above argument in the slice category , we see that (if is a model category, and and are cofibrant) has a section exactly when is an acyclic fibration.
We can also construct the type
in global context, which has a global element precisely when has a section. Thus, a global element of this type is also equivalent to being an acyclic fibration.
The unit type is a contractible type.
The interval type is a contractible type.
Every cone type is a contractible type, of which the unit type (cone type of the empty type) and the interval type (cone type of the unit type) are examples of cone types.
homotopy level | n-truncation | homotopy theory | higher category theory | higher topos theory | homotopy type theory |
---|---|---|---|---|---|
h-level 0 | (-2)-truncated | contractible space | (-2)-groupoid | true/unit type/contractible type | |
h-level 1 | (-1)-truncated | contractible-if-inhabited | (-1)-groupoid/truth value | (0,1)-sheaf/ideal | mere proposition/h-proposition |
h-level 2 | 0-truncated | homotopy 0-type | 0-groupoid/set | sheaf | h-set |
h-level 3 | 1-truncated | homotopy 1-type | 1-groupoid/groupoid | (2,1)-sheaf/stack | h-groupoid |
h-level 4 | 2-truncated | homotopy 2-type | 2-groupoid | (3,1)-sheaf/2-stack | h-2-groupoid |
h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | (4,1)-sheaf/3-stack | h-3-groupoid |
h-level | -truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h--groupoid |
h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid |
isContr
The notion of contractible types (and with it the modern notion of equivalence in homotopy type theory) originates around:
Textbook account:
Coq-code for contractible types:
Last revised on June 21, 2023 at 13:00:14. See the history of this page for a list of all contributions to it.