Add documentation: Equality, HProp, Isomorphism, Sigma (#41)

* Add doc: Equality, HProp, Isomorphism, Sigma

* Update documentation with suggestions from Andres

1 files changed, 37 insertions, 1 deletions

diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 7657f96cb..3c3ddd9ff 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -1,7 +1,23 @@
-(** * Lemmas about [eq] *)
+(** * The Structure of the [eq] Type *)
+(** As described by the project of homotopy type theory, there is a
+    lot of structure inherent in the type of propositional equality,
+    [eq].  We build up enough lemmas about this structure to deal
+    nicely with proofs of equality that come up in practice in this
+    project. *)
 Require Import Crypto.Util.Isomorphism.
 Require Import Crypto.Util.HProp.
 
+(** Most of the structure of proofs of equalities fits into what
+    mathematicians call a weak ∞-groupoid.  (In fact, one way of
+    *defining* a weak ∞-groupoid is via what's called the J-rule,
+    which exactly matches the eliminator [eq_rect] for the equality
+    type [eq].)  The first level of this groupoid is given by the
+    identity [eq_refl], the binary operation [eq_trans], and the
+    inverse of [p : x = y] given by [eq_sym p : y = x].  The second
+    level, which we provide here, says that [id ∘ p = p = p ∘ id],
+    that [(p ∘ q)⁻¹ = q⁻¹ ∘ p⁻¹], that [(p⁻¹)⁻¹ = p], and that [p ∘
+    p⁻¹ = p⁻¹ ∘ p = id].  We prove these here, as well as a few lemmas
+    about functoriality of functions over equality. *)
 Definition concat_1p {A x y} (p : x = y :> A) : eq_trans eq_refl p = p.
 Proof. case p; reflexivity. Defined.
 Definition concat_p1 {A x y} (p : x = y :> A) : eq_trans p eq_refl = p.
@@ -26,6 +42,22 @@ Lemma inv_V {A x y} (p : x = y :> A)
 : eq_sym (eq_sym p) = p.
 Proof. case p; reflexivity. Defined.
 
+(** To classify the equalities of a type [A] at a point [a : A], we
+    must give a "code" that stands in for the type [a = x] for each
+    [x], and a way of "encoding" proofs of equality into the code that
+    we claim represents this type.  To prove that the code is good, it
+    turns out that it sufficies to prove that it is freely generated
+    by the encoding of [eq_refl], i.e., that [{ x : A & a = x }] and
+    [{ x : A & code x }] are equivalent, i.e., that [{ x : A & code x
+    }] is an hProp (has at most one element).  When this is the case,
+    we have fully classified the type of equalities in [A] at [a] up
+    to isomorphism.  This lets us replace proofs of equalities in [A]
+    with their codes, which are frequently easier to manipulate.  (For
+    example, the code for [x = y :> A * B] is [(fst x = fst y) * (snd
+    x = snd y)], whence we can destruct the pair.)
+
+    This method of proof, introduced in homotopy type theory, is
+    called encode-decode. *)
 Section gen.
   Context {A : Type} {x : A} (code : A -> Type)
           (encode : forall y, x = y -> code y)
@@ -61,6 +93,10 @@ Section gen.
   Defined.
 End gen.
 
+(** We use the encode-decode method to prove that if [forall x y : A,
+    x = y], then [forall (x y : A) (p q : x = y), p = q]. *)
+(* It's not clear whether this should be in this file, or in HProp.
+   But we require [IsHProp] above, so we leave it here for now. *)
 Section hprop.
   Context {A} `{IsHProp A}.