From 47be1e3a157045377a360900aa99a41027f0fd96 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 13 Nov 2015 17:17:02 -0500 Subject: [PATCH] feat(types/pointed): change definition of loop space --- hott/homotopy/sphere.hlean | 22 ++++++++--- hott/init/equiv.hlean | 2 +- hott/init/logic.hlean | 3 ++ hott/init/trunc.hlean | 1 + hott/types/pointed.hlean | 75 +++++++++++++++++++++++++++----------- hott/types/trunc.hlean | 32 +++++++--------- 6 files changed, 89 insertions(+), 46 deletions(-) diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 7a017857d..9fad2bb99 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -98,8 +98,10 @@ namespace sphere pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv definition surf {n : ℕ} : Ω[n] S. n := - nat.rec_on n (by esimp [Iterated_loop_space]; exact base) - (by intro n s;exact apn n (equator n) s) + nat.rec_on n (proof base qed) + (begin intro m s, refine cast _ (apn m (equator m) s), + exact ap Pointed.carrier !loop_space_succ_eq_in⁻¹ end) + definition bool_of_sphere : S 0 → bool := susp.rec ff tt (λx, empty.elim x) @@ -120,12 +122,20 @@ namespace sphere definition sphere_eq_bool_pointed : S. 0 = Bool := Pointed_eq sphere_equiv_bool idp + -- TODO: the commented-out part makes the forward function below "apn _ surf" definition pmap_sphere (A : Pointed) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A := begin - revert A, induction n with n IH, - { intro A, rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv}, - { intro A, transitivity _, apply susp_adjoint_loop (S. n) A, apply IH} - end -- can we prove this in such a way that the function from left to right is apn _ surf? + -- fapply equiv_change_fun, + -- { + revert A, induction n with n IH: intro A, + { rewrite [sphere_eq_bool_pointed], 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}, + -- { revert A, induction n with n IH: intro A f, + -- { exact sorry}, + -- { exact sorry}} + end protected definition elim {n : ℕ} {P : Pointed} (p : Ω[n] P) : map₊ (S. n) P := to_inv !pmap_sphere p diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 29b698a03..d8cdd9196 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -287,7 +287,7 @@ namespace equiv protected definition trans [trans] (f : A ≃ B) (g : B ≃ C) : A ≃ C := equiv.mk (g ∘ f) !is_equiv_compose - infixl `⬝e`:75 := equiv.trans + infixl ` ⬝e `:75 := equiv.trans postfix [parsing_only] `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded abbreviation erfl [constructor] := @equiv.refl diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index f1d9a16ac..d3de7fecd 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -181,6 +181,9 @@ namespace iff definition rfl {a : Type} : a ↔ a := refl a + definition iff_of_eq (a b : Type) (p : a = b) : a ↔ b := + eq.rec rfl p + definition trans (H₁ : a ↔ b) (H₂ : b ↔ c) : a ↔ c := intro (assume Ha, elim_left H₂ (elim_left H₁ Ha)) diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 84637b4d2..ea2c877b4 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -49,6 +49,7 @@ namespace is_trunc definition succ_le_succ {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := H 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 := diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index c9f535394..17b064e03 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -6,7 +6,7 @@ Authors: Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ -import arity .eq .bool .unit .sigma +import arity .eq .bool .unit .sigma .nat.basic open is_trunc eq prod sigma nat equiv option is_equiv bool unit structure pointed [class] (A : Type) := @@ -66,12 +66,9 @@ namespace pointed definition Loop_space [reducible] [constructor] (A : Type*) : Type* := pointed.mk' (point A = point A) - -- definition Iterated_loop_space : Type* → ℕ → Type* - -- | Iterated_loop_space A 0 := A - -- | Iterated_loop_space A (n+1) := Iterated_loop_space (Loop_space A) n - - definition Iterated_loop_space [unfold 1] [reducible] (n : ℕ) (A : Type*) : Type* := - nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A + definition Iterated_loop_space [unfold 1] [reducible] : ℕ → Type* → Type* + | Iterated_loop_space 0 X := X + | Iterated_loop_space (n+1) X := Loop_space (Iterated_loop_space n X) prefix `Ω`:(max+5) := Loop_space notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A @@ -183,12 +180,6 @@ namespace pointed { esimp, exact !con.left_inv⁻¹}}, end - -- definition Loop_space_functor (f : A →* B) : Ω A →* Ω B := - -- begin - -- fapply pmap.mk, - -- { intro p, exact ap f p}, - -- end - -- set_option pp.notation false -- definition pmap_equiv_right (A : Type*) (B : Type) -- : (Σ(b : B), map₊ A (pointed.Mk b)) ≃ (A → B) := @@ -217,17 +208,59 @@ namespace pointed { esimp, exact !con.left_inv⁻¹}}, end - definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := + definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := begin - revert A B f, induction n with n IH, - { intros A B f, exact f}, - { intros A B f, esimp, apply IH (Ω A), - { esimp, fconstructor, - intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt, - esimp, apply con.left_inv}} + fconstructor, + { intro p, exact !respect_pt⁻¹ ⬝ ap f p ⬝ !respect_pt}, + { esimp, apply con.left_inv} end - definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := apn (succ 0) f + definition apn [unfold 3] (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B := + begin + induction n with n IH, + { exact f}, + { esimp [Iterated_loop_space], exact ap1 IH} + end + + variable (A) + definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) := + begin + induction n with n IH, + { reflexivity}, + { exact ap Loop_space IH} + end + + definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) := + begin + induction n with n IH, + { reflexivity}, + { exact ap Loop_space IH} + end + + definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A) := + idp + + variable {A} + definition loop_space_loop_irrel (p : point A = point A) : Ω(Pointed.mk p) = Ω[2] A := + begin + intros, fapply Pointed_eq, + { esimp, transitivity _, + apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹), + esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv}, + { esimp, apply con.left_inv} + end + + definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A) + : Ω[succ n](Pointed.mk p) = Ω[succ (succ n)] A :> Pointed := + calc + Ω[succ n](Pointed.mk p) = Ω[n](Ω (Pointed.mk p)) : loop_space_succ_eq_in + ... = Ω[n] (Ω[2] A) : loop_space_loop_irrel + ... = Ω[2+n] A : loop_space_add + ... = Ω[n+2] A : add.comm + + -- 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 diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index c8a17fc4b..9c4a85448 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -138,31 +138,27 @@ namespace is_trunc induction p, apply Hp end + theorem is_hprop_iff_is_contr {A : Type} (a : A) : + is_hprop A ↔ is_contr A := + iff.intro (λH, is_contr.mk a (is_hprop.elim a)) _ + theorem is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) : is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) := iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn) - +--set_option pp.all true theorem is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type) : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](Pointed.mk a)) := begin revert A, induction n with n IH, - { intros, esimp [Iterated_loop_space], apply iff.intro, - { intros H a, apply is_contr.mk idp, apply is_hprop.elim}, - { intro H, apply is_hset_of_axiom_K, intros, apply is_hprop.elim}}, - { intros, transitivity _, apply @is_trunc_succ_iff_is_trunc_loop n, constructor, - apply iff.pi_iff_pi, intros, - transitivity _, apply IH, - assert H : Πp : a = a, Ω(Pointed.mk p) = Ω(Pointed.mk (idpath a)), - { intros, fapply Pointed_eq, - { esimp, transitivity _, - apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹), - esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv}, - { esimp, apply con.left_inv}}, - transitivity _, - apply iff.pi_iff_pi, intro p, - rewrite [↑Iterated_loop_space,H], - apply iff.refl, - apply iff.imp_iff, reflexivity} + { intro A, esimp [Iterated_loop_space], transitivity _, + { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl}, + { apply iff.pi_iff_pi, intro a, esimp, apply is_hprop_iff_is_contr, reflexivity}}, + { intro A, esimp [Iterated_loop_space], + transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor, + apply iff.pi_iff_pi, intro a, transitivity _, apply IH, + transitivity _, apply iff.pi_iff_pi, intro p, + rewrite [iterated_loop_space_loop_irrel n p], apply iff.refl, esimp, + apply iff.imp_iff, reflexivity} end theorem is_trunc_iff_is_contr_loop (n : ℕ) (A : Type)