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,
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
Inhabitants of a Set are sets of primitive things like
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
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
, and anything that's contractible to it, is the ( 𝟙 )-truncated Type.
A "mere proposition", an inhabitant of hProp, is simply a (
hSet is the
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
Theorem hPropEquality (P : hProp) (a b : P) : a = b. Proof. by apply path_ishprop. Qed.
Conceptually, this is as simple and elegant as PropEquality.