Here, we talk about equalities, and provide illustrative examples in vanilla Coq, SProp, and HoTT.

## Equality in Mathematics

In zfc-based mathematics, say in abelian groups, $A \oplus B \simeq B \oplus A$, where the equality is a set-based equality. In mathematics based on category theory, equality is too strong a notion on objects, and only speak about objects "upto unique isomorphism"; morphisms in a $\mathrm{1}$-category can be equal though. In higher categories, and in particular, homotopy theory, we talk about "weak homotopy equivalences" almost fully replacing equality. However, it can be tricky to mechanize a theory based on $\infty$-categories; the best dependent-type-theory model we have is homotopy type theory, commonly referred to as HoTT, which we will discuss in the last section.

## Universes in Coq

First, let us briefly talk about the cumulative universe of Coq. Prop is a Set that can be promoted to Type seamlessly. The reason for the distinction between Prop and Set is an engineering one: Prop is impredicative, while Set is not, and proofs are erased during extraction.

```
Definition SetTypeIncl (A : Set) : Type := A.
Definition PropTypeIncl (A : Prop) : Type := A.
Definition PropSetIncl (A : Prop) : Set := A.
```

There is an $\infty$ hierarchy within the Type universe, and types of Types are Types themselves.

Inhabitants of a Set are sets of primitive things like $\mathbb{N}$ and $\mathbb{R}$, while inhabitants of a Prop are propositions, which could be $\top$, $\bot$, or some arbitrary term, the inhabitant of which acts as the proof.

## Propositions

There are two kinds of equalities in vanilla Coq. The difference is as follows: propositional equality roughly translates to "requires proof obligation to be discharged by the user", whereas definitional equality is a simple syntactic rewriting in the metatheory. A propositional equality between propositions can be formalized as:

`Axiom PropositionalProofIrrelevance : ∀ (P : Prop) (a b : P), a = b.`

We then get a proof obligation which we discharge using the axiom:

```
Theorem PropEquality (P : Prop) (a b : P) : a = b.
Proof.
by apply PropositionalProofIrrelevance.
Qed.
```

In the general case, two different inhabitants of Prop are unequal. There is, however, a propositional equality existing between two equal propositions:

```
Theorem PropRefl (P : Prop) (x : P): x = x.
Proof.
exact eq_refl.
Qed.
```

where eq_refl is simply the sole inhabitant of an Inductive:

```
Inductive eq (A : Type) (x : A) : A -> Prop :=
eq_refl : eq A x x.
```

## The proof-irrelevant SProp

There are three inhabitants of SProp: sUnit corresponding to $\top$, sEmpty corresponding to $\bot$, and sProposition corresponding to a definitionally proof-irrelevant term. The way SProp implements definitional proof-irrelevance is a simple engineering detail: there is hard-coding in Coq to render two inhabitants of sProposition trivially inter-convertible.

Unfortunately, = doesn't work as expected:

```
Theorem SPropIrr (P : SProp) (x y : P) : x = y.
Proof.
by reflexivity.
Abort. (* Type-check fails at Qed.
* (=) : ∀ A, A -> A -> Prop, but we want to return an SProp. *)
```

This is because the SProp universe is disjoint from the Prop universe:

```
Theorem SPropToProp : SProp -> Prop.
Proof.
by intros x; exact x.
Abort. (* Type-check fails at Qed.
* SProp is not convertible to Prop. *)
```

Fortunately, we can do better.

## Mere propositions in homotopy type theory

In HoTT, there is just one $\infty$-ladder:

- $\mathbb{1}$, and anything that's contractible to it, is the ($\mathrm{-2}$)-truncated Type.
- A "mere proposition", an inhabitant of hProp, is simply a ($\mathrm{-1}$)-truncated Type.
- hSet is the $\mathrm{0}$-truncated Type.

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

The notion of truncation is central to HoTT, where $A : \mathrm{Type}_n$ can be truncated to a $\mathrm{Type}_m$, whence higher-than-$m$ morphisms are rendered uninteresting. Any two hProps are propositionally equal:

```
Theorem hPropEquality (P : hProp) (a b : P) : a = b.
Proof.
by apply path_ishprop.
Qed.
```

Conceptually, this is as simple and elegant as PropEquality.