-
Notifications
You must be signed in to change notification settings - Fork 59
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Change the inductive definition of iterative loop spaces? #37
Comments
I have no objection to that change. I believe I chose the other one just because I had no idea which one was better and I had to choose one. |
Compare, for example, HoTT-Agda/core/lib/groups/HomotopyGroup.agda Lines 64 to 103 in 159df93
HoTT-Agda/core/lib/groups/HomotopyGroup.agda Lines 107 to 113 in 159df93
|
@favonia asked me to comment. In Lean we use the definition of Actually, long ago we did use the other definition where |
@fpvandoorn Thanks for the comment. I have done the concatenation and lemmas about it, and felt they are fine once you get used to the induction from Right now the alternative concatenation is defined as HoTT-Agda/core/lib/types/LoopSpace.agda Lines 278 to 280 in 159df93
HoTT-Agda/core/lib/types/LoopSpace.agda Lines 351 to 356 in 159df93
|
@fpvandoorn I think my main point is that we do not seem to need any |
Closing this as there's nothing to do. We have two versions now. |
Experience shows that, at least for homotopy groups,
⊙Ω^ (S n) X
should be⊙Ω^ n (⊙Ω X)
, not⊙Ω (⊙Ω^ n X)
.The text was updated successfully, but these errors were encountered: