|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
For a type, let
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 .
(Here of course we have to use a definition of isProp which doesn’t refer to ).
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.
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 .
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
Notice that the pullback is the left morphism in
Therefore a morphism in is equivalently in a diagram of the form
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
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.
|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||(-1)-groupoid/truth value||(0,1)-sheaf||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||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||(4,1)-sheaf||h-3-groupoid|
Coq-code for contractible types is at