nLab
h-set

Idea

In homotopy type theory, the notion of h-set (or just a set, if no ambiguity will result) is an internalization of the notion of set / 0-truncated object.

hSets can be regarded as a way of embedding extensional type theory into intensional type theory.

Definition

Let $A$ be a type in intensional type theory with dependent sums, dependent products, and identity types. We define a new type $\mathrm{isSet}(A)$ as follows:

$$\mathrm{isSet}(A)≔\prod _{x:A}\prod _{y:A}\mathrm{isProp}(x=y)$$isSet(A) \coloneqq \prod_{x\colon A} \prod_{y\colon A} isProp(x=y)

(using any equivalent definition of the predicate isProp for h-propositions; and where ”$\prod$” denotes dependent product types and ”$=$” denotes identity types).

In other words, the only relationship between two elements of an h-set is whether they are equal; there is no room for more than one path between them. By beta-reducing this definition, we can express it as

$$\mathrm{isSet}(A)≔\prod _{x,y:A}\prod _{p,q:x=y}(p=q)$$isSet(A) \coloneqq \prod_{x,y\colon A} \prod_{p,q\colon x=y} (p=q)

In other words, any two parallel paths in $A$ are equal.

A provably equivalent definition is

$$\mathrm{isSet}(A)≔\prod _{x:A}\prod _{p:x=x}(p={\mathrm{id}}_x)$$isSet(A) \coloneqq \prod_{x\colon A} \prod_{p\colon x=x} (p=id_x)

This says that a version of Streicher’s “axiom K” holds for h-sets.

Examples

• Most (non-higher) inductive types are h-sets (assuming that all their parameters and indices are so). In particular, the type of natural numbers is an h-set. This can be proven from Theorem 1 below.

Properties

One interesting consequence of this definition is the following, first proven by Michael Hedberg (see references).

Theorem

Suppose that $A$ is a type which has decidable equality in the propositions as types logic (which is not the logic of h-propositions usually used in HoTT). In other words, the projection

$$\begin{array}{c}{\mathrm{Paths}}_A+(0\to A\times A{)}^{({\mathrm{Paths}}_A\to A\times A)}\\ \downarrow \\ A\times A\end{array}$$\array{Paths_A + (0\to A\times A)^{(Paths_A\to A\times A)}\\ \downarrow\\ A\times A}

(where ${\mathrm{Paths}}_A$ is the path type of $A$, ”+” forms the sum type, and on the right we have the $A\times A$-dependent function type into the empty type), has a section.

Then $A$ is a set.

Proof

Let $d$ be the given section. Thus, for any $x,y:A$, $d(x,y)$ is either a path from $x$ to $y$ or a function from $\mathrm{Paths}(x,y)$ to the empty type (implying that $\mathrm{Paths}(x,y)$ is also empty).

It suffices to exhibit an operation connecting any endo-path $p\in \mathrm{Paths}(x,x)$ to the identity path $1_x$. Given such a path, define $q=d(x,x)$. If $d(x,x)$ lies in the second case, then $\mathrm{Paths}(x,x)$ is empty, a contradiction since we know it contains $1_x$; hence we may assume $q\in \mathrm{Paths}(x,x)$ as well.

Let $r$ be the image of $(1_x,p)\in {\mathrm{Paths}}_{A\times A}((x,x),(x,x)$ under the section $d$. This is a path in the total space ${\mathrm{Paths}}_A$ lying over the path $(1_x,p)$ in $A$. Equivalently, it is a path in the fiber over $x$ from $(1_x,p{)}_{*}(d(x,x))$ to $d(x,x)$, where $(1_x,p{)}_{*}$ denotes transport in the fibration ${\mathrm{Paths}}_A\to A\times A$ along the path $(1_x,p)$. However, we have defined $d(x,x)=q$, and transport in a path-space is just composition, so $r$ may be regarded as a path from $qp$ to $q$. Canceling $q$, we obtain a path from $p$ to $1_x$.

Remarks

• h-sets are also called h-level $2$ types.

References

• Michael Hedberg, A coherence theorem for Martin-Löf’s type theory, J. Functional Programming, 1998

• Nicolai Kraus, A direct proof of Hedberg’s theorem, blog post