nLab contractible type

Contractible types

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contractible types

Idea

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 00. They represent the notion true in homotopy type theory.

Definition

We work in intensional type theory with dependent sums, dependent products, and identity types,

Definition

For XX a type, let

isContr(X) x:X y:X(y=x) isContr(X) \coloneqq \sum_{x\colon X} \prod_{y\colon X} (y=x)

be the dependent sum in one variable x:Xx : X over the dependent product on the other variable y:Xy \colon X of the x,yx,y-dependent identity type (x=y)(x = y).

We say that XX is a contractible type if isContr(X)isContr(X) is an inhabited type.

Remark

In propositions as types language, this can be pronounced as “there exists a point x:Xx\colon X such that every other point y:Xy\colon X is equal to xx.”

Under the homotopy-theoretic interpretation, it should be thought of as the type of contractions of XX — since the dependent product describes continuous functions, the paths from yy to xx depend continuously on yy and thus exhibit a contraction of XX to xx.

Definition

A provably equivalent definition is the product type of XX with the isProp-type of XX:

isContr(X)X×isProp(X). isContr(X) \coloneqq X \;\times\; isProp(X) \,.

(Here of course we have to use a definition of isProp which doesn’t refer to isContrisContr).

Remark

This now says that XX is contractible iff XX is inhabited and an h-proposition.

There is a third definition of a contractible type, provably equivalent to the others.

Definition

Let (A,a:A)(A, a:A) be a pointed type. AA satisfies singleton induction if for every type family BB over AA the dependent function

evpt(a):( x:AB(x))B(a)\mathrm{evpt}(a):\left(\prod_{x:A} B(x)\right) \to B(a)

has a section. A contractible type is a pointed type which satisfies singleton induction.

Rules for isContr

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:

ΓAtypeΓisContr(A)type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{isContr}(A) \; \mathrm{type}}

Introduction rules for isContr types:

ΓAtypeΓa:AΓ,x:Aτ(x):a= AxΓw(a,λx.τ(x)):isContr(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A \vdash \tau(x):a =_A x}{\Gamma \vdash w(a, \lambda x.\tau(x)):\mathrm{isContr}(A)}

Elimination rules for isContr types:

ΓAtypeΓ,p:isContr(A)pt(p):AΓAtypeΓ,p:isContr(A),x:Ac(p,x):pt(p)= Ax\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathrm{isContr}(A) \vdash \mathrm{pt}(p):A} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathrm{isContr}(A), x:A \vdash c(p, x):\mathrm{pt}(p) =_A x}

Computation rules for isContr types:

ΓAtypeΓa:AΓ,x:Aτ(x):a= AxΓβ isContr(A) pt(a):pt(w(a,λx.τ(x)))= Aa\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A \vdash \tau(x):a =_A x}{\Gamma \vdash \beta_{\mathrm{isContr}(A)}^\mathrm{pt}(a):\mathrm{pt}(w(a, \lambda x.\tau(x))) =_A a}
ΓAtypeΓa:AΓ,x:Aτ(x):a= AxΓ,x:Aβ isContr(A) w(x):c(w(a,λx.τ(x)))(x)= ()= Ax β isContr(A) pt(a)τ(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A \vdash \tau(x):a =_A x}{\Gamma, x:A \vdash \beta_{\mathrm{isContr}(A)}^w(x):c(w(a, \lambda x.\tau(x)))(x) =_{(-) =_A x}^{\beta_{\mathrm{isContr}(A)}^\mathrm{pt}(a)} \tau(x)}

Uniqueness rules for isContr types:

ΓAtypeΓ,p:isContr(A)η isContr(A)(p):w(pt(p),λx.c(p,x))= isContr(A)p\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathrm{isContr}(A) \vdash \eta_{\mathrm{isContr}(A)}(p):w(\mathrm{pt}(p), \lambda x.c(p, x)) =_{\mathrm{isContr}(A)} p}

Properties

Proposition

For any type AA, the type isContr(A)isContr(A) is an h-proposition. In particular, we can show isContr(A)isContr(isContr(A))isContr(A) \to isContr(isContr(A)): if a type is contractible, then its space of contractions is also contractible.

Proposition

A type is contractible if and only if it is equivalent to the unit type.

Relation to dependent sum types and equivalences

A family of elements x:Af(x):Bx:A \vdash f(x):B is an equivalence of types if its family of fiber types y:B x:Af(x)= Byy:B \vdash \sum_{x:A} f(x) =_B y is a family of contractible types.

The dependent sum type of a family of contractible types x:AB(x)x:A \vdash B(x) with witnesses x:Ap(x):isContr(B(x))x:A \vdash p(x):\mathrm{isContr}(B(x)) is equivalent to the index type AA itself given by the first pair projection:

z: x:AB(x)π 1(z):Az:\sum_{x:A} B(x) \vdash \pi_1(z):A
x:Ap(x):isContr( z: x:AB(x)π 1(z)= Ax)x:A \vdash p(x):\mathrm{isContr}\left(\sum_{z:\sum_{x:A} B(x)} \pi_1(z) =_A x\right)

This is due to the fact that for any family of types x:AB(x)x:A \vdash B(x), there is an equivalence

x:Aq(x):( z: x:AB(x)π 1(z)= Ax)B(x)x:A \vdash q(x):\left(\sum_{z:\sum_{x:A} B(x)} \pi_1(z) =_A x\right) \simeq B(x)

which means that if B(x)B(x) is contractible, then

z: x:AB(x)π 1(z)= Ax\sum_{z:\sum_{x:A} B(x)} \pi_1(z) =_A x

is contractible.

Categorical semantics

We discuss the categorical semantics of contractible types.

Let 𝒞\mathcal{C} be a locally cartesian closed category with sufficient structure to intepret all the above type theory. This means that 𝒞\mathcal{C} 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 A:Type\vdash A : Type is a fibrant object [A:Type][\vdash A : Type], which for short we will just write AA. The interpretation of the identity type x,y:A(x=y):Typex,y : A \vdash (x = y) : Type is as the path space object A IA×AA^I \to A \times A. The interpretation of isContr(A)isContr(A) is the object obtained by taking the dependent product of the path space object along one projection p 2:A×AAp_2 : A\times A\to A and then forgetting the remaining morphism to AA.

[isContr(A)]= p 2A I A *. [isContr(A)] \;\; = \;\; \array{ \prod_{p_2} A^I \\ \downarrow \\ A \\ \downarrow \\ * } \,.

The interpretation [a^:isContr(A)][\hat a : isContr(A)] of a term of isContr(A)isContr(A) is precisely a morphism a^:* p 2A I\hat a : * \to \prod_{p_2} A^I.

Proposition

Let 𝒞\mathcal{C} be a type-theoretic model category. Write [isContr(A)][isContr(A)] for the interpretation of isContr(A)isContr(A) in 𝒞\mathcal{C}. Then:

Global points *[isContr(A)]* \to [isContr(A)] in 𝒞\mathcal{C} are in bijection with contraction right homotopies of the object AA, hence to diagrams in 𝒞\mathcal{C} of the form

A η A I (id,const a) A×A, \array{ A &\stackrel{\eta}{\to}& A^I \\ & {}_{\mathllap{(id, const_a)}}\searrow & \downarrow \\ && A \times A } \,,

where const aconst_a is a morphism of the form A*aAA \to * \stackrel{a}{\to} A and where A IA^I is the path space object of AA in 𝒞\mathcal{C}.

Proof

Given a global point a^:* p 2A I\hat a : * \to \prod_{p_2} A^I, write a:*Aa : * \to A for the corresponding composite

* a^ p 2A I a A. \array{ * &\stackrel{\hat a}{\to} & \prod_{p_2} A^I \\ &{}_{\mathllap{a}}\searrow & \downarrow \\ && A } \,.

in 𝒞\mathcal{C}. This is an element in the hom set 𝒞 /A(a, p 2A I)\mathcal{C}_{/A}(a, \prod_{p_2} A^I) of the slice category over AA. By the (base change \dashv dependent product)-adjunction this is equivalently an element in 𝒞 /A×A(p 2 *a,A I)\mathcal{C}_{/A \times A}( p_2^* a, A^I ).

Notice that the pullback p 2 *ap_2^* a is the left morphism in

A * (id,const a) a A×A p 2 A. \array{ A &\to& * \\ {}^{\mathllap{(id,const_a)}}\downarrow && \downarrow^{\mathrlap{a}} \\ A \times A &\stackrel{p_2}{\to}& A } \,.

Therefore a morphism p 2 *aA Ip_2^* a \to A^I in 𝒞 /A×A\mathcal{C}_{/A \times A} is equivalently in 𝒞\mathcal{C} a diagram of the form

A η A I (id,const a) A×A. \array{ A &&\stackrel{\eta}{\to}&& A^I \\ & {}_{\mathllap{(id,const_a)}}\searrow && \swarrow \\ && A \times A } \,.

This is by definition a contraction right homotopy of AA.

Remark

Thus if isContr(A)isContr(A), then A1A\to 1 is a (right) homotopy equivalence, and hence (since AA is fibrant) an acyclic fibration.

Conversely, if 𝒞\mathcal{C} is a model category, AA and 11 are cofibrant, and A1A\to 1 is an acyclic fibration, then A1A\to 1 is a right homotopy equivalence, and hence isContr(A)isContr(A) has a global element. Thus, in most cases, the existence of a global element of isContr(A)isContr(A) (which is unique up to homotopy, since isContr(A)isContr(A) is an h-proposition) is equivalent to A1A\to 1 being an acyclic fibration.

More generally, we may apply this locally. Suppose that ABA\to B is a fibration, which we can regard as a dependent type

x:BA(x):Type.x\colon B \vdash A(x)\colon Type.

Then we have a dependent type

x:BisContr(A(x)):Typex\colon B \vdash isContr(A(x))\colon Type

represented by a fibration isContr(A)BisContr(A)\to B. By applying the above argument in the slice category 𝒞/B\mathcal{C}/B, we see that (if 𝒞\mathcal{C} is a model category, and AA and BB are cofibrant) isContr(A)BisContr(A)\to B has a section exactly when ABA\to B is an acyclic fibration.

We can also construct the type

x:BisContr(A(x))\prod_{x\colon B} isContr(A(x))

in global context, which has a global element precisely when isContr(A)BisContr(A)\to B has a section. Thus, a global element of this type is also equivalent to ABA\to B being an acyclic fibration.

Examples

  • 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 leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

References

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.