This note corresponds to Ch. 3 in the HoTT book

This chapter is dedicated to the study of `HSet` (sets, the $0$-type), `HProp` (mere propositions, the $(-1)$-type), and `Contr` (contractible types, the $(-2)$-type):

```
Notation Contr := (IsTrunc minus_two).
Notation IsHProp := (IsTrunc minus_two.+1).
Notation IsHSet := (IsTrunc minus_two.+2).
```

focusing on the logic of mere propositions and the notion of `propositional truncation`.

## Sets and $n$-types

A type $A$ is a `set` if forall $x, y : A$ and $p, q : x = y$, we have $p = q$. The proposition $\texttt{isSet}(A)$ is defined to be the type:

$$ \texttt{isSet}(A) = \Pi_{x, y : A} \Pi_{p, q : x = y} (p = q) $$

Sets in homotopy type theory are not like sets in ZF set theory, in that there is no global "membership predicate" $\in$. To provide some examples of sets, $\mathbb{1}$, $\mathbb{0}$ and $\mathbb{N}$ are sets.

```
Global Instance hprop_Empty : IsHProp Empty.
Proof. intro x. destruct x. Defined.
```

```
Corollary hset_nat : IsHSet nat.
Proof.
exact _.
Defined.
```

Moreover, if $A$ and $B$ are sets, then so is $A \times B$. For given $x, y : A \times B$ and $p, q : x = y$, we have $p = \texttt{pair}^=(\texttt{ap}_{\texttt{pr}_1}(p), \texttt{ap}_{\texttt{pr}_2}(p))$ and $q = \texttt{pair}^=(\texttt{ap}_{\texttt{pr}_1}(q), \texttt{ap}_{\texttt{pr}_2}(q))$. But $\texttt{ap}_{\texttt{pr}_1}(p) = \texttt{ap}_{\texttt{pr}_1}(q)$ since $A$ is a set, and $\texttt{ap}_{\texttt{pr}_2}(p) = \texttt{ap}_{\texttt{pr}_2}(q)$, since $B$ is a set; hence $p = q$.

Similarly, if $A$ is a set, and $B : A \rightarrow \mathscr{U}$ such that $B(x)$ is a set, then $\Sigma_{x : A} B(x)$ is a set

Given $B : A \rightarrow \mathscr{U}$, $\Pi_{x : A} B(x)$ is a set. For suppose $f, g : \Pi_{x : A} B(x)$ and for $p, q : f = g$. By functional extensionality,

$$ p = \texttt{funext}(x \mapsto \texttt{happly}(p, x)) \quad q = \texttt{funext}(x \mapsto \texttt{happly}(q, x)) $$

But for $x : A$, we have

$$ \texttt{happly}(p, x) : f(x) = g(x) \quad \texttt{happly}(q, x) : f(x) = g(x) $$

So since $B(x)$ is a set, we have $\texttt{happly}(p, x) = \texttt{happly}(q, x)$. Now, using funext again, the dependent functions $(x \mapsto \texttt{happly}(p, x))$ and $(x \mapsto \texttt{happly}(q, x))$ are equal, and hence, applying $\texttt{ap}_\texttt{funext}$, so are $p$ and $q$.

```
Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a) | 100.
```

Sets are just the first rung of the ladder of $n$-types, and may also be called the $0$-type; its defining property is that it has no non-trivial paths. Similarly, the $1$-type can be has no non-trivial paths between paths.

`Notation Is1Type := IsTrunc 1.`

A type $A$ is a $1$-type if for all $x, y : A$, and $p, q : x = y$, $r, s : p = q$, we have $r = s$. We can similarly define $2$-types, $3$-types, and so on.

If $A$ is a set, that is, $\texttt{isSet}(A)$ is inhabitated, then $A$ is a $1$-type.

```
(** Truncation levels are cumulative. *)
Global Instance trunc_succ `{IsTrunc n A}
: IsTrunc n.+1 A | 1000.
Proof.
generalize dependent A.
simple_induction n n IH; simpl; intros A H x y.
- apply contr_paths_contr.
- apply IH, H.
Qed.
```

Another fact to keep in mind is that this stratification of types is not degenerate; in particular, not all types are sets. For instance, universe $\mathscr{U}$ is not a set.

```
Definition not_hset_Type : ~ (IsHSet Type).
Proof.
intro HT.
apply true_ne_false.
pose (r := path_ishprop (path_universe equiv_negb) 1).
refine (_ @ (ap (fun q => transport idmap q false) r)).
symmetry; apply transport_path_universe.
Defined.
```

## Propositions as types?

Our previous straightforward interpretation of "propositions as types" do not work anymore. The statements of `double negation` and `law of excluded middle` do not function as they do in classical type theory; in particular, they are incompatible with the univalence axiom.

For $A : \mathscr{U}$, we do not have $\neg(\neg A) \rightarrow A$.

For $A : \mathscr{U}$, we do not have $A + \neg A$.

## Mere propositions

Propositions-as-types have good and bad properties. Both have a common cause: when types are viewed as propositions, they contain more information than mere truth or falsity, and all "logical" constructions on them must respect this additional information. This suggests that we could obtain a more conventional logic by restricting attention to types that do not contain any more information than the truth value, and only regarding these as logical propositions.

Indeed, if $A$ will be "true" if it is inhabitated, and false if its inhabit yields a contradiction (i.e. $A \rightarrow \mathbb{0}$). Now, for example, if we're given an element of $\mathbb{2}$, it contains one bit of additional information: which element of $\mathbb{2}$ we are given. By contrast, when we're given an element of $\mathbb{1}$ (i.e. $\star$), we receive no more information than the mere fact that $\mathbb{1}$ contains an element, since any two elements of $\mathbb{1}$ are equal to each other. This suggests the following definition:

Type $P$ is a `mere proposition` if forall $x, y : P$, we have $x = y$.

For $P : \mathscr{U}$,

$$ \texttt{isProp}(P) :\equiv \Pi_{x, y : P} x = y $$

Thus, to assert that $P$ is a mere proposition means to exhibit an inhabitant of $\texttt{isProp}(P)$, which is a dependent function connecting any two elements of $P$ by a path. The continuity/naturality of this function impiles not only that any two elements of $P$ are equal, but also that $P$ contains no higher homotopies either.

If $P$ is a mere proposition, and $x_0 : P$, then $P \simeq \mathbb{1}$.

```
(** If an hprop is inhabited, then it is equivalent to [Unit]. *)
Lemma if_hprop_then_equiv_Unit (hprop : Type) `{IsHProp hprop} : hprop -> hprop <~> Unit.
Proof.
intro p.
apply equiv_iff_hprop.
- exact (fun _ => tt).
- exact (fun _ => p).
Defined.
```

If $P$ and $Q$ are mere propositions such that $P \rightarrow Q$ and $Q \rightarrow P$, then $P \simeq Q$.

```
(** Two propositions are equivalent as soon as there are maps in both directions. *)
Definition isequiv_iff_hprop `{IsHProp A} `{IsHProp B}
(f : A -> B) (g : B -> A)
: IsEquiv f.
Proof.
apply (isequiv_adjointify f g);
intros ?; apply path_ishprop.
Defined.
```

A space that is homotopy equivalent to $\mathbb{1}$ is said to be contractible. Thus, any mere proposition that is inhabitated is contractible. On the other hand, the uninhabited type $\mathbb{0}$ is also vacuously a mere proposition.

Note that a type $A$ is a set if and only if, for $x, y : A$, the identity type $x =_A y$ is a mere proposition.

Every mere proposition is a set.

For any type $A$, types $\texttt{isProp}(A)$ and $\texttt{isSet}(A)$ are mere propositions.

```
(** Truncatedness is an hprop. *)
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A) | 0.
```

## Classical versus intuitionistic logic

With the notion of mere proposition, we can now give a proper formulation of LEM and double negation:

$$ \texttt{LEM} :\equiv \Pi_{A : \mathscr{U}} (\texttt{isProp}(A) \rightarrow (A + \neg A)) \\ \Pi_{A : \mathscr{U}} (\texttt{isProp}(A) \rightarrow (\neg\neg A \rightarrow A)) $$

These are seen as being logically equivalent to each other. Renaming for clarity:

$$ \texttt{LEM}_\infty :\equiv \Pi_{A : \mathscr{U}} (A + \neg A) $$

- A type $A$ is `decidable` if $A + \neg A$.
- A type family $B : A \rightarrow \mathscr{U}$ is decidable if $\Pi_{a : A}(B(a) + \neg B(a))$.
- $A$ has decidable equality if $\Pi_{a, b : A} ((a = b) + \neg(a = b))$.

```
Class Decidable (A : Type) :=
dec : A + (~ A).
```

```
Class DecidablePaths (A : Type) :=
dec_paths : forall (x y : A), Decidable (x = y).
```

## Subsets and propositional resizing

Suppose $P : A \rightarrow \mathscr{U}$ is a type family with each type $P(x)$ regarded as a proposition. Then $P$ itself is a predicate on $A$, or a property of elements of $A$. What we regard as $\{x \in A \mid P(x)\}$ in set theory can be regarded as $\Sigma_{x : A} P(x)$ in type theory. For a general element $P$, $P(a)$ has more than one distinct proof; but if $P$ is a mere proposition, this cannot happen.

Suppose $P : A \rightarrow \mathscr{U}$ is a type famiy such that $P(x)$ is a mere proposition for all $x : A$. If $u, v : \Sigma_{x : A} P(x)$ are such that $\texttt{pr}_1(u) = \texttt{pr}_1(v)$, then $u = v$.

```
(** ** Subtypes (sigma types whose second components are hprops) *)
(** To prove equality in a subtype, we only need equality of the first component. *)
Definition path_sigma_hprop {A : Type} {P : A -> Type}
`{forall x, IsHProp (P x)}
(u v : sigT P)
: u.1 = v.1 -> u = v
:= path_sigma_uncurried P u v o pr1^-1.
```

For instance, recall that we defined

$$ A \simeq B :\equiv \Sigma_{f : A \rightarrow B} \texttt{isequiv}(f) $$

where each type $\texttt{isequiv}(f)$ was supposed to be a mere proposition. It follows that if two equivalences have equal underlying functions, then they are equal as equivalences. In $\Sigma_{x : A} P(x)$, $P$ can be thought of as a `subtype` of $A$. We may write $a \in \{x : A \mid P(x)\}$ to refer to the mere proposition $P(a)$. If it holds, we say that $a$ is a `member` of $P$. Similarly, $P \subseteq Q$ can be written as $\Pi_{x : A} (P(x) \rightarrow Q(x))$.

As further examples of subtypes, we may define the "subuniverses" of sets and propositions in $\mathscr{U}$:

$$ \texttt{Set}_\mathscr{U} :\equiv \{A : \mathscr{U} \mid \texttt{isSet}(A)\} \\ \texttt{Prop}_\mathscr{U} :\equiv \{A : \mathscr{U} \mid \texttt{isProp}(A)\} $$

Recall that for any two universes $\mathscr{U}_i$ and $\mathscr{U}_{i + 1}$, if $A : \mathscr{U}_i$, then $A : \mathscr{U}_{i + 1}$. For sets and mere propositions, we therefore have maps:

$$ \texttt{Set}_{\mathscr{U}_i} \rightarrow \texttt{Set}_{\mathscr{U}_{i + 1}} \\ \texttt{Prop}_{\mathscr{U}_i} \rightarrow \texttt{Prop}_{\mathscr{U}_{i + 1}} $$

However, the former cannot be an equivalence, as making it so would remind us of paradoxes in Cantorian set theory. However, the latter could be an equivalence, and we consier adding the `propositional resizing axiom`:

The map $\texttt{Prop}_{\mathscr{U}_i} \rightarrow \texttt{Prop}_{\mathscr{U}_{i + 1}}$ is an equivalence.

It essentially says that any mere proposition in universe $\mathscr{U}_{i + 1}$ can be resized to an equivalent one in $\mathscr{U}_i$. It follows automatically if $\mathscr{U}_{i + 1}$ satisfies LEM. This is a form of `impredicativity` for mere propositions, and by avoiding its use, our type theory will remain predicative.

In practice, however, what we want is a slightly different statement, that a universe $\mathscr{U}$ under consideration contains a type which "classifies all mere propositions". In other words, we want a type $\Omega : \mathscr{U}$ together with an $\Omega$-indexed family of mere propositions, which contains every mere proposition, upto equivalence. This follows from the propositional resizing axiom, if $\mathscr{U}$ is not the smallest univese $\mathscr{U}_0$, then we can define $\Omega :\equiv \texttt{Prop}_{\mathscr{U}_0}$.

In the absence of propositional resizing, the definition of `power set` depends on the choice of $\mathscr{U}$. In its presence, however, one can define the power set to be:

$$ \mathscr{P}(A) :\equiv (A \rightarrow \Omega)_i $$

which is then independent of $\mathscr{U}$.

## The logic of mere propositions

In many cases, logical connectives and quantifiers can be represented in this logic by simply restricting the type-former to mere propositions; this, of course, requires us to know whether the type former in question preserve mere propositions.

If $A$ and $B$ are mere propositions, so is $A \times B$.

If $B : A \rightarrow \mathscr{U}$ is such that for all $x : A$, B(x) is a mere proposition, then $\Pi_{x : A} B(x)$ is a mere proposition.

```
Definition PiType_isMereProp `{Funext} (A : Type) (B : A -> Type)
:= trunc_forall _ A B (-1).
```

In particular, If $B$ is a mere proposition, then so is $A \rightarrow B$ regardless of what $A$ is. Since $\mathbb{0}$ is a mere proposition, so is $\neg A \equiv A \rightarrow \mathbb{0}$. Thus the connectives "implies", "not", and "forall" preserve mere propositions.

On the other hand, even if $A$ and $B$ are mere propositions, $A + B$ will not, in general, be one. For instance, $\mathbb{1}$ is a mere proposition, but $\mathbb{2} = \mathbb{1} + \mathbb{1}$ is not. Logically speaking, $A + B$ is a "purely constructive" sort of "or": a witness of it contains which disjunct is true. However, if we need a more classical sort of "or" that preserves mere propositions, we need a way to "truncate" this type into a mere proposition by forgetting the additional information. The same issue arises with $\Sigma_{x : A} P(x)$.

## Propositional truncation

The `propositional truncation`, also called `$(-1)$-truncation`, `bracket type`, or `squash type`, is an additional type former wich "truncates" a type down to a mere proposition, forgetting all information contained in inhabitants of that type other than their existence.

More precisely, given type $A$, there is a type $||A||$ with two constructors:

- For any $a : A$, we have $|a| : ||A||$.
- For any $x, y : ||A||$, we have $x = y$.

The first constructor means that if $A$ is inhabitated, so is $||A||$. The second ensures that $||A||$ is a mere proposition; usually we leave the witness of this fact nameless.

The recursion principle of $||A||$ says that: if $B$ is a mere proposition, and we have $f : A \rightarrow B$, then there is an induced $g : ||A|| \rightarrow B$ such that $g(|a|) = f(a)$ for all $a : A$.

In other words, any mere proposition that follows from $A$ already follows from $||A||$. Thus, $||A||$, as a mere proposition, contains no more information than the inhabitatedness of $A$.

With propositional truncation, we can extend the "logic of mere propositions" to cover disjunction and existential quantification. Specifically, $||A + B|||$ is a mere propositional version of "A or B", which does not remember which disjunct is true.

The recursion principle of truncation implies that we can still do a case analysis on $||A + B||$ when attempting to prove a mere proposition. That is, suppose we have an assumption $u : ||A + B||$, and we are trying to prove a mere proposition $Q$. In other words, we are trying to define an element $||A + B|| \rightarrow Q$. Since $Q$ is a mere proposition, by recursion principle for propositional truncation, it suffices to construct a function $A + B \rightarrow Q$. But now we can do case analysis on $A + B$.

Similarly, or a type family $P : A \rightarrow \mathscr{U}$, we can consider $||\Sigma_{x : A} P(x)||$ to be the mere propositional version of "there exists an $x : A$ such that $P(x)$". If we have an assumption of type $||\Sigma_{x : A} P(x)||$, we may introduce new assumptions $x : A$ and $y: P(x)$ when attempting to prove a mere proposition. In other words, if we know that there exists some $x : A$ such that $P(x)$, but we don't have a particular such $x$ at hand, then we are free to make use of such an $x$ as long as we aren't trying to construct anything which might depend on the particular value of $x$.

## The axiom of choice

assume type $X$ and type families

$$ A : X \rightarrow \mathscr{U} \\ P : \Pi_{x : X} A(x) \rightarrow \mathscr{U} $$

and moreover that:

- $X$ is a set.
- $A(x)$ is a set for all $x : X$.
- $P(x, a)$ is a mere proposition for all $x : X$ and $a : A(x)$.

The `axiom of choice` asserts that under these assumptions,

$$ \Pi_{x :A} (||\Sigma_{x : A(x)} P(x, a)||) \rightarrow ||\Sigma_{g : \Pi_{x : A} A(x)}\Pi_{x : A} P(x, g(x))|| $$

Note, in particular, that propositional truncation appears twice. The truncation in the domain means we assume that for every $x$, there exists some $a : A(x)$ such that $P(x, a)$, but that these values are not chosen or specified in any known way. The truncation in the codomain means we conclude that there exists some function $g$, but this function is not determined or specified in any known way.

AC is equivalent to the statement that for any set $X$ and map $Y : X \rightarrow \mathscr{U}$ such that each $Y(x)$ is a set, we have

$$ \Pi_{x : X}(||Y(x)||) \rightarrow ||\Pi_{x : X} Y(x)|| $$

this corresponds to a well-known equivalent form of the classical AC, namely "the cartesian product of a family of nonempty sets is nonempty".

These two statements of AC are not a consequence of out basic type theory, but they may be consistently assumed as axioms. Note that the latter can be shown equivalent to asking for an equivalence:

$$ \Pi_{x : X}(||Y(x)||) \simeq ||\Pi_{x : X} Y(x)|| $$

This illustrates a common pitfall: although dependent function types preserve mere propositions, they do not commute with truncation. AC says that the equivalence holds for sets, but fails in general.

## The principle of unique choice

If $P$ is a mere proposition, then $P \simeq ||P||$.

```
Definition isequiv_to_O_inO (T : Type) `{In O T} : IsEquiv (to O T).
Definition p_simeq_trun_p := isequiv_to_O_inO (Tr (-1)).
```

It has the following important consequence:

`Principle of unique choice`. Suppose $P : A \rightarrow \mathscr{U}$ such that:

- For each $s$, the type $P(x)$ is a mere proposition.
- For each $x$ we have $||P(x)||$.

Then we have $\Pi_{x : A} P(x)$.

```
Lemma unique_choice {X Y} (R:X->Y->Type) :
(forall x y, IsHProp (R x y)) -> (forall x, (hunique (R x)))
-> {f : X -> Y & forall x, (R x (f x))}.
```

## When are mere propositions truncated?

In a nutshell, we shall use untruncated logic as the default convention, and qualify the truncated versions by "mere", for the following reason: mere propositions aren't a fundamental part of type theory; they are only the second rung on the $\infty$-ladder of types, and there are many other modalities not lying on this ladder at all.

## Contractability

A mere proposition which is inhabited must be equivalent to $\mathbb{1}$, and the converse also holds. A type with this property is called `contractible`.

Type `A` is contractible or a `singleton`, if there is an $a : A$, called the `center of contraction`, such tht $a = x$ for all $x : A$. We denote the specified path $a = x$ by $\texttt{contr}_x$. In other words,

$$ \texttt{isContr}(A) :\equiv \Sigma_{a : A} \Pi_{x : A} (a = x) $$

We can pronounce this as "$A$ contains an element, and every other element of $A$ is equal to that element". To the classical ear, this could sound as a definition of `connectedness`, rather than contractability.

For type $A$, the following are logically equivalent:

- $A$ is contractible.
- $A$ is a mere proposition, and there is a point $a : A$.
- $A$ is equivalent to $\mathbb{1}$.

```
(* The Unit type is contractible *)
(** Because [Contr] is a notation, and [Contr_internal] is the record, we need to iota expand to fool Coq's typeclass machinery into accepting supposedly "mismatched" contexts. *)
Global Instance contr_unit : Contr Unit | 0 := let x := {|
center := tt;
contr := fun t : Unit => match t with tt => 1 end
|} in x.
```

For any type $A$, the type $\texttt{isContr}(A)$ is a mere proposition.

```
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A) | 0.
```

If $A$ is contractible, so is $\texttt{isContr}(A)$.

```
Global Instance contr_contr `{Funext} (A : Type) `{Contr A}
: Contr (Contr A) | 100.
```

If $P : A \rightarrow \mathscr{U}$ is a type family such that $P(a)$ is contractible, then $\Pi_{x : A} P(x)$ is contractible.

```
Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a) | 100.
```

If $B$ is a retract of $A$, and $A$ is contractible, then so is $B$.

For any $A$ and any $a : A$, the type $\Sigma_{x : A} (x = a)$ is contractible.

`Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y} | 100.`

Let $P : A \rightarrow \mathscr{U}$ be a type family.

- If each $P(x)$ is contractible, then $\Sigma_{x : A} P(x)$ is equivalent to $A$.
- If $A$ is contractible with center $a$, then $\Sigma_{x : A} P(x)$ is equivalent to $P(a)$.

```
Definition equiv_sigma_contr {A : Type} (P : A -> Type)
`{forall a, Contr (P a)}
: sigT P <~> A
:= Build_Equiv _ _ pr1 _.
```

```
Definition equiv_contr_sigma {A : Type} (P : A -> Type) `{Contr A}
: { x : A & P x } <~> P (center A).
```

Type $A$ is a mere proposition if and only if for all $x, y : A$, the type $x =_A y$ is contractible.

```
(** Any two points in an hprop are connected by a path. *)
Theorem path_ishprop `{H : IsHProp A}
: forall x y : A, x = y.
Proof.
apply H.
Defined.
```

```
Theorem hprop_allpath (A : Type)
: (forall (x y : A), x = y) -> IsHProp A.
intros H x y.
pose (C := Build_Contr A x (H x)).
apply contr_paths_contr.
Defined.
```