diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 450e63a4f..dff58db36 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -45,8 +45,8 @@ namespace eq definition fundamental_group [constructor] (A : Type*) : MulGroup := 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 := ghomotopy_group n + notation `πag[`:95 n:0 ` +2]`:0 := cghomotopy_group n notation `π₁` := fundamental_group -- should this be notation for the group or pointed type? @@ -93,30 +93,24 @@ namespace eq definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp - definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] (Ω A) :> Type* := - ap (ptrunc 0) (loop_space_succ_eq_in A n) + definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A ≃* π*[n] (Ω A) := + ptrunc_pequiv_ptrunc 0 (loop_space_succ_in A n) definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp definition phomotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) : - pcast (phomotopy_group_succ_in A (succ n)) (g * h) = - pcast (phomotopy_group_succ_in A (succ n)) g * - pcast (phomotopy_group_succ_in A (succ n)) h := + phomotopy_group_succ_in A (succ n) (g * h) = + phomotopy_group_succ_in A (succ n) g * phomotopy_group_succ_in A (succ n) h := begin induction g with p, induction h with q, esimp, - rewrite [-+ tr_eq_cast_ap, ↑phomotopy_group_succ_in, -+ tr_compose], - refine ap (transport _ _) !tr_mul_tr' ⬝ _, - rewrite [+ trunc_transport], - apply ap tr, apply loop_space_succ_eq_in_concat, + apply ap tr, apply loop_space_succ_in_con end - definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] Ω A := + definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] (Ω A) := begin fapply isomorphism_of_equiv, - { apply equiv_of_eq, exact ap (ptrunc 0) (loop_space_succ_eq_in A (succ n))}, - { exact abstract [irreducible] begin refine trunc.rec _, intro p, refine trunc.rec _, intro q, - rewrite [▸*,-+tr_eq_cast_ap, +trunc_transport], refine !trunc_transport ⬝ _, apply ap tr, - apply loop_space_succ_eq_in_concat end end}, + { exact phomotopy_group_succ_in A (succ n)}, + { exact phomotopy_group_succ_in_con}, end definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) @@ -142,22 +136,20 @@ namespace eq @(is_equiv_trunc_functor 0 _) !is_equiv_apn definition phomotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) : - pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f ~* - π→*[n] (Ω→ f) ∘* pcast (phomotopy_group_succ_in A n) := + phomotopy_group_succ_in B n ∘* π→*[n + 1] f ~* + π→*[n] (Ω→ f) ∘* phomotopy_group_succ_in A n := begin - refine pwhisker_right _ (pcast_ptrunc 0 (loop_space_succ_eq_in B n)) ⬝* _, - refine _ ⬝* pwhisker_left _ (pcast_ptrunc 0 (loop_space_succ_eq_in A n))⁻¹*, refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose, exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) end definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) := - have is_equiv (pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f), + have is_equiv (phomotopy_group_succ_in B n ∘* π→*[n + 1] f), from is_equiv_compose _ (π→*[n + 1] f), - have is_equiv (π→*[n] (Ω→ f) ∘ pcast (phomotopy_group_succ_in A n)), + have is_equiv (π→*[n] (Ω→ f) ∘ phomotopy_group_succ_in A n), from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f), - is_equiv.cancel_right (pcast (phomotopy_group_succ_in A n)) _ + is_equiv.cancel_right (phomotopy_group_succ_in A n) _ definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X := ptrunc_functor 0 pinverse @@ -204,7 +196,7 @@ namespace eq { reflexivity}, { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _, apply homotopy_group_isomorphism_of_pequiv, - exact pequiv_of_eq !loop_space_succ_eq_in⁻¹} + exact !loop_space_succ_in⁻¹ᵉ*} end theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) @@ -249,22 +241,19 @@ namespace eq /- some homomorphisms -/ - definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : - is_homomorphism - (cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n))) - : πg[n+1+1] A → πg[n+1] Ω A) := - begin - intro g h, induction g with g, induction h with h, - xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose, - loop_space_succ_eq_in_concat, - + tr_compose], - end + -- definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) : + -- is_homomorphism (loop_space_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) := + -- begin + -- intro g h, induction g with g, induction h with h, + -- xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose, + -- loop_space_succ_eq_in_concat, - + tr_compose], + -- end + local attribute MulGroup MulCommGroup [reducible] definition is_homomorphism_inverse (A : Type*) (n : ℕ) - : is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) := + : is_homomorphism (λp, p⁻¹ : (πag[n+2] A) → (πag[n+2] A)) := begin - intro g h, rewrite mul.comm, - induction g with g, induction h with h, - exact ap tr !con_inv + intro g h, exact ap inv (mul.comm g h) ⬝ mul_inv h g, end notation `π→g[`:95 n:0 ` +1]`:0 := homotopy_group_homomorphism n diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index b99f06ccc..39b935098 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -485,7 +485,7 @@ namespace chain_complex definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed - | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* pcast (loop_space_succ_eq_in Y n) qed + | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loop_space_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2) @@ -501,12 +501,7 @@ namespace chain_complex definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2) : loop_spaces_fun2 (n+1, fin.mk 2 H) ~* cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) := - begin - esimp, - refine _ ⬝* !ap1_compose⁻¹*, - apply pwhisker_left, - apply pcast_ap_loop_space - end + proof !ap1_compose⁻¹* qed definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ := λx, succ n * pr1 x + val (pr2 x) @@ -651,7 +646,7 @@ namespace chain_complex | (n, fin.mk 0 H) := proof π→*[n] f qed | (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed | (n, fin.mk 2 H) := - proof π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) qed + proof π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible] @@ -662,8 +657,7 @@ namespace chain_complex | (n, fin.mk 2 H) := begin refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*, - refine !ptrunc_functor_pcompose ⬝* _, - apply pwhisker_left, apply ptrunc_functor_pcast, + refine !ptrunc_functor_pcompose end | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end @@ -710,7 +704,7 @@ namespace chain_complex cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) := by reflexivity definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) = - π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) := + π→*[n] boundary_map ∘* phomotopy_group_succ_in Y n := by reflexivity open group @@ -749,10 +743,8 @@ namespace chain_complex begin apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)), exact abstract begin rewrite [LES_of_homotopy_groups_fun_2], - refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[k + 1] boundary_map) _ _ _, - { apply phomotopy_group_functor_mul}, - { rewrite [▸*, -ap_compose', ▸*], - apply is_homomorphism_cast_loop_space_succ_eq_in} end end + refine homomorphism.struct ((π→g[k+1] boundary_map) ∘g ghomotopy_group_succ_in Y k), + end end end | (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end @@ -781,7 +773,7 @@ namespace chain_complex : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n | (n, fin.mk 0 H) := proof Ω→[n] f qed | (n, fin.mk 1 H) := proof Ω→[n] g qed - | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* pcast (loop_space_succ_eq_in Y n) qed + | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loop_space_succ_in Y n qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition fibration_sequence_pequiv : Π(x : +3ℕ), diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index 6e535f8a0..b12793f26 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -176,7 +176,7 @@ freudenthal_pequiv A H definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) : π*[k + 1] (psusp A) ≃* π*[k] A := calc - π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (phomotopy_group_succ_in (psusp A) k) + π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : phomotopy_group_succ_in (psusp A) k ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 51c471885..fcc08220d 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -270,20 +270,20 @@ namespace sphere apply add_one_sub_one end - - definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) := - pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv + definition equator [constructor] (n : ℕ) : S. n →* Ω (S. (succ n)) := + loop_susp_unit (S. n) definition surf {n : ℕ} : Ω[n] S. n := - nat.rec_on n (proof @base 0 qed) - (begin intro m s, refine cast _ (apn m (equator m) s), - exact ap carrier !loop_space_succ_eq_in⁻¹ end) + begin + induction n with n s, + { exact @base 0}, + { exact (loop_space_succ_in (S. (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), } + end - - definition bool_of_sphere : S 0 → bool := + definition bool_of_sphere [unfold 1] : S 0 → bool := proof susp.rec ff tt (λx, empty.elim x) qed - definition sphere_of_bool : bool → S 0 + definition sphere_of_bool [unfold 1] : bool → S 0 | ff := proof north qed | tt := proof south qed @@ -293,21 +293,24 @@ namespace sphere (λb, match b with | tt := idp | ff := idp end) (λx, proof susp.rec_on x idp idp (empty.rec _) qed) + definition psphere_pequiv_pbool : S. 0 ≃* pbool := + pequiv_of_equiv sphere_equiv_bool idp + definition sphere_eq_bool : S 0 = bool := ua sphere_equiv_bool definition sphere_eq_pbool : S. 0 = pbool := pType_eq sphere_equiv_bool idp - -- TODO1: the commented-out part makes the forward function below "apn _ surf" + -- TODO1: the commented-out part makes the forward function below "apn _ surf" (the next def also) -- TODO2: we could make this a pointed equivalence - definition pmap_sphere (A : Type*) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A := + definition pmap_sphere (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A := begin -- fapply equiv_change_fun, -- { revert A, induction n with n IH: intro A, - { 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]} + { refine _ ⬝e !pmap_bool_equiv, exact equiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ*}, + { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e !loop_space_succ_in⁻¹ᵉ* } -- }, -- { intro f, exact apn n f surf}, -- { revert A, induction n with n IH: intro A f, @@ -315,7 +318,19 @@ namespace sphere -- { exact sorry}} end - protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : map₊ (S. n) P := + -- definition pmap_sphere' (A : Type*) (n : ℕ) : (S. n →* A) ≃ Ω[n] A := + -- begin + -- fapply equiv.MK, + -- { intro f, exact apn n f surf }, + -- { revert A, induction n with n IH: intro A p, + -- { exact !pmap_bool_equiv⁻¹ᵉ p ∘* psphere_pequiv_pbool }, + -- { refine (susp_adjoint_loop (S. n) A)⁻¹ᵉ (IH (Ω A) _), + -- exact loop_space_succ_in A n p }}, + -- { exact sorry}, + -- { exact sorry} + -- end + + protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S. n →* P := to_inv !pmap_sphere p -- definition elim_surf {n : ℕ} {P : Type*} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := @@ -350,7 +365,7 @@ namespace is_trunc open trunc_index variables {n : ℕ} {A : Type} definition is_trunc_of_pmap_sphere_constant - (H : Π(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n), f x = f base) : is_trunc (n.-2.+1) A := + (H : Π(a : A) (f : S. n →* pointed.Mk a) (x : S n), f x = f base) : is_trunc (n.-2.+1) A := begin apply iff.elim_right !is_trunc_iff_is_contr_loop, intro a, @@ -370,7 +385,7 @@ namespace is_trunc end definition pmap_sphere_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A] - (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base := + (a : A) (f : S. n →* pointed.Mk a) (x : S n) : f x = f base := begin let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a, note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H', @@ -380,7 +395,7 @@ namespace is_trunc end definition pmap_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] - (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x y : S n) : f x = f y := + (a : A) (f : S. n →* pointed.Mk a) (x y : S n) : f x = f y := let H := pmap_sphere_constant_of_is_trunc' a f in !H ⬝ !H⁻¹ definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index d928943ad..5f6b417a4 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -104,55 +104,6 @@ namespace pointed definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (A : n-Type*) : is_trunc n A := trunctype.struct A - /- properties of iterated loop space -/ - variable (A : Type*) - definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) := - begin - induction n with n IH, - { reflexivity}, - { exact ap ploop_space IH} - end - - definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) := - begin - induction n with n IH, - { reflexivity}, - { exact ap ploop_space IH} - end - - definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A) := - idp - - variable {A} - - /- the equality [loop_space_succ_eq_in] preserves concatenation -/ - theorem loop_space_succ_eq_in_concat {n : ℕ} (p q : Ω[succ (succ n)] A) : - transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) (p ⬝ q) - = transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) p - ⬝ transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) q := - begin - rewrite [-+tr_compose, ↑function.compose], - rewrite [+@transport_eq_FlFr_D _ _ _ _ Point Point, +con.assoc], apply whisker_left, - rewrite [-+con.assoc], apply whisker_right, rewrite [con_inv_cancel_right, ▸*, -ap_con] - end - - definition loop_space_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := - begin - intros, fapply pType_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 :> pType := - 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 : by rewrite [algebra.add.comm] - end pointed open pointed namespace pointed @@ -496,18 +447,6 @@ namespace pointed { induction p, reflexivity} end - definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : - pcast (loop_space_succ_eq_in B n) ∘* Ω→[n + 1] f ~* - Ω→[n] (Ω→ f) ∘* pcast (loop_space_succ_eq_in A n) := - begin - induction n with n IH, - { reflexivity}, - { refine pwhisker_right _ (pcast_loop_space (loop_space_succ_eq_in B n)) ⬝* _, - refine _ ⬝* pwhisker_left _ (pcast_loop_space (loop_space_succ_eq_in A n))⁻¹*, - refine (ap1_compose _ (Ω→[n + 1] f))⁻¹* ⬝* _ ⬝* ap1_compose (Ω→[n] (Ω→ f)) _, - exact ap1_phomotopy IH} - end - definition ap1_pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) : ap1 (pmap_of_map f a) ~* pmap_of_map (ap f) (idpath a) := begin @@ -812,4 +751,100 @@ namespace pointed end end -/ + /- properties of iterated loop space -/ + variable (A) + definition loop_space_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) := + begin + induction n with n IH, + { reflexivity}, + { exact loop_pequiv_loop IH} + end + + definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) := + begin + induction n with n IH, + { reflexivity}, + { exact loop_pequiv_loop IH} + end + + definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A) := + by reflexivity + + variable {A} + + theorem loop_space_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) : + loop_space_succ_in A (succ n) (p ⬝ q) = + loop_space_succ_in A (succ n) p ⬝ loop_space_succ_in A (succ n) q := + !loop_pequiv_loop_con + + definition loop_space_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := + begin + intros, fapply pType_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 :> pType := + calc + Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : eq_of_pequiv !loop_space_succ_in + ... = Ω[n] (Ω[2] A) : loop_space_loop_irrel + ... = Ω[2+n] A : eq_of_pequiv !loop_space_add + ... = Ω[n+2] A : by rewrite [algebra.add.comm] + + definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : + loop_space_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loop_space_succ_in A n := + begin + induction n with n IH, + { reflexivity}, + { exact !ap1_compose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_compose} + end + + definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C := + pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, respect_pt g) (idp_con _)⁻¹)) + + definition is_equiv_ppcompose_left [instance] [constructor] (g : B →* C) [H : is_equiv g] : + is_equiv (@ppcompose_left A B C g) := + begin + fapply is_equiv.adjointify, + { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, + all_goals (intros f; esimp; apply eq_of_phomotopy), + { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc + ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) + ... ~* f : pid_comp f }, + { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc + ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) + ... ~* f : pid_comp f } + end + + definition equiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C := + pequiv_of_pmap (ppcompose_left g) _ + + definition pcompose_pconst [constructor] (f : B →* C) : f ∘* pconst A B ~* pconst A C := + phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ + + definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C := + phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ + + definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C := + begin + fconstructor, + { intro g, exact g ∘* f }, + { apply eq_of_phomotopy, esimp, apply pconst_pcompose } + end + + definition equiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C := + begin + fapply pequiv.MK, + { exact ppcompose_right f }, + { exact ppcompose_right f⁻¹ᵉ* }, + { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, + refine pwhisker_left g !pright_inv ⬝* !comp_pid, }, + { intro g, apply eq_of_phomotopy, refine !passoc ⬝* _, + refine pwhisker_left g !pleft_inv ⬝* !comp_pid, }, + end + + end pointed