aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jasongross9@gmail.com>2016-08-01 13:22:21 -0700
committerGitHub <noreply@github.com>2016-08-01 13:22:21 -0700
commit212b073990426dccd8799294c583e2e58a015463 (patch)
tree546ae1c8fc26f3f73f71e94bc49072caf598191a /src/Util/Equality.v
parentb92653291b6ac977d2bf1b72420d686580adf2f4 (diff)
Add documentation: Equality, HProp, Isomorphism, Sigma (#41)
* Add doc: Equality, HProp, Isomorphism, Sigma * Update documentation with suggestions from Andres
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v38
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}.