From 212b073990426dccd8799294c583e2e58a015463 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 1 Aug 2016 13:22:21 -0700 Subject: Add documentation: Equality, HProp, Isomorphism, Sigma (#41) * Add doc: Equality, HProp, Isomorphism, Sigma * Update documentation with suggestions from Andres --- src/Util/Equality.v | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) (limited to 'src/Util/Equality.v') 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}. -- cgit v1.2.3