feat(algebra/e_closure): add some support for dependent elimination of two_quotients

hott/algebra/e_closure.hlean

@@ -10,11 +10,11 @@ A more appropriate intuition is the type of words formed from the relation,
 
 import .relation eq2 arity
 
-open eq
+open eq equiv
 
 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
+| of_path : Π{a a'} (pp : a = 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''
 
@@ -22,7 +22,7 @@ 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
+  abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
 end e_closure
 
 namespace relation
@@ -37,11 +37,11 @@ section
   protected definition e_closure.elim [unfold 8] {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,
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       exact e r,
-      reflexivity,
-      exact v_0⁻¹,
-      exact v_0 ⬝ v_1
+      exact ap f pp,
+      exact IH⁻¹,
+      exact IH₁ ⬝ IH₂
   end
 
   definition ap_e_closure_elim_h [unfold 12] {B C : Type} {f : A → B} {g : B → C}
@@ -50,15 +50,15 @@ section
     (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,
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       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)
+      induction pp, reflexivity,
+      exact ap_inv g (e_closure.elim e r) ⬝ inverse2 IH,
+      exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂)
   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')
+  definition ap_e_closure_elim [unfold 10] {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
 
@@ -84,18 +84,18 @@ section
              (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,
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
     { esimp,
       apply square_of_eq, exact !con.right_inv ⬝ !con.left_inv⁻¹},
-    { apply ids},
+    { induction pp, apply ids},
     { rewrite [▸*,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},
+      exact !ap_inv2 ⬝v square_inv2 IH},
     { rewrite [▸*,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},
+      refine !ap_con2 ⬝v square_con2 IH₁ IH₂},
   end
 
   theorem ap_ap_e_closure_elim {B C D : Type} {f : A → B}
@@ -134,34 +134,55 @@ section
   --dependent elimination:
 
   variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)}
-  protected definition e_closure.elimo [unfold 6]
+  protected definition e_closure.elimo [unfold 11]
     (p : Π⦃a a' : A⦄, R a a' → f a = f a')
     (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
     (t : T a a') : f' a =[e_closure.elim p t] f' a' :=
   begin
-    induction t,
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       exact po r,
-      constructor,
-      exact v_0⁻¹ᵒ,
-      exact v_0 ⬝o v_1
+      induction pp, constructor,
+      exact IH⁻¹ᵒ,
+      exact IH₁ ⬝o IH₂
   end
 
   definition ap_e_closure_elimo_h [unfold 12]  {g' : Πb, Q (g b)}
     (p : Π⦃a a' : A⦄, R a a' → f a = f a')
-    --(po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
     (po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a'))
     (q : Π⦃a a' : A⦄ (s : R a a'), apdo g' (p s) = po s)
     (t : T a a') : apdo g' (e_closure.elim p t) = e_closure.elimo p po t :=
   begin
-    induction t,
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       apply q,
-      reflexivity,
+      induction pp, reflexivity,
       esimp [e_closure.elim],
-      exact apdo_inv g' (e_closure.elim p r) ⬝ v_0⁻²ᵒ,
-      exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (v_0 ◾o v_1)
+      exact apdo_inv g' (e_closure.elim p r) ⬝ IH⁻²ᵒ,
+      exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂)
   end
 
+/-
+  definition e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))}
+    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a')
+    (t : T a a') : e_closure.elimo (λa a' r, ap g (p r)) po t =
+    change_path (ap_e_closure_elim g p t)
+      (pathover_ap Q g (e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t)) :=
+  begin
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
+    { esimp, exact (to_right_inv !pathover_compose (po r))⁻¹},
+    { induction pp, reflexivity},
+    { exact sorry},
+    { exact sorry},
+  end
 
+  definition e_closure_elimo_ap' {g' : Π(a : A), Q (g (f a))}
+    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a')
+    (t : T a a') :
+      pathover_of_pathover_ap Q g (change_path (ap_e_closure_elim g p t)⁻¹ (e_closure.elimo (λa a' r, ap g (p r)) po t)) =
+      e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t :=
+  sorry
+-/
 
 end
 end relation