nLab
h-proposition

Idea

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

h-Propositions are how logic is embedded into homotopy type theory, via the propositions as some types / bracket types approach.

h-Propositions are also said to be of h-level $1$.

Definition

Consider intensional type theory with dependent sums, dependent products, and identity types.

There are many equivalent definitions of a type being an h-proposition. Perhaps the simplest is as follows.

Definition

For $A$ a tpye, let $\mathrm{isProp}(A)$ denote the dependent product of the identity types for all pairs of terms of $A$:

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

We say that $A$ is an h-proposition if $\mathrm{isProp}(A)$ is an inhabited type.

In propositions as types language, this can be pronounced as “every two elements of $A$ are equal”.

Proposition

The following are two provably equivalent definitions of $\mathrm{isProp}(A)$, in terms of the dependent type $\mathrm{isContr}(-)$ that checks for contractible types:

• $\mathrm{isProp}(A)≔{\prod }_{x:A}{\prod }_{y:A}\mathrm{isContr}(x=y)$
• $\mathrm{isProp}(A)≔(A\to \mathrm{isContr}(A))$

The first fits into the general inductive definition of n-groupoid: an $\mathrm{\infty }$-groupoid is an $n$-groupoid if all its hom-groupoids are $(n-1)$-groupoids. The second says that being a proposition is equivalent to being “contractible if inhabited”.

Properties

• We can prove that for any $A$, the type $\mathrm{isProp}(A)$ is an h-proposition, i.e. $\mathrm{isProp}(\mathrm{isProp}(A))$. Thus, any two inhabitants of $\mathrm{isProp}(A)$ (witnesses that $A$ is an h-proposition) are “equal”.

• If $A$ and $B$ are h-props and there exist maps $A\to B$ and $B\to A$, then $A$ and $B$ are equivalent.

Categorical semantics

We discuss the categorical semantics of h-propositions.

Let $𝒞$ be a locally cartesian closed category with sufficient structure to intepret all the above type theory. This means that $C$ has a weak factorization system with stable path objects, and that trivial cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.)

Then for a fibrant object $A$, the object $\mathrm{isProp}(A)$ defined above (with the first definition) is obtained by taking dependent product of the path-object $A^I\to A\times A$ along the projection $A\times A\to 1$. By adjunction, a global element of $\mathrm{isProp}(A)$ is therefore equivalent to a section of the path-object, which exactly means a (right) homotopy between the two projections $A\times A\rightrightarrows A$. The existence of such a homotopy, in turn, is equivalent to saying that any two maps $X\rightrightarrows A$ are homotopic.

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

$$x:B⊢A(x):\mathrm{Type}.$$x\colon B \vdash A(x)\colon Type.

Then we have a dependent type

$$x:B⊢\mathrm{isProp}(A(x)):\mathrm{Type}$$x\colon B \vdash isProp(A(x))\colon Type

represented by a fibration $\mathrm{isProp}(A)\to B$. By applying the above argument in the slice category $𝒞/B$, we see that $\mathrm{isProp}(A)\to B$ has a section exactly when any two maps in $𝒞/B$ into $A\to B$ are homotopic over $B$. We can also construct the type

$$\prod _{x:B}\mathrm{isProp}(A(x))$$\prod_{x\colon B} isProp(A(x))

in global context, which has a global element precisely when $\mathrm{isProp}(A)\to B$ has a section.

Related concepts

• isEquiv

• isContr

• isProp

References

Coq-code for h-propositions is in

• HoTT repository