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

removing errors and warnings

Browse source
This commit is contained in:
Egbert Rijke 2017-07-08 11:43:41 +01:00
parent 6378a34fa6
commit cce49435f6
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
homotopy/spectrum.hlean
View file

@ -599,8 +599,6 @@ set_option pp.coercions true
exact pwhisker_left_refl _ _, exact pwhisker_left_refl _ _,
end end
print ap1_phomotopy_refl
/- homotopy group of a prespectrum -/ /- homotopy group of a prespectrum -/
definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ) definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ)
@ -659,8 +657,6 @@ set_option pp.coercions true
spectrum.MK (λn, Π*a, E a n) spectrum.MK (λn, Π*a, E a n)
(λn, !ppi_loop_pequiv⁻¹ᵉ* ∘*ᵉ ppi_pequiv_right (λa, equiv_glue (E a) n)) (λn, !ppi_loop_pequiv⁻¹ᵉ* ∘*ᵉ ppi_pequiv_right (λa, equiv_glue (E a) n))
print glue_square,
definition spi_compose_left_topsq definition spi_compose_left_topsq
{N : succ_str} {A : Type*} {E F : A → gen_spectrum N} (f : Π a, (E a) →ₛ (F a)) (n : N) {N : succ_str} {A : Type*} {E F : A → gen_spectrum N} (f : Π a, (E a) →ₛ (F a)) (n : N)
: psquare : psquare
@ -682,8 +678,8 @@ set_option pp.coercions true
fapply phomotopy.mk, fapply phomotopy.mk,
intro h, fapply eq_of_ppi_homotopy, intro h, fapply eq_of_ppi_homotopy,
fapply ppi_homotopy.mk, fapply ppi_homotopy.mk,
intro a, reflexivity, -- intro a, reflexivity,
esimp, -- esimp,
repeat exact sorry, repeat exact sorry,
end end