equality constructors

Abstract

In homotopy type theory, A path constructor specifies point-wise equalities or higher-dimensional identity relations within a higher inductive type.

Definition

A path constructor for a higher inductive type $A:I\to \mathrm{Type}$ generates terms of an identity type $s{=}_{P}t$ for terms $s,t:P$.

The type $P$ must be either:

• A point type $Ai$ for some $i:I$.
• A path type defined inductively over $A$.

We use higher path constructors when $P$ is a path type, generating equalities between equalities.

Examples

For the circle $S^1$, the term $\mathrm{loop}:\mathrm{base}{=}_{S^1}\mathrm{base}$ is introduced by a path constructor.

See also

Point Constructor Identity Type Quotient Inductive Type Higher Inductive Type

References

• HoTT
• altenkirch2016-qiit