Proposition/h-Proposition

A type $A$ is said to be a proposition if its identity types are contractible:

$$ \text{is-prop}(A) := \Pi_{(x,y : A)} \text{is-contr}(x = y) $$

Some equivalent definitions:

  • $\text{is-prop}(A) := \Pi_{(x,y : A)} x = y$. This means iff every pair of elements on $A$ are equal.

  • $\text{is-prop}(A) := A \rightarrow \text{is-contr}(A)$. This means iff A is not empty, and it is contractible, then it is a proposition.

  • $\text{const}_{\text{tt}} : A → ⊤$ is an embedding. This means iff A can be mapped to the unit type "injectivly", then it is a proposition.

The reason why we call it a (h-)proposition is that, in first-order logic, we don't have any way to distinguish between any two proofs of the same proposition. In here HoTT case, a proposition is a type (which corresponds to a set theory proposition) that either is empty, or contractable (ie. all of its elements, which correspond to proofs are equal).

In Agda:

is-prop : (A : Set) → Set
is-prop A = (x y : A) → is-contr (x ≡ y)

is-prop' : (A : Set) → Set
is-prop' A = (x y : A) → x ≡ y

is-prop'' : (A : Set) → Set
is-prop'' A = A → is-contr A

is-prop''' : (A : Set) → Set
is-prop''' A = is-emb (const {B = A} tt)

(h-)Set

A type $A$ is said to be a set if its identity types are propositions:

$$ \text{is-set}(A) := \Pi_{(x,y : A)} \text{is-prop}(x = y) $$

An equivalent definition is the type $A$ satisfies axiom K:

$$ \text{is-set}(A) := \Pi_{(x : A)} \Pi_{(p : x = x)} \text{refl}_x = p $$

General truncation levels

We define $\text{is-contr}(A)$ as the bottom level of the truncation hierarchy, and $\text{is-prop}(A)$ as the first, $\text{is-set}(A)$ as the second, and so on.

For some reason we want to make set to be the 0 level, thus $\text{is-contr}(A)$ is level -2 and $\text{is-prop}(A)$ is level -1.

So we define the truncation level of a type $A$ as:

$$ \begin{align} \text{is-trunc}{-2}(A) &:=& \text{is-contr}(A) \text{is-trunc}{k+1}(A) &:=& \Pi_{(x,y:A)}\text{is-trunc}_k(x = y) \end{align} $$

In Agda:

data 𝕋 : Set where
    neg-two-𝕋 : 𝕋
    succ-𝕋 : 𝕋 → 𝕋

neg-one-𝕋 : 𝕋
neg-one-𝕋 = succ-𝕋 (neg-two-𝕋)

zero-𝕋 : 𝕋
zero-𝕋 = succ-𝕋 (neg-one-𝕋)

is-trunc : (k : 𝕋) → Set → Set
is-trunc neg-two-𝕋 A = is-contr A
is-trunc (succ-𝕋 k) A = (x y : A) → is-trunc k (x ≡ y)

is-prop-is-neg-one-trunc : (A : Set) → is-prop A → is-trunc neg-one-𝕋 A
is-prop-is-neg-one-trunc A = id

is-set-is-zero-trunc : (A : Set) → is-set A → is-trunc zero-𝕋 A
is-set-is-zero-trunc A = id