feat(hott): add recursor to refl_quotient

2015-11-22 03:08:31 -05:00 · 2015-11-22 03:08:31 -05:00 · fe8a858d79
commit fe8a858d79
parent ae92e8c94d
5 changed files with 45 additions and 57 deletions
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@ -22,6 +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
+  notation `<`:max p `>`:0 := e_closure.of_path _ p
  abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
 end e_closure
 open e_closure
@ -57,21 +58,6 @@ section
      exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂)
  end

-/-  definition ap_e_closure_elim_h_inv [unfold_full] {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_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² :=
-  by reflexivity
-
-  definition ap_e_closure_elim_h_con [unfold_full] {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') (t' : T a' a'')
-    : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
-        (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') :=
-  by reflexivity-/
-
  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 :=
@ -141,6 +127,7 @@ section
      intro a a' a'' t t', exact t ⬝r t',
  end

+/-
  definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
    (t : e_closure R a a') (p : a = a'')
    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t :=
@ -155,6 +142,7 @@ section
    (t : e_closure R a a) (p : a = a')
    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
  by induction p; esimp; exact !idp_con⁻¹
+-/

  /- dependent elimination -/

--- a/hott/hit/hit.md
+++ b/hott/hit/hit.md
@ -14,9 +14,13 @@ hits related to homotopy theory are defined in

 Files in this folder:

-* [quotient](quotient.hlean) (quotients, primitive)
-* [trunc](trunc.hlean) (truncation, primitive)
-* [colimit](colimit.hlean) (Colimits of arbitrary diagrams and sequential colimits, defined using quotients)
-* [pushout](pushout.hlean) (Pushouts, defined using quotients)
-* [coeq](coeq.hlean) (Co-equalizers, defined using quotients)
-* [set_quotient](set_quotient.hlean) (Set-quotients, defined using quotients and set-truncation)
+* [quotient](quotient.hlean): quotients, primitive
+* [trunc](trunc.hlean): truncation, primitive
+* [colimit](colimit.hlean): Colimits of arbitrary diagrams and sequential colimits, defined using quotients
+* [pushout](pushout.hlean): Pushouts, defined using quotients
+* [coeq](coeq.hlean): Co-equalizers, defined using quotients
+* [set_quotient](set_quotient.hlean): Set-quotients, defined using quotients and set-truncation
+
+The following hits have also 2-constructors. They are defined only using quotients.
+* [two_quotient](two_quotient.hlean): Quotients where you can also specify 2-paths. These are used for all hits which have 2-constructors, and they are almost fully general for such hits, as long as they are nonrecursive
+* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths
--- a/hott/hit/refl_quotient.hlean
+++ b/hott/hit/refl_quotient.hlean
@ -20,7 +20,7 @@ section
  open refl_quotient_Q
  local abbreviation Q := refl_quotient_Q

-  definition refl_quotient : Type := simple_two_quotient R Q -- TODO: define this in root namespace
+  definition refl_quotient : Type := simple_two_quotient R Q

  definition rclass_of (a : A) : refl_quotient := incl0 R Q a
  definition req_of_rel ⦃a a' : A⦄ (r : R a a') : rclass_of a = rclass_of a' :=
@ -29,32 +29,26 @@ section
  definition pρ (a : A) : req_of_rel (ρ a) = idp :=
  incl2 R Q (Qmk a)

-  -- protected definition rec {P : refl_quotient → Type}
-  --   (Pc : Π(a : A), P (rclass_of a))
-  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
-  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
-  --   (x : refl_quotient) : P x :=
-  -- sorry
+  protected definition rec {P : refl_quotient → Type} (Pc : Π(a : A), P (rclass_of a))
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+    (Pr : Π(a : A), change_path (pρ a) (Pp (ρ a)) = idpo) (x : refl_quotient) : P x :=
+  begin
+    induction x,
+      exact Pc a,
+      exact Pp s,
+      induction q, apply Pr
+  end

-  -- protected definition rec_on [reducible] {P : refl_quotient → Type}
-  --   (Pc : Π(a : A), P (rclass_of a))
-  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
-  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) : P y :=
-  -- rec Pinl Pinr Pglue y
+  protected definition rec_on [reducible] {P : refl_quotient → Type} (x : refl_quotient)
+    (Pc : Π(a : A), P (rclass_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+    (Pr : Π(a : A), change_path (pρ a) (Pp (ρ a)) = idpo) : P x :=
+  rec Pc Pp Pr x

-  -- definition rec_req_of_rel {P : Type} {P : refl_quotient → Type}
-  --   (Pc : Π(a : A), P (rclass_of a))
-  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
-  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
-  --   ⦃a a' : A⦄ (r : R a a') : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
-  -- !rec_incl1
-
-  -- theorem rec_pρ {P : Type} {P : refl_quotient → Type}
-  --   (Pc : Π(a : A), P (rclass_of a))
-  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
-  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) (a : A)
-  --    : square (ap02 (rec Pc Pp Pr) (pρ a)) (Pr a) (elim_req_of_rel Pr (ρ a)) idp :=
-  -- !rec_incl2
+  definition rec_req_of_rel {P : Type} {P : refl_quotient → Type} (Pc : Π(a : A), P (rclass_of a))
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+    (Pr : Π(a : A), change_path (pρ a) (Pp (ρ a)) = idpo) ⦃a a' : A⦄ (r : R a a')
+    : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
+  !rec_incl1

  protected definition elim {P : Type} (Pc : Π(a : A), P)
    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp)
@ -84,7 +78,7 @@ end
 end refl_quotient

 attribute refl_quotient.rclass_of [constructor]
-attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold 8] [recursor 8]
+attribute refl_quotient.rec refl_quotient.elim [unfold 8] [recursor 8]
 --attribute refl_quotient.elim_type [unfold 9]
-attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold 5]
+attribute refl_quotient.rec_on refl_quotient.elim_on [unfold 5]
 --attribute refl_quotient.elim_type_on [unfold 6]
--- a/hott/hit/set_quotient.hlean
+++ b/hott/hit/set_quotient.hlean
@ -34,7 +34,7 @@ section
    { intro x', apply Pt},
    { intro y, fapply (quotient.rec_on y),
      { exact Pc},
-      { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}}
+      { intros, exact pathover_of_pathover_ap P tr (Pp H)}}
  end

  protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient)
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@ -133,6 +133,7 @@ namespace simple_two_quotient
  local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible]
  local attribute i aux incl0 [constructor]

+  parameters {R Q}
  protected definition rec {P : D → Type} (P0 : Π(a : A), P (incl0 a))
    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
@ -358,6 +359,7 @@ namespace two_quotient
  definition incl2 (q : Q t t') : inclt t = inclt t' :=
  eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q))

+  parameters {R Q}
  protected definition rec {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
@ -389,14 +391,14 @@ namespace two_quotient
    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
    ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
-  rec_incl1 _ _ _ _ _ s
+  rec_incl1 _ _ _ s

  theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
    ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
-  rec_inclt _ _ _ _ _ t
+  rec_inclt _ _ _ t

  protected definition elim {P : Type} (P0 : A → P)
    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@ -437,15 +439,15 @@ namespace two_quotient
    : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
  begin
    rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp],
-    xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))],
-    xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2)
+    xrewrite [eq_top_of_square (elim_incl2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))],
+    xrewrite [{simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2)
           (t ⬝r t'⁻¹ʳ)}
-      idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+      idpath (ap_con (simple_two_quotient.elim P0 P1 (elim_1 A R Q P P0 P1 P2))
                     (inclt t) (inclt t')⁻¹ ⬝
-             (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t ◾
-             (ap_inv (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+             (simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2) t ◾
+             (ap_inv (simple_two_quotient.elim P0 P1 (elim_1 A R Q P P0 P1 P2))
                     (inclt t') ⬝
-             inverse2 (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t')))),▸*],
+             inverse2 (simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2) t')))),▸*],
    rewrite [-con.assoc _ _ (con_inv_eq_idp _),-con.assoc _ _ (_ ◾ _),con.assoc _ _ (ap_con _ _ _),
             con.left_inv,↑whisker_left,con2_con_con2,-con.assoc (ap_inv _ _)⁻¹,
             con.left_inv,+idp_con,eq_of_con_inv_eq_idp_con2],