michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update after changes in the HoTT library. Mostly some naming and notation changes

Browse source
This commit is contained in:
Floris van Doorn 2016-09-22 16:03:08 -04:00
parent a34606c64f
commit d8c694e113
8 changed files with 103 additions and 93 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
algebra/group_constructions.hlean
View file

@ -165,10 +165,10 @@ namespace group
variable {N}
definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 :=
begin
begin
apply eq_of_rel,
have e : (g * 1⁻¹ = g),
from calc
from calc
g * 1⁻¹ = g * 1 : one_inv
... = g : mul_one,
unfold quotient_rel, rewrite e, exact H
@ -177,18 +177,18 @@ namespace group
definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g :=
begin
have e : (g * 1⁻¹ = g),
from calc
from calc
g * 1⁻¹ = g * 1 : one_inv
... = g : mul_one,
rewrite (inverse e),
apply rel_of_eq _ H
end
apply rel_of_eq _ H
end
definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
begin
fapply homomorphism.mk,
-- define function
{ apply set_quotient.elim f,
{ apply set_quotient.elim f,
intro g h K,
apply eq_of_mul_inv_eq_one,
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
@ -197,8 +197,8 @@ namespace group
... = f g * (f h)⁻¹ : to_respect_inv,
rewrite (inverse e),
apply H, exact K},
{ intro g h, induction g using set_quotient.rec_prop with g,
induction h using set_quotient.rec_prop with h,
{ intro g h, induction g using set_quotient.rec_prop with g,
induction h using set_quotient.rec_prop with h,
krewrite (inverse (to_respect_mul (gq_map N) g h)),
unfold gq_map, esimp, exact to_respect_mul f g h }
end

19
algebra/module.hlean
View file

@ -17,13 +17,26 @@ infixl ` • `:73 := has_scalar.smul
/- modules over a ring -/
structure left_module [class] (R M : Type) [ringR : ring R]
extends has_scalar R M, add_comm_group M :=
structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm_group M renaming
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
mul_left_inv→add_left_inv mul_comm→add_comm :=
(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x)))
(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x)))
(mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
(one_smul : Π x, smul one x = x)
/- we make it a class now (and not as part of the structure) to avoid
left_module.to_comm_group to be an instance -/
attribute left_module [class]
definition add_comm_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
[H : left_module R M] : add_comm_group M :=
@left_module.to_comm_group R M K H
definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
[H : left_module R M] : has_scalar R M :=
@left_module.to_has_scalar R M K H
section left_module
variables {R M : Type}
variable [ringR : ring R]

25
homotopy/EM.hlean
View file

@ -10,7 +10,7 @@ Eilenberg MacLane spaces
import homotopy.EM .spectrum
open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index
fiber prod fin pointed susp EM.ops
fiber prod pointed susp EM.ops
namespace EM
@ -26,7 +26,7 @@ namespace EM
induction n with n IH,
{ exact loop_pequiv_loop (loop_EM2 G)},
refine _ ⬝e* IH,
refine !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !phomotopy_group_pequiv_loop_ptrunc,
refine !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !homotopy_group_pequiv_loop_ptrunc,
apply iterate_psusp_stability_pequiv,
rexact add_mul_le_mul_add n 1 1
end
@ -97,12 +97,12 @@ namespace EM
{ exact pt},
{ exact pt},
change carrier (Ω X), refine f _ _ _ _ _ (tr x),
{ refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply pequiv_of_eq, apply loop_space_succ_eq_in},
{ refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in},
exact abstract begin
intro p q, refine _ ⬝ !r, apply ap e, esimp,
apply inv_tr_eq_of_eq_tr, symmetry,
rewrite [- + ap_inv, - + tr_compose],
refine !loop_space_succ_eq_in_concat ⬝ _, exact !tr_inv_tr ◾ !tr_inv_tr
apply inv_eq_of_eq,
refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹,
exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q
end end
end
@ -172,10 +172,10 @@ namespace EM
-- 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] (ptrunc k (Ω (psusp A))) : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A))
-- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k)
-- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_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)⁻¹ᵉ*
-- ... ≃* π*[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) :
iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) :=
@ -217,9 +217,9 @@ namespace EM
{ exact pcompose f},
{ exact pcompose f⁻¹ᵉ*},
{ intro f, apply pmap_eq_of_phomotopy,
exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_comp},
exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose},
{ intro f, apply pmap_eq_of_phomotopy,
exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_comp}
exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_pcompose}
end
definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) :
@ -228,10 +228,9 @@ namespace EM
revert X Y, induction n with n IH: intro X Y,
{ reflexivity},
{ refine !susp_adjoint_loop ⬝e !IH ⬝e _, apply pmap_equiv_pmap_right,
symmetry, apply pequiv_of_eq, apply loop_space_succ_eq_in}
symmetry, apply loopn_succ_in}
end
end EM
-- cohomology ∥ X → K(G,n) ∥
-- reduced cohomology ∥ X →* K(G,n) ∥

4
homotopy/cohomology.hlean
View file

@ -22,5 +22,5 @@ ordinary_cohomology X agℤ n
notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n
notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n
check H^3[S¹.,EM_spectrum agℤ]
check H^3[S¹.]
check H^3[S¹*,EM_spectrum agℤ]
check H^3[S¹*]

44
homotopy/degree.hlean
View file

@ -29,12 +29,12 @@ namespace sphere
-- unfold [π2S2, chain_complex.LES_of_homotopy_groups],
-- end
check (pmap.to_fun
(chain_complex.cc_to_fn
(chain_complex.LES_of_homotopy_groups
hopf.complex_phopf)
(pair 1 2))
(tr surf))
-- check (pmap.to_fun
-- (chain_complex.cc_to_fn
-- (chain_complex.LES_of_homotopy_groups
-- hopf.complex_phopf)
-- (pair 1 2))
-- (tr surf))
-- eval (pmap.to_fun
-- (chain_complex.cc_to_fn
@ -43,33 +43,31 @@ check (pmap.to_fun
-- (pair 1 2))
-- (tr surf))
-- definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
-- begin
-- cases n with n IH,
-- { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop },
-- { unfold [πnSn], }
-- end
-- set_option pp.all true
definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
begin
cases n with n IH,
{ refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop },
{ unfold [πnSn], exact sorry}
end
exit
definition deg {n : ℕ} [H : is_succ n] (f : S. n →* S. n) : ℤ :=
definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ :=
by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf))
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S. n)) = (1 : ℤ) :=
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) :=
by induction H with n;
exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S. (succ n)) (tr surf)) ⬝ πnSn_surf n
exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n
definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S. n →* S. n} (p : f ~* g) :
definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) :
deg f = deg g :=
begin
induction H with n,
exact ap (πnSn n) (phomotopy_group_functor_phomotopy (succ n) p (tr surf)),
exact ap (πnSn n) (homotopy_group_functor_phomotopy (succ n) p (tr surf)),
end
definition endomorphism_int (f : gℤ →g gℤ) (n : ℤ) : f n = f (1 : ℤ) *[ℤ] n :=
@endomorphism_int_unbundled f (homomorphism.addstruct f) n
definition endomorphism_equiv_Z {i : signature} {X : Group i} (e : X ≃g gℤ) {one : X}
definition endomorphism_equiv_Z {X : Group} (e : X ≃g gℤ) {one : X}
(p : e one = 1 :> ℤ) (φ : X →g X) (x : X) : e (φ x) = e (φ one) *[ℤ] e x :=
begin
revert x, refine equiv_rect' (equiv_of_isomorphism e) _ _,
@ -81,15 +79,15 @@ exit
{ symmetry, exact to_right_inv (equiv_of_isomorphism e) n}
end
definition deg_compose {n : ℕ} [H : is_succ n] (f g : S. n →* S. n) :
definition deg_compose {n : ℕ} [H : is_succ n] (f g : S* n →* S* n) :
deg (g ∘* f) = deg g *[ℤ] deg f :=
begin
induction H with n,
refine ap (πnSn n) (phomotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
refine ap (πnSn n) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g)
end
definition deg_equiv {n : ℕ} [H : is_succ n] (f : S. n ≃* S. n) :
definition deg_equiv {n : ℕ} [H : is_succ n] (f : S* n ≃* S* n) :
deg f = 1 ⊎ deg f = -1 :=
begin
induction H with n,

34
homotopy/spectrum.hlean
View file

@ -130,9 +130,9 @@ namespace spectrum
definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E :=
smap.mk (λn, pid (E n))
(λn, calc glue E n ∘* pid (E n) ~* glue E n : comp_pid
... ~* pid (Ω(E (S n))) ∘* glue E n : pid_comp
... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_id⁻¹*)
(λn, calc glue E n ∘* pid (E n) ~* glue E n : pcompose_pid
... ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose
... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_pid⁻¹*)
definition scompose {N : succ_str} {X Y Z : gen_prespectrum N} (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z :=
smap.mk (λn, g n ∘* f n)
@ -142,7 +142,7 @@ namespace spectrum
... ~* Ω→(to_fun g (S n)) ∘* (glue Y n ∘* to_fun f n) : passoc
... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left Ω→(to_fun g (S n)) (glue_square f n)
... ~* (Ω→(to_fun g (S n)) ∘* Ω→(f (S n))) ∘* glue X n : passoc
... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_compose _ _))
... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_pcompose _ _))
infixr ` ∘ₛ `:60 := scompose
@ -209,7 +209,7 @@ namespace spectrum
-- prespectra too, but as with truncation, why bother?
definition sp_cotensor {N : succ_str} (A : Type*) (B : gen_spectrum N) : gen_spectrum N :=
spectrum.MK (λn, ppmap A (B n))
(λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (equiv_ppcompose_left (equiv_glue B n)))
(λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n)))
----------------------------------------
-- Sections of parametrized spectra
@ -234,11 +234,11 @@ namespace spectrum
intro n, exact sorry
end
definition π_glue (X : spectrum) (n : ℤ) : π*[2] (X (2 - succ n)) ≃* π*[3] (X (2 - n)) :=
definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) :=
begin
refine phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _,
refine homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _,
assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1,
exact pequiv_of_eq (ap (λn, π*[2] (Ω (X n))) H),
exact pequiv_of_eq (ap (λn, π[2] (Ω (X n))) H),
end
definition πg_glue (X : spectrum) (n : ℤ) : πg[1+1] (X (2 - succ n)) ≃g πg[2+1] (X (2 - n)) :=
@ -257,14 +257,14 @@ namespace spectrum
end
definition π_glue_square {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) :
π_glue Y n ∘* π→*[2] (f (2 - succ n)) ~* π→*[3] (f (2 - n)) ∘* π_glue X n :=
π_glue Y n ∘* π→[2] (f (2 - succ n)) ~* π→[3] (f (2 - n)) ∘* π_glue X n :=
begin
refine !passoc ⬝* _,
assert H1 : phomotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→*[2] (f (2 - succ n))
~* π→*[2] (Ω→ (f (succ (2 - succ n)))) ∘* phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)),
{ refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
refine phomotopy_group_functor_phomotopy 2 !sglue_square ⬝* _,
apply phomotopy_group_functor_compose },
assert H1 : homotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→[2] (f (2 - succ n))
~* π→[2] (Ω→ (f (succ (2 - succ n)))) ∘* homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)),
{ refine !homotopy_group_functor_compose⁻¹* ⬝* _,
refine homotopy_group_functor_phomotopy 2 !sglue_square ⬝* _,
apply homotopy_group_functor_compose },
refine pwhisker_left _ H1 ⬝* _, clear H1,
refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
apply pwhisker_right,
@ -314,12 +314,12 @@ namespace spectrum
-- | (n, fin.mk k H) := πₛ[n] (sfiber f)
-- definition shomotopy_groups_fun : Π(n : -3ℤ), shomotopy_groups (S n) →g shomotopy_groups n
-- | (n, fin.mk 0 H) := proof π→g[1+1] (f (n + 2)) qed --π→*[2] f (n+2)
-- | (n, fin.mk 0 H) := proof π→g[1+1] (f (n + 2)) qed --π→[2] f (n+2)
-- --pmap_of_homomorphism (πₛ→[n] f)
-- | (n, fin.mk 1 H) := proof π→g[1+1] (ppoint (f (n + 2))) qed
-- | (n, fin.mk 2 H) :=
-- proof _ ∘g π→g[1+1] equiv_glue Y (pred n + 2) qed
-- --π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n))
-- --π→[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n))
-- | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
end
@ -348,7 +348,7 @@ namespace spectrum
gen_spectrum N :=
gen_spectrum.mk
(mapping_prespectrum X Y)
(is_spectrum.mk (λn, to_is_equiv (equiv_ppcompose_left (equiv_glue Y n) ⬝e
(is_spectrum.mk (λn, to_is_equiv (pequiv_ppcompose_left (equiv_glue Y n) ⬝e
pfunext X (Y (S n)))))
/- Spectrification -/

4
homotopy/spherical_fibrations.hlean
View file

@ -48,10 +48,10 @@ namespace spherical_fibrations
/- classifying type of pointed spherical fibrations -/
definition BF (n : ℕ) : Type₁ :=
Σ(X : Type*), ∥ X ≃* S. n ∥
Σ(X : Type*), ∥ X ≃* S* n ∥
definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) :=
pointed.mk ⟨ S. n , tr pequiv.rfl ⟩
pointed.mk ⟨ S* n , tr pequiv.rfl ⟩
definition pBF [constructor] (n : ℕ) : Type* := pointed.mk' (BF n)

50
move_to_lib.hlean
View file

@ -20,13 +20,13 @@ open sigma
namespace group
open is_trunc
definition pSet_of_Group {i : signature} (G : Group i) : Set* := ptrunctype.mk G _ 1
definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1
definition pmap_of_isomorphism [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j}
definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group}
(φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ :=
pequiv_of_isomorphism φ
definition pequiv_of_isomorphism_of_eq {i : signature} {G₁ G₂ : Group i} (p : G₁ = G₂) :
definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
begin
induction p,
@ -36,7 +36,7 @@ namespace group
{ apply is_prop.elim}
end
definition homomorphism_change_fun [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j}
definition homomorphism_change_fun [constructor] {G₁ G₂ : Group}
(φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ :=
homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h))
@ -128,30 +128,30 @@ namespace pointed
... -/ ≃ (A →* Ω B) : pmap.sigma_char)
(by reflexivity)
definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C :=
pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹))
-- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C :=
-- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹))
definition is_equiv_ppcompose_left [instance] {A B C : Type*} (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 is_equiv_ppcompose_left [instance] {A B C : Type*} (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_pcompose 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_pcompose f }
-- end
definition equiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
pequiv_of_pmap (ppcompose_left g) _
-- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
-- pequiv_of_pmap (ppcompose_left g) _
definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
-- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
-- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
-- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
-- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) :=
phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl
@ -232,7 +232,7 @@ end fiber
namespace eq --algebra.homotopy_group
definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→*[n] (pid A) ~* pid (π*[n] A) :=
definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) :=
ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid
end eq