Point Constructor

Idea

A point constructor specifies the standard elements or points of an inductive or higher inductive type.

Definition

A point constructor for an indexed type family $A:I\to \mathrm{Type}$ is a constructor specified by a chain of strictly-positive $\Pi$-types ¹ terminating in the type $Ai$ for some index $i:I$.

We use point constructors to generate the zero-dimensional terms of a type. They coincide with standard constructors in ordinary inductive types.

Examples

For the higher inductive type representing the circle $S^1$, the term $\mathrm{base}:S^1$ is introduced by a point constructor.

See also

Path Constructor Higher Inductive Type

References

• hott2013-book
• altenkirch2016-qiit

Footnotes

1. Pi type ↩