center of contraction (changes) in nLab

Showing changes from revision #4 to #5: Added | Removed | Changed

\tableofcontents

Definition

In a dependent type theory with identity types, a term a:Aa:A is a center of contraction or a centre of contraction if in the context of a variable b:Ab:A there is an identification p(b):a= Abp(b):a =_A b. If the type theory also has dependent product types, the above is equivalent to having a dependent function

p:∏ b:Aa= Abp:\prod_{b:A} a =_A b

called a contraction of AA at aa. Thus, contractons of AA at aa are witnesses that a:Aa:A is a center of contraction.

We then define the type of contractions of AA at aa as

Contr A(a)≔∏ b:Aa= Ab\mathrm{Contr}_A(a) \coloneqq \prod_{b:A} a =_A b

Rules for contraction types

If the dependent type theory does not have dependent product types, contraction types could still be defined by adding the formation, introduction, elimination, computation, and uniqueness types for contraction types

Formation rules for contraction types:

Γ⊢AtypeΓ,a:A,x:A⊢a= AxtypeΓ,a:A⊢Contr A(a)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, a:A, x:A \vdash a =_A x \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{Contr}_A(a) \; \mathrm{type}}

Introduction rules for contraction types:

Γ⊢AtypeΓ,a:A,x:A⊢a= AxΓ,a:A⊢λ(x).p(x):Contr A(a)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, a:A, x:A \vdash a =_A x}{\Gamma, a:A \vdash \lambda(x).p(x):\mathrm{Contr}_A(a)}

Elimination rules for contraction types:

Γ,a:A⊢p:Contr A(a)Γ⊢b:AΓ⊢p(b):a= Ab\frac{\Gamma, a:A \vdash p:\mathrm{Contr}_A(a) \quad \Gamma \vdash b:A}{\Gamma \vdash p(b):a =_A b}

Computation rules for contraction types:

Γ,a:A,x:A⊢p(x):a= AxΓ⊢b:AΓ⊢β Contr:(λ(x).p(x))(b)= a= Abp(b)\frac{\Gamma, a:A, x:A \vdash p(x):a =_A x \quad \Gamma \vdash b:A}{\Gamma \vdash \beta_\mathrm{Contr}:(\lambda(x).p(x))(b) =_{a =_A b} p(b)}

Uniqueness rules for contraction types:

Γ,a:A⊢p:Contr A(a)Γ⊢η Contr:p= Contr A(a)λ(x).p(x)\frac{\Gamma, a:A \vdash p:\mathrm{Contr}_A(a)}{\Gamma \vdash \eta_\mathrm{Contr}:p =_{\mathrm{Contr}_A(a)} \lambda(x).p(x)}

Properties

A type AA is a contractible type if there exists a center of contraction

isContr(A)=∑ a:AContr A(a)isContr(A) = \sum_{a:A} \mathrm{Contr}_A(a)

and a type AA is an h-proposition if every element in AA is a center of contraction

isProp(A)=∏ a:AContr A(a)isProp(A) = \prod_{a:A} \mathrm{Contr}_A(a)

The axiom K on a type states that for every element a:Aa:A, reflexivity refl A(a)\mathrm{refl}_A(a) is the center of contraction of the loop space type of aa.

See also

• contractible type
• h-proposition

References

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press ( pdf arXiv:2212.11082 ) (478 pages)