Equality in Mechanized Mathematics


Paris
vn

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:

  1. $\mathbb{1}$, and anything that's contractible to it, is the ($\mathrm{-2}$)-truncated Type.
  2. A "mere proposition", an inhabitant of `hProp`, is simply a ($\mathrm{-1}$)-truncated Type.
  3. `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`.

† Big thanks to [Kenji Maillard](https://kenji.maillard.blue) for the scintillating discussion, and for helping with the examples.

‡ Kudos to Hugo Moeneclaey for giving a wonderful introduction to truncation in the last HoTT class.

§ Thanks to [Pierre-Marie Pédrot](https://www.pédrot.fr) for pointing out some very serious errors.