diff --git a/hott/book.md b/hott/book.md index e8131f411..19bd9f0f6 100644 --- a/hott/book.md +++ b/hott/book.md @@ -22,7 +22,7 @@ The rows indicate the chapters, the columns the sections. | Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | | | Ch 6 | . | + | + | + | + | ½ | ½ | + | ¾ | ¼ | ¾ | + | . | | | | Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | | -| Ch 8 | ¾ | ¾ | - | - | ¼ | ¼ | - | - | - | - | | | | | | +| Ch 8 | + | + | - | - | ¼ | ¼ | - | - | - | - | | | | | | | Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | - | | | | | | | | Ch 10 | - | - | - | - | - | | | | | | | | | | | | Ch 11 | - | - | - | - | - | - | | | | | | | | | | @@ -141,7 +141,7 @@ Chapter 8: Homotopy theory Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy.md) -- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only one of the proofs) +- 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only the encode-decode proof) - 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof) - 8.3 (πk≤n of an n-connected space and π_{k ℕ₋₁ := + definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ := idp end sphere_index @@ -85,15 +86,15 @@ open sphere_index namespace trunc_index definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ := sphere_index.rec_on n -2 (λ n k, k.+1) - postfix `.-1`:(max+1) := sub_one + postfix `..-1`:(max+1) := sub_one definition of_sphere_index [coercion] [reducible] (n : ℕ₋₁) : ℕ₋₂ := - n.-1.+1 + n..-1.+1 - definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n.-1.-1 := + definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 := nat.rec_on n idp (λn p, ap trunc_index.succ p) - definition succ_sub_one (n : ℕ₋₁) : n.+1.-1 = n :> ℕ₋₂ := + definition succ_sub_one (n : ℕ₋₁) : n.+1..-1 = n :> ℕ₋₂ := idp definition of_sphere_index_of_nat (n : ℕ) @@ -114,6 +115,8 @@ definition sphere : ℕ₋₁ → Type₀ namespace sphere + export [notation] [coercion] sphere_index + definition base {n : ℕ} : sphere n := north definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) := pointed.mk base diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 0832bbd18..fc33ce52c 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -7,7 +7,7 @@ The Wedge Sum of Two pType Types -/ import hit.pointed_pushout .connectedness -open eq pushout pointed unit is_trunc.trunc_index pType +open eq pushout pointed unit trunc_index definition pwedge (A B : Type*) : Type* := ppushout (pconst punit A) (pconst punit B) diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 3f7d83a5d..e24ee08d2 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -13,37 +13,40 @@ import .nat .logic .equiv .pathover open eq nat sigma unit sigma.ops --set_option class.force_new true -namespace is_trunc +/- Truncation levels -/ - /- Truncation levels -/ +inductive trunc_index : Type₀ := +| minus_two : trunc_index +| succ : trunc_index → trunc_index - inductive trunc_index : Type₀ := - | minus_two : trunc_index - | succ : trunc_index → trunc_index +open trunc_index - open trunc_index +/- + notation for trunc_index is -2, -1, 0, 1, ... + from 0 and up this comes from a coercion from num to trunc_index (via ℕ) +-/ + +notation `ℕ₋₂` := trunc_index -- input using \N-2 + +definition has_zero_trunc_index [instance] [priority 2000] : has_zero ℕ₋₂ := +has_zero.mk (succ (succ minus_two)) + +definition has_one_trunc_index [instance] [priority 2000] : has_one ℕ₋₂ := +has_one.mk (succ (succ (succ minus_two))) + +namespace trunc_index - /- - notation for trunc_index is -2, -1, 0, 1, ... - from 0 and up this comes from a coercion from num to trunc_index (via ℕ) - -/ notation `-1` := trunc_index.succ trunc_index.minus_two -- ISSUE: -1 gets printed as -2.+1? notation `-2` := trunc_index.minus_two postfix `.+1`:(max+1) := trunc_index.succ postfix `.+2`:(max+1) := λn, (n .+1 .+1) - notation `ℕ₋₂` := trunc_index -- input using \N-2 - definition has_zero_trunc_index [instance] [priority 2000] : has_zero ℕ₋₂ := - has_zero.mk (succ (succ minus_two)) - - definition has_one_trunc_index [instance] [priority 2000] : has_one ℕ₋₂ := - has_one.mk (succ (succ (succ minus_two))) - - namespace trunc_index --addition, where we add two to the result definition add_plus_two [reducible] (n m : ℕ₋₂) : ℕ₋₂ := trunc_index.rec_on m n (λ k l, l .+1) + infix ` +2+ `:65 := trunc_index.add_plus_two + -- addition of trunc_indices, where results smaller than -2 are changed to -2 protected definition add (n m : ℕ₋₂) : ℕ₋₂ := trunc_index.cases_on m @@ -58,15 +61,17 @@ namespace is_trunc | tr_refl : le a a | step : Π {b}, le a b → le a (b.+1) - end trunc_index +end trunc_index - definition has_le_trunc_index [instance] [priority 2000] : has_le ℕ₋₂ := - has_le.mk trunc_index.le +definition has_le_trunc_index [instance] [priority 2000] : has_le ℕ₋₂ := +has_le.mk trunc_index.le - attribute trunc_index.add [reducible] - infix ` +2+ `:65 := trunc_index.add_plus_two - definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ := - has_add.mk trunc_index.add +attribute trunc_index.add [reducible] + +definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ := +has_add.mk trunc_index.add + +namespace trunc_index definition sub_two [reducible] (n : ℕ) : ℕ₋₂ := nat.rec_on n -2 (λ n k, k.+1) @@ -77,10 +82,9 @@ namespace is_trunc postfix `.-2`:(max+1) := sub_two postfix `.-1`:(max+1) := λn, (n .-2 .+1) - definition trunc_index.of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₂ := + definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₂ := n.-2.+2 - namespace trunc_index definition succ_le_succ {n m : ℕ₋₂} (H : n ≤ m) : n.+1 ≤ m.+1 := by induction H with m H IH; apply le.tr_refl; exact le.step IH @@ -89,7 +93,11 @@ namespace is_trunc protected definition le_refl (n : ℕ₋₂) : n ≤ n := le.tr_refl n - end trunc_index +end trunc_index open trunc_index + +namespace is_trunc + + export [notation] [coercion] trunc_index /- truncated types -/ @@ -112,7 +120,7 @@ end is_trunc open is_trunc structure is_trunc [class] (n : ℕ₋₂) (A : Type) := (to_internal : is_trunc_internal n A) -open nat num is_trunc.trunc_index +open nat num trunc_index namespace is_trunc diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 784c4bd23..567f457bf 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -11,196 +11,196 @@ Properties of is_trunc and trunctype import .pointed2 ..function algebra.order types.nat.order open eq sigma sigma.ops pi function equiv trunctype - is_equiv prod is_trunc.trunc_index pointed nat is_trunc algebra + is_equiv prod pointed nat is_trunc algebra + +namespace trunc_index + + definition minus_one_le_succ (n : trunc_index) : -1 ≤ n.+1 := + succ_le_succ (minus_two_le n) + + definition zero_le_of_nat (n : ℕ) : 0 ≤ of_nat n := + succ_le_succ !minus_one_le_succ + + open decidable + protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₂), decidable (n = m) + | has_decidable_eq -2 -2 := inl rfl + | has_decidable_eq (n.+1) -2 := inr (by contradiction) + | has_decidable_eq -2 (m.+1) := inr (by contradiction) + | has_decidable_eq (n.+1) (m.+1) := + match has_decidable_eq n m with + | inl xeqy := inl (by rewrite xeqy) + | inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney) + end + + definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := + by cases H + + protected definition le_trans {n m k : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := + begin + induction H2 with k H2 IH, + { exact H1}, + { exact le.step IH} + end + + definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := + begin + cases H with m H', + { apply le.tr_refl}, + { exact trunc_index.le_trans (le.step !le.tr_refl) H'} + end + + theorem not_succ_le_self {n : ℕ₋₂} : ¬n.+1 ≤ n := + begin + induction n with n IH: intro H, + { exact not_succ_le_minus_two H}, + { exact IH (le_of_succ_le_succ H)} + end + + protected definition le_antisymm {n m : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := + begin + induction H2 with n H2 IH, + { reflexivity}, + { exfalso, apply @not_succ_le_self n, exact trunc_index.le_trans H1 H2} + end + + protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m): n ≤ m.+1 := + le.step H1 + +end trunc_index open trunc_index + +definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index := +weak_order.mk le trunc_index.le_refl @trunc_index.le_trans @trunc_index.le_antisymm + +namespace trunc_index + + /- more theorems about truncation indices -/ + + definition zero_add (n : ℕ₋₂) : (0 : ℕ₋₂) + n = n := + begin + cases n with n, reflexivity, + cases n with n, reflexivity, + induction n with n IH, reflexivity, exact ap succ IH + end + + definition add_zero (n : ℕ₋₂) : n + (0 : ℕ₋₂) = n := + by reflexivity + + definition succ_add_nat (n : ℕ₋₂) (m : ℕ) : n.+1 + m = (n + m).+1 := + by induction m with m IH; reflexivity; exact ap succ IH + + definition nat_add_succ (n : ℕ) (m : ℕ₋₂) : n + m.+1 = (n + m).+1 := + begin + cases m with m, reflexivity, + cases m with m, reflexivity, + induction m with m IH, reflexivity, exact ap succ IH + end + + definition add_nat_succ (n : ℕ₋₂) (m : ℕ) : n + (nat.succ m) = (n + m).+1 := + by reflexivity + + definition nat_succ_add (n : ℕ) (m : ℕ₋₂) : (nat.succ n) + m = (n + m).+1 := + begin + cases m with m, reflexivity, + cases m with m, reflexivity, + induction m with m IH, reflexivity, exact ap succ IH + end + + definition sub_two_add_two (n : ℕ₋₂) : sub_two (add_two n) = n := + begin + induction n with n IH, + { reflexivity}, + { exact ap succ IH} + end + + definition add_two_sub_two (n : ℕ) : add_two (sub_two n) = n := + begin + induction n with n IH, + { reflexivity}, + { exact ap nat.succ IH} + end + + definition of_nat_add_plus_two_of_nat (n m : ℕ) : n +2+ m = of_nat (n + m + 2) := + begin + induction m with m IH, + { reflexivity}, + { exact ap succ IH} + end + + definition of_nat_add_of_nat (n m : ℕ) : of_nat n + of_nat m = of_nat (n + m) := + begin + induction m with m IH, + { reflexivity}, + { exact ap succ IH} + end + + definition succ_add_plus_two (n m : ℕ₋₂) : n.+1 +2+ m = (n +2+ m).+1 := + begin + induction m with m IH, + { reflexivity}, + { exact ap succ IH} + end + + definition add_plus_two_succ (n m : ℕ₋₂) : n +2+ m.+1 = (n +2+ m).+1 := + idp + + definition add_succ_succ (n m : ℕ₋₂) : n + m.+2 = n +2+ m := + idp + + definition succ_add_succ (n m : ℕ₋₂) : n.+1 + m.+1 = n +2+ m := + begin + cases m with m IH, + { reflexivity}, + { apply succ_add_plus_two} + end + + definition succ_succ_add (n m : ℕ₋₂) : n.+2 + m = n +2+ m := + begin + cases m with m IH, + { reflexivity}, + { exact !succ_add_succ ⬝ !succ_add_plus_two} + end + + definition succ_sub_two (n : ℕ) : (nat.succ n).-2 = n.-2 .+1 := rfl + definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl + definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl + + definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) := + begin + induction H with m H IH, + { apply le.refl}, + { exact trunc_index.le_succ IH} + end + + definition sub_two_le_sub_two {n m : ℕ} (H : n ≤ m) : n.-2 ≤ m.-2 := + begin + induction H with m H IH, + { apply le.refl}, + { exact trunc_index.le_succ IH} + end + + definition add_two_le_add_two {n m : ℕ₋₂} (H : n ≤ m) : add_two n ≤ add_two m := + begin + induction H with m H IH, + { reflexivity}, + { constructor, exact IH}, + end + + definition le_of_sub_two_le_sub_two {n m : ℕ} (H : n.-2 ≤ m.-2) : n ≤ m := + begin + rewrite [-add_two_sub_two n, -add_two_sub_two m], + exact add_two_le_add_two H, + end + + definition le_of_of_nat_le_of_nat {n m : ℕ} (H : of_nat n ≤ of_nat m) : n ≤ m := + begin + apply le_of_sub_two_le_sub_two, + exact le_of_succ_le_succ (le_of_succ_le_succ H) + end + +end trunc_index open trunc_index namespace is_trunc - namespace trunc_index - - definition minus_one_le_succ (n : trunc_index) : -1 ≤ n.+1 := - succ_le_succ (minus_two_le n) - - definition zero_le_of_nat (n : ℕ) : 0 ≤ of_nat n := - succ_le_succ !minus_one_le_succ - - open decidable - protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₂), decidable (n = m) - | has_decidable_eq -2 -2 := inl rfl - | has_decidable_eq (n.+1) -2 := inr (by contradiction) - | has_decidable_eq -2 (m.+1) := inr (by contradiction) - | has_decidable_eq (n.+1) (m.+1) := - match has_decidable_eq n m with - | inl xeqy := inl (by rewrite xeqy) - | inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney) - end - - definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := - by cases H - - protected definition le_trans {n m k : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := - begin - induction H2 with k H2 IH, - { exact H1}, - { exact le.step IH} - end - - definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := - begin - cases H with m H', - { apply le.tr_refl}, - { exact trunc_index.le_trans (le.step !le.tr_refl) H'} - end - - theorem not_succ_le_self {n : ℕ₋₂} : ¬n.+1 ≤ n := - begin - induction n with n IH: intro H, - { exact not_succ_le_minus_two H}, - { exact IH (le_of_succ_le_succ H)} - end - - protected definition le_antisymm {n m : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ n) : n = m := - begin - induction H2 with n H2 IH, - { reflexivity}, - { exfalso, apply @not_succ_le_self n, exact trunc_index.le_trans H1 H2} - end - - protected definition le_succ {n m : ℕ₋₂} (H1 : n ≤ m): n ≤ m.+1 := - le.step H1 - - end trunc_index open trunc_index - - definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index := - weak_order.mk le trunc_index.le_refl @trunc_index.le_trans @trunc_index.le_antisymm - - namespace trunc_index - - /- more theorems about truncation indices -/ - - definition zero_add (n : ℕ₋₂) : (0 : ℕ₋₂) + n = n := - begin - cases n with n, reflexivity, - cases n with n, reflexivity, - induction n with n IH, reflexivity, exact ap succ IH - end - - definition add_zero (n : ℕ₋₂) : n + (0 : ℕ₋₂) = n := - by reflexivity - - definition succ_add_nat (n : ℕ₋₂) (m : ℕ) : n.+1 + m = (n + m).+1 := - by induction m with m IH; reflexivity; exact ap succ IH - - definition nat_add_succ (n : ℕ) (m : ℕ₋₂) : n + m.+1 = (n + m).+1 := - begin - cases m with m, reflexivity, - cases m with m, reflexivity, - induction m with m IH, reflexivity, exact ap succ IH - end - - definition add_nat_succ (n : ℕ₋₂) (m : ℕ) : n + (nat.succ m) = (n + m).+1 := - by reflexivity - - definition nat_succ_add (n : ℕ) (m : ℕ₋₂) : (nat.succ n) + m = (n + m).+1 := - begin - cases m with m, reflexivity, - cases m with m, reflexivity, - induction m with m IH, reflexivity, exact ap succ IH - end - - definition sub_two_add_two (n : ℕ₋₂) : sub_two (add_two n) = n := - begin - induction n with n IH, - { reflexivity}, - { exact ap succ IH} - end - - definition add_two_sub_two (n : ℕ) : add_two (sub_two n) = n := - begin - induction n with n IH, - { reflexivity}, - { exact ap nat.succ IH} - end - - definition of_nat_add_plus_two_of_nat (n m : ℕ) : n +2+ m = of_nat (n + m + 2) := - begin - induction m with m IH, - { reflexivity}, - { exact ap succ IH} - end - - definition of_nat_add_of_nat (n m : ℕ) : of_nat n + of_nat m = of_nat (n + m) := - begin - induction m with m IH, - { reflexivity}, - { exact ap succ IH} - end - - definition succ_add_plus_two (n m : ℕ₋₂) : n.+1 +2+ m = (n +2+ m).+1 := - begin - induction m with m IH, - { reflexivity}, - { exact ap succ IH} - end - - definition add_plus_two_succ (n m : ℕ₋₂) : n +2+ m.+1 = (n +2+ m).+1 := - idp - - definition add_succ_succ (n m : ℕ₋₂) : n + m.+2 = n +2+ m := - idp - - definition succ_add_succ (n m : ℕ₋₂) : n.+1 + m.+1 = n +2+ m := - begin - cases m with m IH, - { reflexivity}, - { apply succ_add_plus_two} - end - - definition succ_succ_add (n m : ℕ₋₂) : n.+2 + m = n +2+ m := - begin - cases m with m IH, - { reflexivity}, - { exact !succ_add_succ ⬝ !succ_add_plus_two} - end - - definition succ_sub_two (n : ℕ) : (nat.succ n).-2 = n.-2 .+1 := rfl - definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl - definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl - - definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) := - begin - induction H with m H IH, - { apply le.refl}, - { exact trunc_index.le_succ IH} - end - - definition sub_two_le_sub_two {n m : ℕ} (H : n ≤ m) : n.-2 ≤ m.-2 := - begin - induction H with m H IH, - { apply le.refl}, - { exact trunc_index.le_succ IH} - end - - definition add_two_le_add_two {n m : ℕ₋₂} (H : n ≤ m) : add_two n ≤ add_two m := - begin - induction H with m H IH, - { reflexivity}, - { constructor, exact IH}, - end - - definition le_of_sub_two_le_sub_two {n m : ℕ} (H : n.-2 ≤ m.-2) : n ≤ m := - begin - rewrite [-add_two_sub_two n, -add_two_sub_two m], - exact add_two_le_add_two H, - end - - definition le_of_of_nat_le_of_nat {n m : ℕ} (H : of_nat n ≤ of_nat m) : n ≤ m := - begin - apply le_of_sub_two_le_sub_two, - exact le_of_succ_le_succ (le_of_succ_le_succ H) - end - - end trunc_index open trunc_index - variables {A B : Type} {n : ℕ₋₂} /- theorems about trunctype -/ @@ -374,7 +374,7 @@ namespace is_trunc { apply is_trunc_eq} end -end is_trunc open is_trunc is_trunc.trunc_index +end is_trunc open is_trunc namespace trunc variable {A : Type}