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

## Equality in Mathematics

In [zfc-based mathematics](/zfc), 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](https://coq.inria.fr/refman/addendum/sprop.html): `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](https://github.com/HoTT/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`.