From 914addc66c5c7546e3be6937b8d08053e54fbb7e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 8 Jan 2017 22:47:48 +0100 Subject: [PATCH] feat(homotopy): introduce notation for topological type constructors Also change the alternative induction/recursion principle for the smash product --- hott/homotopy/cofiber.hlean | 2 ++ hott/homotopy/join.hlean | 2 ++ hott/homotopy/red_susp.hlean | 49 ++++++++++++++++++++++++++ hott/homotopy/smash.hlean | 66 +++++++++++++++--------------------- hott/homotopy/susp.hlean | 2 ++ hott/homotopy/wedge.hlean | 1 + src/emacs/lean-input.el | 1 + 7 files changed, 84 insertions(+), 39 deletions(-) diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean index 948f3e82f..5c7891518 100644 --- a/hott/homotopy/cofiber.hlean +++ b/hott/homotopy/cofiber.hlean @@ -74,6 +74,8 @@ attribute cofiber.rec_on cofiber.elim_on [unfold 5] definition pcofiber [constructor] {A B : Type*} (f : A →* B) : Type* := pointed.MK (cofiber f) !cofiber.base +notation `ℂ` := pcofiber + namespace cofiber variables (A : Type*) diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index dce4ed436..79d042cdb 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -74,6 +74,8 @@ attribute join.rec [recursor] attribute join.elim [recursor 7] attribute join.rec join.elim [unfold 7] +notation ` ★ `:40 := pjoin + /- Diamonds in joins -/ namespace join variables {A B : Type} diff --git a/hott/homotopy/red_susp.hlean b/hott/homotopy/red_susp.hlean index bd692eb00..cf0d5030b 100644 --- a/hott/homotopy/red_susp.hlean +++ b/hott/homotopy/red_susp.hlean @@ -138,4 +138,53 @@ namespace red_susp refine transpose !ap_con_right_inv_sq ⬝h _, apply red_susp_helper_lemma } end end } end +print change_path_cono + + -- definition north {A : Type*} : red_susp A := base + -- definition south {A : Type*} : red_susp A := base + -- definition merid {A : Type*} (a : A) : north = south :> red_susp A := equator a + +print inverse2 + -- protected definition susp_rec {A : Type*} {P : red_susp A → Type} (PN : P north) (PS : P south) + -- (Pm : Πa, PN =[merid a] PS) (x : red_susp A) : P x := + -- begin + -- induction x, + -- { exact PN }, + -- { refine change_path _ (Pm a ⬝o (Pm pt)⁻¹ᵒ), refine whisker_left _ equator_pt⁻² }, + -- { } + -- end + + + definition whisker_left_inverse2 {A : Type} {a : A} {p : a = a} (q : p = idp) : whisker_left p q⁻² ⬝ q = con.right_inv p := + by cases q; reflexivity + + protected definition susp_rec {A : Type*} {P : red_susp A → Type} (P0 : P base) + (P1 : Πa, P0 =[equator a] P0) (x : red_susp' A) : P x := + begin + induction x, + { exact P0 }, + { refine change_path _ (P1 a ⬝o (P1 pt)⁻¹ᵒ), exact whisker_left (equator a) equator_pt⁻² }, + { refine !change_path_con⁻¹ ⬝ _, refine ap (λx, change_path x _) _ ⬝ cono_invo_eq_idpo idp, + exact whisker_left_inverse2 equator_pt } + end + + definition red_susp_equiv_susp' [constructor] (A : Type*) : red_susp A ≃ susp A := + begin + fapply equiv.MK, + { exact susp_of_red_susp }, + { exact red_susp_of_susp }, + { exact abstract begin intro x, induction x, + { reflexivity }, + { exact merid pt }, + { apply eq_pathover_id_right, + refine ap_compose susp_of_red_susp _ _ ⬝ ap02 _ !elim_merid ⬝ !elim_equator ⬝ph _, + apply whisker_bl, exact hrfl } end end }, + { intro x, induction x using red_susp.susp_rec, + { reflexivity }, + { apply eq_pathover, apply hdeg_square, + refine ap_compose red_susp_of_susp _ _ ⬝ (ap02 _ !elim_equator ⬝ _) ⬝ !ap_id⁻¹, + exact !ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_merid ◾ (!elim_merid ⬝ equator_pt)⁻² }} + end + + end red_susp diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean index 0ea929ef6..c9b3206ca 100644 --- a/hott/homotopy/smash.hlean +++ b/hott/homotopy/smash.hlean @@ -28,13 +28,16 @@ namespace smash by induction u; exact ff; exact tt definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B) - protected definition mk (a : A) (b : B) : smash' A B := inl (a, b) + protected definition mk' (a : A) (b : B) : smash' A B := inl (a, b) definition pointed_smash' [instance] [constructor] (A B : Type*) : pointed (smash' A B) := - pointed.mk (smash.mk pt pt) + pointed.mk (smash.mk' pt pt) definition smash [constructor] (A B : Type*) : Type* := pointed.mk' (smash' A B) + infixr ` ∧ ` := smash + + protected definition mk (a : A) (b : B) : A ∧ B := inl (a, b) definition auxl : smash A B := inr ff definition auxr : smash A B := inr tt definition gluel (a : A) : smash.mk a pt = auxl :> smash A B := glue (inl a) @@ -56,10 +59,10 @@ namespace smash proof whisker_left _ !con.right_inv qed definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, smash.mk a (Point B)) p = gluel' a a' := - by induction p; exact !con.right_inv⁻¹ + !ap_is_constant definition ap_mk_right {b b' : B} (p : b = b') : ap (smash.mk (Point A)) p = gluer' b b' := - by induction p; exact !con.right_inv⁻¹ + !ap_is_constant protected definition rec {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) (Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl) @@ -73,23 +76,6 @@ namespace smash { apply Pgr }} end - -- a rec which is easier to prove, but with worse computational properties - protected definition rec' {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) - (Pg : Πa b, Pmk a pt =[glue a b] Pmk pt b) (x : smash' A B) : P x := - begin - induction x using smash.rec, - { apply Pmk }, - { exact gluel pt ▸ Pmk pt pt }, - { exact gluer pt ▸ Pmk pt pt }, - { refine change_path _ (Pg a pt ⬝o !pathover_tr), - refine whisker_right _ !glue_pt_right ⬝ _, esimp, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv }, - { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr), - refine whisker_right _ !glue_pt_left⁻² ⬝ _, - refine whisker_right _ !inv_con_inv_right ⬝ _, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv } - end - theorem rec_gluel {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) : @@ -113,10 +99,11 @@ namespace smash (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (x : smash' A B) : P := smash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x - -- an elim which is easier to prove, but with worse computational properties - protected definition elim' {P : Type} (Pmk : Πa b, P) (Pg : Πa b, Pmk a pt = Pmk pt b) - (x : smash' A B) : P := - smash.rec' Pmk (λa b, pathover_of_eq _ (Pg a b)) x + -- an elim where you are forced to make (Pgl pt) and (Pgl pt) to be reflexivity + protected definition elim' [reducible] {P : Type} (Pmk : Πa b, P) + (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B, Pmk pt b = Pmk pt pt) + (ql : Pgl pt = idp) (qr : Pgr pt = idp) (x : smash' A B) : P := + smash.elim Pmk (Pmk pt pt) (Pmk pt pt) Pgl Pgr x theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P} (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) : @@ -141,9 +128,8 @@ namespace smash end smash open smash -attribute smash.mk auxl auxr [constructor] -attribute smash.rec smash.elim [unfold 9] [recursor 9] -attribute smash.rec' smash.elim' [unfold 6] +attribute smash.mk smash.mk' auxl auxr [constructor] +attribute smash.elim' smash.rec smash.elim [unfold 9] [recursor 9] namespace smash @@ -166,17 +152,19 @@ namespace smash { exact of_smash_pbool }, { intro a, exact smash.mk a tt }, { intro a, reflexivity }, - { exact abstract begin intro x, induction x using smash.rec', - { induction b, exact (glue a tt)⁻¹, reflexivity }, - { apply eq_pathover_id_right, induction b: esimp, - { refine ap02 _ !glue_pt_right ⬝ph _, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ph _, - refine ap02 _ (!ap_con ⬝ (!elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²))) ⬝ph _, - apply hinverse, apply square_of_eq, - esimp, refine (!glue_pt_right ◾ !glue_pt_left)⁻¹ }, - { apply square_of_eq, refine !con.left_inv ⬝ _, esimp, symmetry, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ _, - exact ap02 _ !elim_glue }} end end }}, + { exact abstract begin intro x, induction x, + { induction b, exact gluer' tt pt ⬝ gluel' pt a, reflexivity }, + { exact gluer' tt ff ⬝ gluel pt, }, + { exact gluer tt, }, + { apply eq_pathover_id_right, + refine ap_compose (λa, smash.mk a tt) _ _ ⬝ ap02 _ !elim_gluel ⬝ph _, + apply square_of_eq_top, refine !con.assoc⁻¹ ⬝ whisker_right _ !idp_con⁻¹ }, + { apply eq_pathover_id_right, + refine ap_compose (λa, smash.mk a tt) _ _ ⬝ ap02 _ !elim_gluer ⬝ph _, + induction b: esimp, + { apply square_of_eq_top, + refine whisker_left _ !con.right_inv ⬝ !con_idp ⬝ whisker_right _ !idp_con⁻¹ }, + { apply square_of_eq idp }} end end }}, { reflexivity } end diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index a5d0dc691..e27b47394 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -202,6 +202,8 @@ open susp definition psusp [constructor] (X : Type) : Type* := pointed.mk' (susp X) +notation `⅀` := psusp + namespace susp open pointed is_trunc variables {X Y Z : Type*} diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 633f8f3c6..6f4891f9e 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -12,6 +12,7 @@ open eq pushout pointed unit trunc_index definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) local attribute wedge [reducible] definition pwedge (A B : Type*) : Type* := pointed.mk' (wedge A B) +infixr ` ∨ ` := pwedge namespace wedge diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index d602aced3..efc3ddfbc 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -289,6 +289,7 @@ order for the change to take effect." ("intersection" . ,(lean-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉")) ("union" . ,(lean-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀")) + ("join". ("★")) ("smash". ("∧")) ("wedge" . ("∨")) ("cofiber" . ("ℂ")) ("susp" . ("⅀")) ("and" . ("∧")) ("or" . ("∨")) ("And" . ("⋀")) ("Or" . ("⋁")) ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍"))