From e5d5ef9d5575c6788fb0f92675fe3f27d32abd98 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 24 Feb 2016 19:43:50 -0500 Subject: [PATCH] feat(hott/library): various changes and additions. Most notably: Give le.refl the attribute [refl]. This simplifies tactic proofs in various places. Redefine the order of trunc_index, and instantiate it as weak order. Add more about pointed equivalences. --- hott/algebra/homotopy_group.hlean | 14 +- hott/algebra/order.hlean | 10 +- hott/algebra/ordered_group.hlean | 2 +- hott/homotopy/circle.hlean | 4 +- hott/homotopy/sphere.hlean | 24 +- hott/init/path.hlean | 22 +- hott/init/trunc.hlean | 136 +++++----- hott/types/pointed.hlean | 31 ++- hott/types/pointed2.hlean | 56 ++++- hott/types/trunc.hlean | 235 +++++++++++++++--- hott/types/univ.hlean | 2 +- library/algebra/complete_lattice.lean | 8 +- library/algebra/order.lean | 10 +- library/algebra/order_bigops.lean | 4 +- library/algebra/ring_bigops.lean | 11 +- library/data/real/complete.lean | 4 - .../measure_theory/extended_real.lean | 2 +- src/emacs/lean-input.el | 9 +- 18 files changed, 414 insertions(+), 170 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 272bbab79..6a156f775 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -40,13 +40,13 @@ namespace eq definition fundamental_group [constructor] (A : Type*) : Group := ghomotopy_group zero A - notation `πG[`:95 n:0 ` +1] `:0 A:95 := ghomotopy_group n A - notation `πaG[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A + notation `πg[`:95 n:0 ` +1] `:0 A:95 := ghomotopy_group n A + notation `πag[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A prefix `π₁`:95 := fundamental_group open equiv unit - theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πG[n+1] A = G0 := + theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 := begin apply trivial_group_of_is_contr, apply is_trunc_trunc_of_is_trunc, @@ -54,9 +54,9 @@ namespace eq apply is_trunc_succ_succ_of_is_set end - definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πG[ n +1] A = π₁ Ω[n] A := idp + definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πg[ n +1] A = π₁ Ω[n] A := idp - definition homotopy_group_succ_in (A : Type*) (n : ℕ) : πG[succ n +1] A = πG[n +1] Ω A := + definition homotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A := begin fapply Group_eq, { apply equiv_of_eq, exact ap (λ(X : Type*), trunc 0 X) (loop_space_succ_eq_in A (succ n))}, @@ -65,7 +65,7 @@ namespace eq apply loop_space_succ_eq_in_concat end end}, end - definition homotopy_group_add (A : Type*) (n m : ℕ) : πG[n+m +1] A = πG[n +1] Ω[m] A := + definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A = πg[n +1] Ω[m] A := begin revert A, induction m with m IH: intro A, { reflexivity}, @@ -74,7 +74,7 @@ namespace eq end theorem trivial_homotopy_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_set (Ω[n] A)) - : πG[m+n+1] A = G0 := + : πg[m+n+1] A = G0 := !homotopy_group_add ⬝ !trivial_homotopy_of_is_set definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean index d0b6049b8..47acbf3a7 100644 --- a/hott/algebra/order.hlean +++ b/hott/algebra/order.hlean @@ -23,7 +23,7 @@ section variable [s : weak_order A] include s - definition le.refl (a : A) : a ≤ a := !weak_order.le_refl + definition le.refl [refl] (a : A) : a ≤ a := !weak_order.le_refl definition le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a @@ -307,13 +307,13 @@ section theorem min_le_left (a b : A) : min a b ≤ a := by_cases - (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply le.refl) + (assume H : a ≤ b, by rewrite [↑min, if_pos H]) (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le_of_lt (lt_of_not_ge H)) theorem min_le_right (a b : A) : min a b ≤ b := by_cases (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply H) - (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le.refl) + (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]) theorem le_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ min a b := by_cases @@ -323,11 +323,11 @@ section theorem le_max_left (a b : A) : a ≤ max a b := by_cases (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H) - (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le.refl) + (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]) theorem le_max_right (a b : A) : b ≤ max a b := by_cases - (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply le.refl) + (assume H : a ≤ b, by rewrite [↑max, if_pos H]) (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le_of_lt (lt_of_not_ge H)) theorem max_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : max a b ≤ c := diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean index 723d9603d..6edcaf543 100644 --- a/hott/algebra/ordered_group.hlean +++ b/hott/algebra/ordered_group.hlean @@ -16,7 +16,7 @@ variable {A : Type} namespace algebra structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A, - add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A := + add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A := (add_le_add_left : Πa b, le a b → Πc, le (add c a) (add c b)) (le_of_add_le_add_left : Πa b c, le (add a b) (add a c) → le b c) (add_lt_add_left : Πa b, lt a b → Πc, lt (add c a) (add c b)) diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index b5fcce244..abbae1108 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -252,7 +252,7 @@ namespace circle end open nat - definition homotopy_group_of_circle (n : ℕ) : πG[n+1 +1] S¹. = G0 := + definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. = G0 := begin refine @trivial_homotopy_of_is_set_loop_space S¹. 1 n _, apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv @@ -272,7 +272,7 @@ namespace circle definition is_trunc_circle [instance] : is_trunc 1 S¹ := begin apply is_trunc_succ_of_is_trunc_loop, - { exact unit.star}, + { apply trunc_index.minus_one_le_succ}, { intro x, apply is_trunc_equiv_closed_rev, apply eq_equiv_Z} end diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index d219a078b..a6a084a34 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -48,16 +48,25 @@ namespace sphere_index notation `-1` := minus_one notation `ℕ₋₁` := sphere_index - definition add (n m : sphere_index) : sphere_index := + definition add_plus_one (n m : sphere_index) : sphere_index := sphere_index.rec_on m n (λ k l, l .+1) - definition leq (n m : sphere_index) : Type₀ := + -- addition of sphere_indices, where (-1 + -1) is defined to be -1. + protected definition add (n m : sphere_index) : sphere_index := + sphere_index.cases_on m + (sphere_index.cases_on n -1 id) + (sphere_index.rec n (λn' r, succ r)) + + protected definition le (n m : sphere_index) : Type₀ := sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m - infix `+1+`:65 := sphere_index.add + infix `+1+`:65 := sphere_index.add_plus_one + + definition has_add_sphere_index [instance] [priority 2000] [reducible] : has_add ℕ₋₁ := + has_add.mk sphere_index.add definition has_le_sphere_index [instance] : has_le sphere_index := - has_le.mk leq + has_le.mk sphere_index.le definition succ_le_succ {n m : sphere_index} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed definition le_of_succ_le_succ {n m : sphere_index} (H : n.+1 ≤ m.+1) : n ≤ m := proof H qed @@ -125,16 +134,17 @@ namespace sphere definition sphere_eq_bool : S 0 = bool := ua sphere_equiv_bool - definition sphere_eq_bool_pointed : S. 0 = pbool := + definition sphere_eq_pbool : S. 0 = pbool := pType_eq sphere_equiv_bool idp - -- TODO: the commented-out part makes the forward function below "apn _ surf" + -- TODO1: the commented-out part makes the forward function below "apn _ surf" + -- TODO2: we could make this a pointed equivalence definition pmap_sphere (A : Type*) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A := begin -- fapply equiv_change_fun, -- { revert A, induction n with n IH: intro A, - { krewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv}, + { apply tr_rev (λx, x →* _ ≃ _) sphere_eq_pbool, apply pmap_bool_equiv}, { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e _, rewrite [loop_space_succ_eq_in]} -- }, -- { intro f, exact apn n f surf}, diff --git a/hott/init/path.hlean b/hott/init/path.hlean index e1114f2f2..9561099cc 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -56,11 +56,11 @@ namespace eq -- Concatenation is associative. definition con.assoc' (p : x = y) (q : y = z) (r : z = t) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r := - by induction r; induction q; reflexivity + by induction r; reflexivity definition con.assoc (p : x = y) (q : y = z) (r : z = t) : (p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) := - by induction r; induction q; reflexivity + by induction r; reflexivity -- The left inverse law. definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp := @@ -80,10 +80,10 @@ namespace eq by induction q; induction p; reflexivity definition con_inv_cancel_right (p : x = y) (q : y = z) : (p ⬝ q) ⬝ q⁻¹ = p := - by induction q; induction p; reflexivity + by induction q; reflexivity definition inv_con_cancel_right (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p := - by induction q; induction p; reflexivity + by induction q; reflexivity -- Inverse distributes over concatenation definition con_inv (p : x = y) (q : y = z) : (p ⬝ q)⁻¹ = q⁻¹ ⬝ p⁻¹ := @@ -168,22 +168,22 @@ namespace eq by induction p; intro h; exact h ⬝ !idp_con definition con_inv_eq_idp [unfold 6] {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp := - by cases r;apply con.right_inv + by cases r; apply con.right_inv definition inv_con_eq_idp [unfold 6] {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp := - by cases r;apply con.left_inv + by cases r; apply con.left_inv definition con_eq_idp {p : x = y} {q : y = x} (r : p = q⁻¹) : p ⬝ q = idp := - by cases q;exact r + by cases q; exact r definition idp_eq_inv_con {p q : x = y} (r : p = q) : idp = p⁻¹ ⬝ q := - by cases r;exact !con.left_inv⁻¹ + by cases r; exact !con.left_inv⁻¹ definition idp_eq_con_inv {p q : x = y} (r : p = q) : idp = q ⬝ p⁻¹ := - by cases r;exact !con.right_inv⁻¹ + by cases r; exact !con.right_inv⁻¹ definition idp_eq_con {p : x = y} {q : y = x} (r : p⁻¹ = q) : idp = q ⬝ p := - by cases p;exact r + by cases p; exact r /- Transport -/ @@ -248,7 +248,7 @@ namespace eq definition apd [unfold 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y := by induction p; reflexivity - definition ap011 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := + definition ap011 [unfold 9] (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := by cases Ha; exact ap (f a) Hb /- More theorems for moving things around in equations -/ diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 527e0eab4..5aaaf2c46 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -23,15 +23,9 @@ namespace is_trunc open trunc_index - definition has_zero_trunc_index [instance] [priority 2000] : has_zero trunc_index := - has_zero.mk (succ (succ minus_two)) - - definition has_one_trunc_index [instance] [priority 2000] : has_one trunc_index := - has_one.mk (succ (succ (succ minus_two))) - /- notation for trunc_index is -2, -1, 0, 1, ... - from 0 and up this comes from a coercion from num to trunc_index (via nat) + 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 @@ -39,47 +33,63 @@ namespace is_trunc 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) : trunc_index := + definition add_plus_two [reducible] (n m : ℕ₋₂) : ℕ₋₂ := trunc_index.rec_on m n (λ k l, l .+1) -- addition of trunc_indices, where results smaller than -2 are changed to -2 - definition tr_add (n m : trunc_index) : trunc_index := + protected definition add (n m : ℕ₋₂) : ℕ₋₂ := trunc_index.cases_on m (trunc_index.cases_on n -2 (λn', (trunc_index.cases_on n' -2 id))) (λm', trunc_index.cases_on m' (trunc_index.cases_on n -2 id) (trunc_index.rec n (λn' r, succ r))) - definition leq [reducible] (n m : trunc_index) : Type₀ := - trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m - - definition has_le_trunc_index [instance] [priority 2000] : has_le trunc_index := - has_le.mk leq + /- we give a weird name to the reflexivity step to avoid overloading le.refl + (which can be used if types.trunc is imported) -/ + inductive le (a : ℕ₋₂) : ℕ₋₂ → Type := + | tr_refl : le a a + | step : Π {b}, le a b → le a (b.+1) end trunc_index - attribute trunc_index.tr_add [reducible] + 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.tr_add + has_add.mk trunc_index.add - namespace trunc_index - definition succ_le_succ {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed - definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := proof H qed - definition minus_two_le (n : trunc_index) : -2 ≤ n := star - definition le.refl (n : trunc_index) : n ≤ n := by induction n with n IH; exact star; exact IH - definition empty_of_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := H - end trunc_index - definition trunc_index.of_nat [coercion] [reducible] (n : nat) : trunc_index := - (nat.rec_on n -2 (λ n k, k.+1)).+2 - - definition sub_two [reducible] (n : nat) : trunc_index := + definition sub_two [reducible] (n : ℕ) : ℕ₋₂ := nat.rec_on n -2 (λ n k, k.+1) + definition add_two [reducible] (n : ℕ₋₂) : ℕ := + trunc_index.rec_on n nat.zero (λ n k, nat.succ k) + postfix ` .-2`:(max+1) := sub_two + definition trunc_index.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 + + definition minus_two_le (n : ℕ₋₂) : -2 ≤ n := + by induction n with n IH; apply le.tr_refl; exact le.step IH + protected definition le_refl (n : ℕ₋₂) : n ≤ n := + le.tr_refl n + + end trunc_index + /- truncated types -/ /- @@ -91,14 +101,14 @@ namespace is_trunc (center : A) (center_eq : Π(a : A), center = a) - definition is_trunc_internal (n : trunc_index) : Type → Type := + definition is_trunc_internal (n : ℕ₋₂) : Type → Type := trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x = y))) end is_trunc open is_trunc -structure is_trunc [class] (n : trunc_index) (A : Type) := +structure is_trunc [class] (n : ℕ₋₂) (A : Type) := (to_internal : is_trunc_internal n A) open nat num is_trunc.trunc_index @@ -111,12 +121,12 @@ namespace is_trunc variables {A B : Type} - definition is_trunc_succ_intro (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x = y)] + definition is_trunc_succ_intro (A : Type) (n : ℕ₋₂) [H : ∀x y : A, is_trunc n (x = y)] : is_trunc n.+1 A := is_trunc.mk (λ x y, !is_trunc.to_internal) definition is_trunc_eq [instance] [priority 1200] - (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := + (n : ℕ₋₂) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := is_trunc.mk (is_trunc.to_internal (n.+1) A x y) /- contractibility -/ @@ -144,7 +154,7 @@ namespace is_trunc /- truncation is upward close -/ -- n-types are also (n+1)-types - theorem is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index) + theorem is_trunc_succ [instance] [priority 900] (A : Type) (n : ℕ₋₂) [H : is_trunc n A] : is_trunc (n.+1) A := trunc_index.rec_on n (λ A (H : is_contr A), !is_trunc_succ_intro) @@ -152,43 +162,35 @@ namespace is_trunc A H --in the proof the type of H is given explicitly to make it available for class inference - theorem is_trunc_of_leq.{l} (A : Type.{l}) {n m : trunc_index} (Hnm : n ≤ m) + theorem is_trunc_of_le.{l} (A : Type.{l}) {n m : ℕ₋₂} (Hnm : n ≤ m) [Hn : is_trunc n A] : is_trunc m A := - have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from - λ k A, trunc_index.cases_on k - (λh1 h2, h2) - (λk h1 h2, empty.elim (trunc_index.empty_of_succ_le_minus_two h1)), - have step : Π (m : trunc_index) - (IHm : Π (n : trunc_index) (A : Type), n ≤ m → is_trunc n A → is_trunc m A) - (n : trunc_index) (A : Type) - (Hnm : n ≤ m .+1) (Hn : is_trunc n A), is_trunc m .+1 A, from - λm IHm n, trunc_index.rec_on n - (λA Hnm Hn, @is_trunc_succ A m (IHm -2 A star Hn)) - (λn IHn A Hnm (Hn : is_trunc n.+1 A), - @is_trunc_succ_intro A m (λx y, IHm n (x = y) (trunc_index.le_of_succ_le_succ Hnm) _)), - trunc_index.rec_on m base step n A Hnm Hn + begin + induction Hnm with m Hnm IH, + { exact Hn}, + { exact _} + end - definition is_trunc_of_imp_is_trunc {n : trunc_index} (H : A → is_trunc (n.+1) A) + definition is_trunc_of_imp_is_trunc {n : ℕ₋₂} (H : A → is_trunc (n.+1) A) : is_trunc (n.+1) A := @is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y) - definition is_trunc_of_imp_is_trunc_of_leq {n : trunc_index} (Hn : -1 ≤ n) (H : A → is_trunc n A) + definition is_trunc_of_imp_is_trunc_of_le {n : ℕ₋₂} (Hn : -1 ≤ n) (H : A → is_trunc n A) : is_trunc n A := - trunc_index.rec_on n (λHn H, empty.rec _ Hn) - (λn IH Hn, is_trunc_of_imp_is_trunc) - Hn H + begin + cases Hn with n' Hn': apply is_trunc_of_imp_is_trunc H + end -- these must be definitions, because we need them to compute sometimes - definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A := + definition is_trunc_of_is_contr (A : Type) (n : ℕ₋₂) [H : is_contr A] : is_trunc n A := trunc_index.rec_on n H (λn H, _) - definition is_trunc_succ_of_is_prop (A : Type) (n : trunc_index) [H : is_prop A] + definition is_trunc_succ_of_is_prop (A : Type) (n : ℕ₋₂) [H : is_prop A] : is_trunc (n.+1) A := - is_trunc_of_leq A (show -1 ≤ n.+1, from star) + is_trunc_of_le A (show -1 ≤ n.+1, from succ_le_succ (minus_two_le n)) - definition is_trunc_succ_succ_of_is_set (A : Type) (n : trunc_index) [H : is_set A] + definition is_trunc_succ_succ_of_is_set (A : Type) (n : ℕ₋₂) [H : is_set A] : is_trunc (n.+2) A := - @(is_trunc_of_leq A (show 0 ≤ n.+2, from proof star qed)) H + is_trunc_of_le A (show 0 ≤ n.+2, from succ_le_succ (succ_le_succ (minus_two_le n))) /- props -/ @@ -244,10 +246,10 @@ namespace is_trunc local attribute is_contr_unit is_prop_empty [instance] - definition is_trunc_unit [instance] (n : trunc_index) : is_trunc n unit := + definition is_trunc_unit [instance] (n : ℕ₋₂) : is_trunc n unit := !is_trunc_of_is_contr - definition is_trunc_empty [instance] (n : trunc_index) : is_trunc (n.+1) empty := + definition is_trunc_empty [instance] (n : ℕ₋₂) : is_trunc (n.+1) empty := !is_trunc_succ_of_is_prop /- interaction with equivalences -/ @@ -267,7 +269,7 @@ namespace is_trunc (λa, center B) (is_equiv.adjointify (λa, center B) (λb, center A) center_eq center_eq) - theorem is_trunc_is_equiv_closed (n : trunc_index) (f : A → B) [H : is_equiv f] + theorem is_trunc_is_equiv_closed (n : ℕ₋₂) (f : A → B) [H : is_equiv f] [HA : is_trunc n A] : is_trunc n B := trunc_index.rec_on n (λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f) @@ -275,15 +277,15 @@ namespace is_trunc IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv)) A HA B f H - definition is_trunc_is_equiv_closed_rev (n : trunc_index) (f : A → B) [H : is_equiv f] + definition is_trunc_is_equiv_closed_rev (n : ℕ₋₂) (f : A → B) [H : is_equiv f] [HA : is_trunc n B] : is_trunc n A := is_trunc_is_equiv_closed n f⁻¹ - definition is_trunc_equiv_closed (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] + definition is_trunc_equiv_closed (n : ℕ₋₂) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B := is_trunc_is_equiv_closed n (to_fun f) - definition is_trunc_equiv_closed_rev (n : trunc_index) (f : A ≃ B) [HA : is_trunc n B] + definition is_trunc_equiv_closed_rev (n : ℕ₋₂) (f : A ≃ B) [HA : is_trunc n B] : is_trunc n A := is_trunc_is_equiv_closed n (to_inv f) @@ -299,7 +301,7 @@ namespace is_trunc equiv_of_is_prop (iff.elim_left H) (iff.elim_right H) /- truncatedness of lift -/ - definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : trunc_index) + definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : ℕ₋₂) [H : is_trunc n A] : is_trunc n (lift A) := is_trunc_equiv_closed _ !equiv_lift @@ -326,7 +328,7 @@ namespace is_trunc pathover_of_eq_tr !is_prop.elim definition is_trunc_pathover [instance] - (n : trunc_index) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) := + (n : ℕ₋₂) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) := is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr variables {p c c₂} @@ -339,7 +341,7 @@ namespace is_trunc end is_trunc -structure trunctype (n : trunc_index) := +structure trunctype (n : ℕ₋₂) := (carrier : Type) (struct : is_trunc n carrier) @@ -353,13 +355,13 @@ attribute trunctype.struct [instance] [priority 1400] protected abbreviation Prop.mk := @trunctype.mk -1 protected abbreviation Set.mk := @trunctype.mk (-1.+1) -protected definition trunctype.mk' [constructor] (n : trunc_index) (A : Type) [H : is_trunc n A] +protected definition trunctype.mk' [constructor] (n : ℕ₋₂) (A : Type) [H : is_trunc n A] : n-Type := trunctype.mk A H namespace is_trunc - definition tlift.{u v} [constructor] {n : trunc_index} (A : trunctype.{u} n) + definition tlift.{u v} [constructor] {n : ℕ₋₂} (A : trunctype.{u} n) : trunctype.{max u v} n := trunctype.mk (lift A) !is_trunc_lift diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 2c7143aec..4a55ffef9 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -84,6 +84,12 @@ namespace pointed prefix `Ω`:(max+5) := ploop_space notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A + definition iterated_ploop_space_zero [unfold_full] (A : Type*) + : Ω[0] A = A := rfl + + definition iterated_ploop_space_succ [unfold_full] (k : ℕ) (A : Type*) + : Ω[succ k] A = Ω Ω[k] A := rfl + definition rfln [constructor] [reducible] {A : Type*} {n : ℕ} : Ω[n] A := pt definition refln [constructor] [reducible] (A : Type*) (n : ℕ) : Ω[n] A := pt definition refln_eq_refl (A : Type*) (n : ℕ) : rfln = rfl :> Ω[succ n] A := rfl @@ -246,10 +252,10 @@ namespace pointed /- categorical properties of pointed maps -/ - definition pid [constructor] (A : Type*) : A →* A := + definition pid [constructor] [refl] (A : Type*) : A →* A := pmap.mk id idp - definition pcompose [constructor] (g : B →* C) (f : A →* B) : A →* C := + definition pcompose [constructor] [trans] (g : B →* C) (f : A →* B) : A →* C := pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g) infixr ` ∘* `:60 := pcompose @@ -327,12 +333,16 @@ namespace pointed { esimp, exact !con.left_inv⁻¹}}, end - /- instances of pointed maps -/ - -- The constant pointed map between any two types definition pconst [constructor] (A B : Type*) : A →* B := pmap.mk (λ a, Point B) idp + -- the pointed type of pointed maps + definition ppmap [constructor] (A B : Type*) : Type* := + pType.mk (A →* B) (pconst A B) + + /- instances of pointed maps -/ + definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := begin fconstructor, @@ -340,7 +350,7 @@ namespace pointed { esimp, apply con.left_inv} end - definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := + definition apn (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := begin induction n with n IH, { exact f}, @@ -362,10 +372,6 @@ namespace pointed intro p, exact !idp_con⁻¹ end - -- TODO: - -- definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := - -- _ - definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f := begin induction B, induction C, induction g with g pg, induction f with f pf, esimp at *, @@ -484,6 +490,13 @@ namespace pointed { esimp, } end -/ + definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := + begin + induction n with n IH, + { reflexivity}, + { refine ap1_phomotopy IH ⬝* _, apply ap1_compose} + end + infix ` ⬝*p `:75 := pconcat_eq infix ` ⬝p* `:75 := eq_pconcat diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index 6b2d12ffd..081c02555 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -36,11 +36,15 @@ namespace pointed definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B := pequiv.mk f _ H + protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A) + (gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B := + pequiv.mk f (adjointify f g fg gf) (respect_pt f) + definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B := equiv.mk f _ definition to_pinv [constructor] (f : A ≃* B) : B →* A := - pmap.mk f⁻¹ (ap f⁻¹ (respect_pt f)⁻¹ ⬝ !left_inv) + pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ !left_inv) definition pua {A B : Type*} (f : A ≃* B) : A = B := pType_eq (equiv_of_pequiv f) !respect_pt @@ -103,7 +107,7 @@ namespace pointed definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A := phomotopy.mk (left_inv f) abstract begin - esimp, rewrite ap_inv, symmetry, apply con_inv_cancel_left + esimp, symmetry, apply con_inv_cancel_left end end definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B := @@ -182,9 +186,55 @@ namespace pointed (p : h ~* f ∘* g) : f⁻¹ᵉ* ∘* h ~* g := (phomotopy_pinv_left_of_phomotopy p⁻¹*)⁻¹* - definition phomotopy_of_phomotopy_pinv_left {f : C ≃* B} {g : A →* B} {h : A →* C} (p : h ~* f⁻¹ᵉ* ∘* g) : f ∘* h ~* g := (phomotopy_of_pinv_left_phomotopy p⁻¹*)⁻¹* + /- pointed equivalences between particular pointed types -/ + + definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B := + pequiv.MK (ap1 f) (ap1 f⁻¹ᵉ*) + abstract begin + intro p, + refine ((ap1_compose f⁻¹ᵉ* f) p)⁻¹ ⬝ _, + refine ap1_phomotopy (pleft_inv f) p ⬝ _, + exact ap1_id p + end end + abstract begin + intro p, + refine ((ap1_compose f f⁻¹ᵉ*) p)⁻¹ ⬝ _, + refine ap1_phomotopy (pright_inv f) p ⬝ _, + exact ap1_id p + end end + + definition loopn_pequiv_loopn (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B := + begin + induction n with n IH, + { exact f}, + { exact loop_pequiv_loop IH} + end + + definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') : + ppmap A B →* ppmap A' B' := + pmap.mk (λh, g ∘* h ∘* f) + abstract begin + fapply pmap_eq, + { esimp, intro a, exact respect_pt g}, + { rewrite [▸*, ap_constant], apply idp_con} + end end + +/- + definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') : + ppmap A B ≃* ppmap A' B' := + pequiv.MK (pmap_functor f⁻¹ᵉ* g) (pmap_functor f g⁻¹ᵉ*) + abstract begin + intro a, esimp, apply pmap_eq, + { esimp, }, + { } + end end + abstract begin + + end end +-/ + end pointed diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index b48f689a0..f9b1cc51a 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -8,16 +8,152 @@ Properties of is_trunc and trunctype -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc -import types.pi types.eq types.equiv ..function +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_equiv prod is_trunc.trunc_index pointed nat is_trunc algebra namespace is_trunc - variables {A B : Type} {n : trunc_index} + + 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 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}, + { apply ap succ IH} + end + + definition add_two_sub_two (n : ℕ) : add_two (sub_two n) = n := + begin + induction n with n IH, + { reflexivity}, + { apply ap nat.succ IH} + 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 -/ - protected definition trunctype.sigma_char.{l} (n : trunc_index) : + protected definition trunctype.sigma_char.{l} [constructor] (n : ℕ₋₂) : (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := begin fapply equiv.MK, @@ -27,7 +163,7 @@ namespace is_trunc { intro A, induction A with A1 A2, reflexivity}, end - definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) : + definition trunctype_eq_equiv [constructor] (n : ℕ₋₂) (A B : n-Type) : (A = B) ≃ (carrier A = carrier B) := calc (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B) @@ -40,13 +176,13 @@ namespace is_trunc (Hn : -1 ≤ n) : is_trunc n A := begin induction n with n, - {exact !empty.elim Hn}, + {exfalso, exact not_succ_le_minus_two Hn}, {apply is_trunc_succ_intro, intro a a', fapply @is_trunc_is_equiv_closed_rev _ _ n (ap f)} end theorem is_trunc_is_retraction_closed (f : A → B) [Hf : is_retraction f] - (n : trunc_index) [HA : is_trunc n A] : is_trunc n B := + (n : ℕ₋₂) [HA : is_trunc n A] : is_trunc n B := begin revert A B f Hf HA, induction n with n IH, @@ -67,22 +203,22 @@ namespace is_trunc definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B) := λf f', !is_equiv_ap_to_fun - theorem is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) := + theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) := begin apply is_trunc_succ_intro, intro X Y, fapply is_trunc_equiv_closed, - {apply equiv.symm, apply trunctype_eq_equiv}, + { apply equiv.symm, apply trunctype_eq_equiv}, fapply is_trunc_equiv_closed, - {apply equiv.symm, apply eq_equiv_equiv}, + { apply equiv.symm, apply eq_equiv_equiv}, induction n, - {apply @is_contr_of_inhabited_prop, - {apply is_trunc_is_embedding_closed, - {apply is_embedding_to_fun} , - {exact unit.star}}, - {apply equiv_of_is_contr_of_is_contr}}, - {apply is_trunc_is_embedding_closed, - {apply is_embedding_to_fun}, - {exact unit.star}} + { apply @is_contr_of_inhabited_prop, + { apply is_trunc_is_embedding_closed, + { apply is_embedding_to_fun} , + { reflexivity}}, + { apply equiv_of_is_contr_of_is_contr}}, + { apply is_trunc_is_embedding_closed, + { apply is_embedding_to_fun}, + { apply minus_one_le_succ}} end @@ -126,15 +262,15 @@ namespace is_trunc is_set_of_double_neg_elim (λa b, by_contradiction) end - theorem is_trunc_of_axiom_K_of_leq {A : Type} (n : trunc_index) (H : -1 ≤ n) + theorem is_trunc_of_axiom_K_of_le {A : Type} (n : ℕ₋₂) (H : -1 ≤ n) (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A := - @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K)) + @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_le H (λp, eq.rec_on p !K)) theorem is_trunc_succ_of_is_trunc_loop (Hn : -1 ≤ n) (Hp : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A := begin apply is_trunc_succ_intro, intros a a', - apply is_trunc_of_imp_is_trunc_of_leq Hn, intro p, + apply is_trunc_of_imp_is_trunc_of_le Hn, intro p, induction p, apply Hp end @@ -154,7 +290,8 @@ namespace is_trunc { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl}, { apply pi_iff_pi, intro a, esimp, apply is_prop_iff_is_contr, reflexivity}}, { intro A, esimp [iterated_ploop_space], - transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor, + transitivity _, + { apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, apply minus_one_le_succ}, apply pi_iff_pi, intro a, transitivity _, apply IH, transitivity _, apply pi_iff_pi, intro p, rewrite [iterated_loop_space_loop_irrel n p], apply iff.refl, esimp, @@ -178,27 +315,27 @@ namespace is_trunc apply iff.mp !is_trunc_iff_is_contr_loop H end -end is_trunc open is_trunc +end is_trunc open is_trunc is_trunc.trunc_index namespace trunc variable {A : Type} - protected definition code (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type := + protected definition code (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : n-Type := trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a')))) - protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' := + protected definition encode (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' := begin intro p, induction p, induction aa with a, esimp [trunc.code,trunc.rec_on], exact (tr idp) end - protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' := + protected definition decode (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' := begin induction aa' with a', induction aa with a, esimp [trunc.code, trunc.rec_on], intro x, induction x with p, exact ap tr p, end - definition trunc_eq_equiv [constructor] (n : trunc_index) (aa aa' : trunc n.+1 A) + definition trunc_eq_equiv [constructor] (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : aa = aa' ≃ trunc.code n aa aa' := begin fapply equiv.MK, @@ -212,18 +349,18 @@ namespace trunc { intro p, induction p, apply (trunc.rec_on aa), intro a, exact idp}, end - definition tr_eq_tr_equiv [constructor] (n : trunc_index) (a a' : A) + definition tr_eq_tr_equiv [constructor] (n : ℕ₋₂) (a a' : A) : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') := !trunc_eq_equiv definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type) - (n m : trunc_index) [H : is_trunc n A] : is_trunc n (trunc m A) := + (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (trunc m A) := begin revert A m H, eapply (trunc_index.rec_on n), { clear n, intro A m H, apply is_contr_equiv_closed, - { apply equiv.symm, apply trunc_equiv, apply (@is_trunc_of_leq _ -2), exact unit.star} }, + { apply equiv.symm, apply trunc_equiv, apply (@is_trunc_of_le _ -2), apply minus_two_le} }, { clear n, intro n IH A m H, induction m with m, - { apply (@is_trunc_of_leq _ -2), exact unit.star}, + { apply (@is_trunc_of_le _ -2), apply minus_two_le}, { apply is_trunc_succ_intro, intro aa aa', apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_prop)), eapply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_prop)), @@ -238,10 +375,28 @@ namespace trunc !trunc_equiv (f a) /- transport over a truncated family -/ - definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : trunc_index) (x : P a) + definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : ℕ₋₂) (x : P a) : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) := by induction p; reflexivity + definition trunc_trunc_equiv_left [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m) + : trunc n (trunc m A) ≃ trunc n A := + begin + note H2 := is_trunc_of_le (trunc n A) H, + fapply equiv.MK, + { intro x, induction x with x, induction x with x, exact tr x}, + { intro x, induction x with x, exact tr (tr x)}, + { intro x, induction x with x, reflexivity}, + { intro x, induction x with x, induction x with x, reflexivity} + end + + definition trunc_trunc_equiv_right [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m) + : trunc m (trunc n A) ≃ trunc n A := + begin + apply trunc_equiv, + exact is_trunc_of_le _ H, + end + definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥ definition image.mk [constructor] {A B : Type} {f : A → B} {b : B} (a : A) (p : f a = b) @@ -249,13 +404,27 @@ namespace trunc tr (fiber.mk a p) -- truncation of pointed types - definition ptrunc [constructor] (n : trunc_index) (X : Type*) : n-Type* := + definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* := ptrunctype.mk (trunc n X) _ (tr pt) definition ptrunc_functor [constructor] {X Y : Type*} (n : ℕ₋₂) (f : X →* Y) : ptrunc n X →* ptrunc n Y := pmap.mk (trunc_functor n f) (ap tr (respect_pt f)) + definition loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) : + Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) := + pequiv_of_equiv !tr_eq_tr_equiv idp + + definition iterated_loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (k : ℕ) (A : Type*) : + Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) := + begin + revert n, induction k with k IH: intro n, + { reflexivity}, + { refine _ ⬝e* loop_ptrunc_pequiv n (Ω[k] A), + rewrite [iterated_ploop_space_succ], apply loop_pequiv_loop, + refine _ ⬝e* IH (n.+1), + rewrite succ_add_nat} + end end trunc open trunc diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index 4f9df9c1a..0f3129cd1 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -45,7 +45,7 @@ namespace univ definition not_is_set_type : ¬is_set Type.{u} := assume H : is_set Type, - absurd (is_trunc_is_embedding_closed lift star) not_is_set_type0 + absurd (is_trunc_is_embedding_closed lift !trunc_index.minus_one_le_succ) not_is_set_type0 definition not_double_negation_elimination0 : ¬Π(A : Type₀), ¬¬A → A := begin diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index 6664652c5..0f434638a 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -211,7 +211,7 @@ have h₂ : ∀ b, f b = b → a ≤ b, from take b, suppose f b = b, have b ∈ {u | f u ≤ u}, from - show f b ≤ b, by rewrite this; apply le.refl, + show f b ≤ b, by rewrite this, Inf_le this, exists.intro a (and.intro h₁ h₂) @@ -233,7 +233,7 @@ have h₁ : f a = a, from have h₂ : ∀ b, f b = b → b ≤ a, from take b, suppose f b = b, - have b ≤ f b, by rewrite this; apply le.refl, + have b ≤ f b, by rewrite this, le_Sup this, exists.intro a (and.intro h₁ h₂) @@ -266,12 +266,12 @@ lemma Inf_singleton {a : A} : ⨅'{a} = a := have ⨅'{a} ≤ a, from Inf_le !mem_insert, have a ≤ ⨅'{a}, from - le_Inf (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl), + le_Inf (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this), le.antisymm `⨅'{a} ≤ a` `a ≤ ⨅'{a}` lemma Sup_singleton {a : A} : ⨆'{a} = a := have ⨆'{a} ≤ a, from - Sup_le (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this; apply le.refl), + Sup_le (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this), have a ≤ ⨆'{a}, from le_Sup !mem_insert, le.antisymm `⨆'{a} ≤ a` `a ≤ ⨆'{a}` diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 3d722f64a..03adaa6f7 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -20,7 +20,7 @@ structure weak_order [class] (A : Type) extends has_le A := section variables [weak_order A] - theorem le.refl (a : A) : a ≤ a := !weak_order.le_refl + theorem le.refl [refl] (a : A) : a ≤ a := !weak_order.le_refl theorem le_of_eq {a b : A} (H : a = b) : a ≤ b := H ▸ le.refl a @@ -315,13 +315,13 @@ section theorem min_le_left (a b : A) : min a b ≤ a := by_cases - (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply le.refl) + (assume H : a ≤ b, by rewrite [↑min, if_pos H]) (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le_of_lt (lt_of_not_ge H)) theorem min_le_right (a b : A) : min a b ≤ b := by_cases (assume H : a ≤ b, by rewrite [↑min, if_pos H]; apply H) - (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]; apply le.refl) + (assume H : ¬ a ≤ b, by rewrite [↑min, if_neg H]) theorem le_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) : c ≤ min a b := by_cases @@ -331,11 +331,11 @@ section theorem le_max_left (a b : A) : a ≤ max a b := by_cases (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H) - (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le.refl) + (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]) theorem le_max_right (a b : A) : b ≤ max a b := by_cases - (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply le.refl) + (assume H : a ≤ b, by rewrite [↑max, if_pos H]) (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply le_of_lt (lt_of_not_ge H)) theorem max_le {a b c : A} (H₁ : a ≤ c) (H₂ : b ≤ c) : max a b ≤ c := diff --git a/library/algebra/order_bigops.lean b/library/algebra/order_bigops.lean index c9276ce43..9e3c54ab9 100644 --- a/library/algebra/order_bigops.lean +++ b/library/algebra/order_bigops.lean @@ -79,7 +79,7 @@ section decidable_linear_ordered_cancel_comm_monoid_B induction s with a' s' a'nins' ih, {exact false.elim (not_mem_empty a H)}, cases (decidable.em (s' = ∅)) with s'empty s'nempty, - {rewrite [s'empty at *, Max_singleton, eq_of_mem_singleton H], apply le.refl}, + {rewrite [s'empty at *, Max_singleton, eq_of_mem_singleton H]}, rewrite [Max_insert f a'nins' s'nempty], cases (eq_or_mem_of_mem_insert H) with aeqa' ains', {rewrite aeqa', apply le_max_left}, @@ -154,7 +154,7 @@ section decidable_linear_ordered_cancel_comm_monoid_B induction s with a' s' a'nins' ih, {exact false.elim (not_mem_empty a H)}, cases (decidable.em (s' = ∅)) with s'empty s'nempty, - {rewrite [s'empty at *, Min_singleton, eq_of_mem_singleton H], apply le.refl}, + {rewrite [s'empty at *, Min_singleton, eq_of_mem_singleton H]}, rewrite [Min_insert f a'nins' s'nempty], cases (eq_or_mem_of_mem_insert H) with aeqa' ains', {rewrite aeqa', apply min_le_left}, diff --git a/library/algebra/ring_bigops.lean b/library/algebra/ring_bigops.lean index d0ac89458..de64b7963 100644 --- a/library/algebra/ring_bigops.lean +++ b/library/algebra/ring_bigops.lean @@ -82,7 +82,7 @@ section decidable_linear_ordered_comm_group proposition abs_Sum_le (f : A → B) (s : finset A) : abs (∑ x ∈ s, f x) ≤ (∑ x ∈ s, abs (f x)) := begin induction s with a s ans ih, - {rewrite [+Sum_empty, abs_zero], apply le.refl}, + {rewrite [+Sum_empty, abs_zero]}, rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem _ ans], apply le.trans, apply abs_add_le_abs_add_abs, @@ -141,13 +141,12 @@ section ordered_comm_group begin cases (em (finite s)) with fins nfins, {induction fins with a s fins ans ih, - {rewrite +Sum_empty; apply le.refl}, + {rewrite +Sum_empty}, {rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem g ans], have H1 : f a ≤ g a, from H !mem_insert, have H2 : (∑ x ∈ s, f x) ≤ (∑ x ∈ s, g x), from ih (forall_of_forall_insert H), apply add_le_add H1 H2}}, - rewrite [+Sum_of_not_finite nfins], - apply le.refl + rewrite [+Sum_of_not_finite nfins] end proposition Sum_nonneg (f : A → B) {s : set A} (H : ∀₀ x ∈ s, f x ≥ 0) : @@ -171,9 +170,9 @@ section decidable_linear_ordered_comm_group begin cases (em (finite s)) with fins nfins, rotate 1, - {rewrite [+Sum_of_not_finite nfins, abs_zero], apply le.refl}, + {rewrite [+Sum_of_not_finite nfins, abs_zero]}, induction fins with a s fins ans ih, - {rewrite [+Sum_empty, abs_zero], apply le.refl}, + {rewrite [+Sum_empty, abs_zero]}, rewrite [Sum_insert_of_not_mem f ans, Sum_insert_of_not_mem _ ans], apply le.trans, apply abs_add_le_abs_add_abs, diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index c97490fb7..e56255bb6 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -115,7 +115,6 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a apply add_le_add, repeat (apply inv_ge_of_le; apply Hn), krewrite pnat.add_halves, - apply le.refl end theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) : s_abs s ≡ sneg s := @@ -146,7 +145,6 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) : apply add_le_add, repeat (apply inv_ge_of_le; apply Hn), krewrite pnat.add_halves, - apply le.refl, let Hneg' := lt_of_not_ge Hneg, rewrite [abs_of_neg Hneg', ↑sneg, sub_neg_eq_add, neg_add_eq_sub, sub_self, abs_zero], @@ -289,7 +287,6 @@ theorem cauchy_with_rate_of_converges_to_with_rate {X : r_seq} {a : ℝ} {N : xrewrite -of_rat_add, apply of_rat_le_of_rat_of_le, krewrite pnat.add_halves, - apply rat.le_refl end private definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k)) @@ -425,7 +422,6 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li apply Nb_spec_left, rewrite -*pnat.mul_assoc, krewrite pnat.p_add_fractions, - apply rat.le_refl end end lim_seq diff --git a/library/theories/measure_theory/extended_real.lean b/library/theories/measure_theory/extended_real.lean index 524925810..62c353b2c 100644 --- a/library/theories/measure_theory/extended_real.lean +++ b/library/theories/measure_theory/extended_real.lean @@ -330,7 +330,7 @@ theorem neg_infty_le : ∀ v, -∞ ≤ v protected theorem le_refl : ∀ u : ereal, u ≤ u | ∞ := trivial | -∞ := trivial -| (of_real x) := by rewrite [of_real_le_of_real]; apply le.refl +| (of_real x) := by rewrite [of_real_le_of_real] protected theorem le_trans : ∀ u v w : ereal, u ≤ v → v ≤ w → u ≤ w | u v ∞ H1 H2 := !le_infty diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index 7fa1bf85e..4c39391d7 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -229,6 +229,10 @@ order for the change to take effect." ("m=" . ("≞")) ("?=" . ("≟")) + ;; Pointed types in HoTT + ("pequiv" . ("≃*")) + ("phomotopy" . ("~*")) + ("1" . ("₁")) ("2" . ("₂")) ("3" . ("₃")) @@ -338,7 +342,7 @@ order for the change to take effect." ("dot" . ("⬝")) ("sy" . ("⁻¹")) ("inv" . ("⁻¹")) - ("-1" . ("⁻¹")) + ("-1" . ("⁻¹" "₋₁")) ("-1e" . ("⁻¹ᵉ")) ("-1f" . ("⁻¹ᶠ")) ("-1g" . ("⁻¹ᵍ")) @@ -351,7 +355,7 @@ order for the change to take effect." ("-1s" . ("⁻¹ˢ")) ("-1v" . ("⁻¹ᵛ")) ("-1E" . ("⁻¹ᴱ")) - ("-2" . ("⁻²")) + ("-2" . ("⁻²" "₋₂")) ("-2o" . ("⁻²ᵒ")) ("-3" . ("⁻³")) ("qed" . ("∎")) @@ -598,6 +602,7 @@ order for the change to take effect." ("Nat" . ("ℕ")) ("N" . ("ℕ")) ("N-2" . ("ℕ₋₂")) + ("N-1" . ("ℕ₋₁")) ("int" . ("ℤ")) ("Int" . ("ℤ")) ("Z" . ("ℤ"))