Equality in Mechanized Mathematics

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, , 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 -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 -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 hierarchy within the Type universe, and types of Types are Types themselves.

Inhabitants of a Set are sets of primitive things like and , while inhabitants of a Prop are propositions, which could be , , 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 , sEmpty corresponding to , 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 -ladder:

  1. 𝟙, and anything that's contractible to it, is the ()-truncated Type.
  2. A "mere proposition", an inhabitant of hProp, is simply a ()-truncated Type.
  3. hSet is the -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 can be truncated to a , whence higher-than- 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.