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

comment out some print statements, fix broken definition

Browse source
This commit is contained in:
Floris van Doorn 2017-07-08 15:49:30 +01:00
parent 0f24cda263
commit 5959ccf2af
2 changed files with 22 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
homotopy/pointed_cubes.hlean
View file

@ -37,14 +37,14 @@ end
definition psquare_of_pid_top_bot {A B : Type*} {fleft : A →* B} {fright : A →* B} (phtpy : fright ~* fleft) : psquare (pid A) (pid B) fleft fright :=
psquare_of_phomotopy ((pcompose_pid fright) ⬝* phtpy ⬝* (pid_pcompose fleft)⁻¹*)
print psquare_of_pid_top_bot
--print psquare_of_pid_top_bot
--λ phtpy, psquare_of_phomotopy ((pid_pcompose fleft) ⬝* phtpy ⬝* ((pcompose_pid fright)⁻¹*))
definition psquare_of_pid_left_right {A B : Type*} {ftop : A →* B} {fbot : A →* B} (phtpy : ftop ~* fbot) : psquare ftop fbot (pid A) (pid B) :=
psquare_of_phomotopy ((pid_pcompose ftop) ⬝* phtpy ⬝* ((pcompose_pid fbot)⁻¹*))
print psquare_of_pid_left_right
--print psquare_of_pid_left_right
definition psquare_hcompose {A B C D E F : Type*} {ftop : A →* B} {fbot : D →* E} {fleft : A →* D} {fright : B →* E} {gtop : B →* C} {gbot : E →* F} {gright : C →* F} (psq_left : psquare ftop fbot fleft fright) (psq_right : psquare gtop gbot fright gright) : psquare (gtop ∘* ftop) (gbot ∘* fbot) fleft gright :=
begin
@ -100,7 +100,7 @@ phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_b
definition ptube_h {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft fleft' : A →* C} (phtpy_left : fleft ~* fleft') {fright fright' : B →* D} (phtpy_right : fright ~* fright') (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop fbot fleft' fright') : Type :=
phsquare (pwhisker_right ftop phtpy_right) (pwhisker_left fbot phtpy_left) psq_back psq_front
print pinv_right_phomotopy_of_phomotopy
--print pinv_right_phomotopy_of_phomotopy
definition psquare_inv_top_bot {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} (psq : psquare ftop fbot fleft fright) : psquare ftop⁻¹ᵉ* fbot⁻¹ᵉ* fright fleft :=
begin
@ -119,7 +119,7 @@ definition p2homotopy_ty_respect_pt {A B : Type*} {f g : A →* B} {H K : f ~* g
induction K with K q, exact q
end
print p2homotopy_ty_respect_pt
--print p2homotopy_ty_respect_pt
structure p2homotopy {A B : Type*} {f g : A →* B} (H K : f ~* g) : Type :=
( to_2htpy : H ~ K)

4
homotopy/strunc.hlean
View file

@ -210,8 +210,8 @@ end
open option
definition is_strunc_add_point_spectrum {X : Type} {Y : X → spectrum} {s₀ : ℤ}
(H : Πx, is_strunc s₀ (Y x)) : Π(x : X₊), is_strunc s₀ (add_point_spectrum Y x)
| (some x) := H x
| none := is_strunc_sunit s₀
| (some x) := proof H x qed
| none := begin intro k, apply is_trunc_lift, apply is_trunc_unit end
definition is_strunc_EM_spectrum (G : AbGroup)
: is_strunc 0 (EM_spectrum G) :=