Here, we talk about equalities, and provide illustrative examples in vanilla Coq, SProp, and HoTT.
Equality in Mathematics
In zfcbased 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
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 proofirrelevant 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. (* Typecheck 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. (* Typecheck 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 (
)truncated Type. 
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
Theorem hPropEquality (P : hProp) (a b : P) : a = b.
Proof.
by apply path_ishprop.
Qed.
Conceptually, this is as simple and elegant as PropEquality.