feat(hott/relation): add equivalence closure of a relation

hott/algebra/e_closure.hlean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+The "equivalence closure" of a type-valued relation.
+Given a binary type-valued relation (fibration), we add reflexivity, symmetry and transitivity terms
+-/
+
+import .relation types.eq2 arity
+
+open eq
+
+inductive e_closure {A : Type} (R : A → A → Type) : A → A → Type :=
+| of_rel : Π{a a'} (r : R a a'), e_closure R a a'
+| refl : Πa, e_closure R a a
+| symm : Π{a a'} (r : e_closure R a a'), e_closure R a' a
+| trans : Π{a a' a''} (r : e_closure R a a') (r' : e_closure R a' a''), e_closure R a a''
+
+namespace e_closure
+  infix `⬝r`:75 := e_closure.trans
+  postfix `⁻¹ʳ`:(max+10) := e_closure.symm
+  notation `[`:max a `]`:0 := e_closure.of_rel a
+  abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := refl R a
+end e_closure
+
+namespace relation
+
+section
+  parameters {A : Type}
+             (R : A → A → Type)
+  local abbreviation T := e_closure R
+
+  variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
+  parameter {R}
+  protected definition e_closure.elim {B : Type} {f : A → B}
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
+  begin
+    induction t,
+      exact e r,
+      reflexivity,
+      exact v_0⁻¹,
+      exact v_0 ⬝ v_1
+  end
+
+  definition ap_e_closure_elim_h {B C : Type} {f : A → B} {g : B → C}
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
+    : ap g (e_closure.elim e t) = e_closure.elim e' t :=
+  begin
+    induction t,
+      apply p,
+      reflexivity,
+      exact ap_inv g (e_closure.elim e r) ⬝ inverse2 v_0,
+      exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (v_0 ◾ v_1)
+  end
+
+  definition ap_e_closure_elim {B C : Type} {f : A → B} (g : B → C)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
+    : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t :=
+  ap_e_closure_elim_h e (λa a' s, idp) t
+
+  definition ap_e_closure_elim_h_eq {B C : Type} {f : A → B} {g : B → C}
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
+    : ap_e_closure_elim_h e p t =
+      ap_e_closure_elim g e t ⬝ ap (λx, e_closure.elim x t) (eq_of_homotopy3 p) :=
+  begin
+    fapply homotopy3.rec_on p,
+    intro q, esimp at q, induction q,
+    esimp, rewrite eq_of_homotopy3_id
+  end
+
+  theorem ap_ap_e_closure_elim_h {B C D : Type} {f : A → B}
+    {g : B → C} (h : C → D)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
+    : square (ap (ap h) (ap_e_closure_elim_h e p t))
+             (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)
+             (ap_compose h g (e_closure.elim e t))⁻¹
+             (ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) :=
+  begin
+    induction t,
+    { unfold [ap_e_closure_elim_h,e_closure.elim],
+      apply square_of_eq, exact !con.right_inv ⬝ !con.left_inv⁻¹},
+    { apply ids},
+    { rewrite [↑e_closure.elim,↓e_closure.elim e r,
+               ↑ap_e_closure_elim_h,
+               ↓ap_e_closure_elim_h e p r,
+               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r,
+               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r,
+               ap_con (ap h)],
+      refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
+      rewrite [con_inv,inv_inv,-inv2_inv],
+      exact !ap_inv2 ⬝v square_inv2 v_0},
+    { rewrite [↑e_closure.elim,↓e_closure.elim e r, ↓e_closure.elim e r',
+               ↑ap_e_closure_elim_h,
+               ↓ap_e_closure_elim_h e p r,
+               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r,
+               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r,
+               ↓ap_e_closure_elim_h e p r',
+               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r',
+               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r',
+               ap_con (ap h)],
+      refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _,
+      rewrite [con_inv,inv_inv,con2_inv],
+      refine !ap_con2 ⬝v square_con2 v_0 v_1},
+  end
+
+  theorem ap_ap_e_closure_elim {B C D : Type} {f : A → B}
+    (g : B → C) (h : C → D)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
+    : square (ap (ap h) (ap_e_closure_elim g e t))
+             (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)
+             (ap_compose h g (e_closure.elim e t))⁻¹
+             (ap_e_closure_elim h (λa a' r, ap g (e r)) t) :=
+  !ap_ap_e_closure_elim_h
+
+  open e_closure
+  definition is_equivalence_e_closure : is_equivalence T :=
+  begin
+    constructor,
+      intro a, exact rfl,
+      intro a a' t, exact t⁻¹ʳ,
+      intro a a' a'' t t', exact t ⬝r t',
+  end
+
+end
+end relation

hott/algebra/relation.hlean

@@ -18,7 +18,6 @@ section
   definition transitive : Type := Π⦃x y z⦄, R x y → R y z → R x z
 end
 
-
 /- classes for equivalence relations -/
 
 structure is_reflexive [class] {T : Type} (R : T → T → Type) := (refl : reflexive R)

hott/types/eq2.hlean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn
 

hott/types/types.md

@@ -16,7 +16,8 @@ Types (not necessarily HoTT-related):
 HoTT types
 
 * [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
-* [eq](eq.hlean)
+* [eq](eq.hlean): show that functions related to the identity type are equivalences
+* [eq2](eq2.hlean): higher dimensional structure of equality
 * [pointed](pointed.hlean)
 * [fiber](fiber.hlean)
 * [equiv](equiv.hlean)

src/emacs/lean-input.el

@@ -336,14 +336,15 @@ order for the change to take effect."
   ("sy"        . ("⁻¹"))
   ("inv"       . ("⁻¹"))
   ("-1"        . ("⁻¹"))
-  ("-1p"       . ("⁻¹ᵖ"))
   ("-1e"       . ("⁻¹ᵉ"))
   ("-1f"       . ("⁻¹ᶠ"))
-  ("-1h"       . ("⁻¹ʰ"))
-  ("-1v"       . ("⁻¹ᵛ"))
-  ("-1m"       . ("⁻¹ᵐ"))
   ("-1g"       . ("⁻¹ᵍ"))
+  ("-1h"       . ("⁻¹ʰ"))
+  ("-1m"       . ("⁻¹ᵐ"))
   ("-1o"       . ("⁻¹ᵒ"))
+  ("-1r"       . ("⁻¹ʳ"))
+  ("-1p"       . ("⁻¹ᵖ"))
+  ("-1v"       . ("⁻¹ᵛ"))
   ("-2"        . ("⁻²"))
   ("-3"        . ("⁻³"))
   ("qed"       . ("∎"))