Eckmann-Hilton in the Universe

[morphismz]

This pr formalizes most of the "Eckmann-Hilton in the universe" idea, thus bringing partial completion to one of the task on the issue "Formalize the Hopf Fibration" ( #702 ).

The main theorem of the pr, named tr³-htpy-swap-path-swap, establishes that tr³ sends path-swap to htpy-swap.

[morphismz]

I'm having trouble with the pre-commit tool. Its throwing an error, but I can't tell whats causing it.

[EgbertRijke]

I'm having trouble with the pre-commit tool. Its throwing an error, but I can't tell whats causing it.

Can you show us the output of make pre-commit?

[morphismz]

I'm having trouble with the pre-commit tool. Its throwing an error, but I can't tell whats causing it.

Can you show us the output of make pre-commit?

Here is the out put:

I ran pre-commit back to back, so this shows the output of two different runs. Maybe I'm just not reading the out put right...

[morphismz]

I might also be formatting concatenation of paths wrong, let me work on that

[EgbertRijke]

Ah, it is not telling us which files were modified. @fredrik-bakke, do you think it would be better if it told us which files were modified?

One trick to see which files are being modified is to commit all your changes, then run make pre-commit and see from the git logs which files are being modified/problematic.

[VojtechStep]

I think the offender is printed at the end of the log, and it's the transport file. I see that one of the code blocks is missing the language declaration (i.e. it starts with just triple backticks, without agda), which probably breaks Fredrik's parser, I remember it being sensitive to that stuff.

[morphismz]

I think the offender is printed at the end of the log, and it's the transport file. I see that one of the code blocks is missing the language declaration (i.e. it starts with just triple backticks, without agda), which probably breaks Fredrik's parser, I remember it being sensitive to that stuff.

great catch, I'll fix that and see what happens. Maybe there is way for the parser to report back that a code block is set up right?

Edit: Cool, that fixed it! Sorry about that 🙃

[fredrik-bakke]

Ah, it is not telling us which files were modified. @fredrik-bakke, do you think it would be better if it told us which files were modified?

One trick to see which files are being modified is to commit all your changes, then run make pre-commit and see from the git logs which files are being modified/problematic.

I totally agree that it should display which files are modified, but as far as I can recall, there didn't seem to be a way to make pre-commit do that. If any of you know of a way, that would be greatly appreciated!

[VojtechStep]

In May you wrote

So one of my pre-commit scripts doesn't accept unspecified code blocks. So far, that has only ever been due to typos. But if text works, that would be great

on the Discord, which I interpreted as "it breaks on unspecified code blocks", but if it intentionally rejects them, then that's great 👌

[fredrik-bakke]

In May you wrote

So one of my pre-commit scripts doesn't accept unspecified code blocks. So far, that has only ever been due to typos. But if text works, that would be great

on the Discord, which I interpreted as "it breaks on unspecified code blocks", but if it intentionally rejects them, then that's great 👌

Aha, I guess I should've said "rejects". Sorry about that!

[VojtechStep]

Wait, but then "Markdown conventions", which checks for well-formatted code blocks, should have triggered, right? Which it didn't?

[fredrik-bakke]

Ah, that confused me too. I'll look into that!

[fredrik-bakke]

It's unclear to me where we draw the line between what's foundational and what's synthetic homotopy theory. I think you could make an argument for placing the Eckmann-Hilton argument in either, but I'd assume users of the library would look in synthetic-homotopy-theory first. Do you have any opinion on this, @EgbertRijke? Also, do we want Eckmann-Hilton in its own file?

[fredrik-bakke]

By the way, you can link to your issue using its issue number, i.e. #702. GitHub will then place links in the appropriate places so that things get nicely catalogued. :) Also, if you write "closes #XYZ" or "resolves #XYZ", the appropriate issue will be closed when that PR is merged.

[morphismz]

It's unclear to me where we draw the line between what's foundational and what's synthetic homotopy theory. I think you could make an argument for placing the Eckmann-Hilton argument in either, but I'd assume users of the library would look in synthetic-homotopy-theory first. Do you have any opinion on this, @EgbertRijke? Also, do we want Eckmann-Hilton in its own file?

I'm all for Eckmann-Hilton getting its own file! I just put this stuff in path algebra, since it seems vaguely related and there was no file with a more direct relation.

[morphismz]

@fredrik-bakke I believe I have implemented all suggestions, except the one about putting this code in foundation vs. synthetic homotopy theory, since I wasn't sure if this was a suggestion, or a question

[fredrik-bakke]

Things seem to be mostly in order now, but I made a couple of additional suggestions. Also, let's wait for Egbert's input before merging. Or do you want this merged as soon as possible?

[morphismz]

Things seem to be mostly in order now, but I made a couple of additional suggestions. Also, let's wait for Egbert's input before merging. Or do you want this merged as soon as possible?

No rush on my end, happy to get more feedback first!

[fredrik-bakke]

Alright, I think we've waited long enough. If we want to move Eckmann-Hilton, we can do so at a later point. I will merge this PR when the checks pass. Thanks again for these contributions, I'm excited for all the new additions to synthetic-homotopy-theory! :)

(I've checked that there are no broken links)