begin work on some homotopy coherences

[jonalfcam]

In the course of proving 9.10 I ran into a small part of the proof that needs more homotopy coherences than I originally thought. I've begun putting in the ones that I need, but I figure it would be a good thing to leave most of the groupoidal structure for homotopies to someone as a first issue. What doe you think @emilyriehl @fizruk ?

I also added a dependent homotopy type, which as far as I could tell was not in there? Of course one can get away with $\lambda$-abstraction, but I found using this easier to read when working with homotopies between homotopies.

[jonalfcam]

As a side issue about documentation, the little lemma I need to prove is absolutely unparseable with a commutative diagram or some diagram accompanying it . Is there a way to include those?

[fizruk]

As a side issue about documentation, the little lemma I need to prove is absolutely unparseable with a commutative diagram or some diagram accompanying it . Is there a way to include those?

There should be a way to enable amscd package for MathJax, but I haven't yet figured out the settings. I will let you know when I have a working example.

Otherwise, we could attach pictures :)

[jonalfcam]

As a side issue about documentation, the little lemma I need to prove is absolutely unparseable with a commutative diagram or some diagram accompanying it . Is there a way to include those?

There should be a way to enable amscd package for MathJax, but I haven't yet figured out the settings. I will let you know when I have a working example.

Otherwise, we could attach pictures :)

I’m happy to generate svg commutative diagrams! Just wanted to make sure it would be ok.

[fizruk]

As a side issue about documentation, the little lemma I need to prove is absolutely unparseable with a commutative diagram or some diagram accompanying it . Is there a way to include those?

There should be a way to enable amscd package for MathJax, but I haven't yet figured out the settings. I will let you know when I have a working example.
Otherwise, we could attach pictures :)

I’m happy to generate svg commutative diagrams! Just wanted to make sure it would be ok.

Yes, I believe it is okay to generate and add SVG commutative diagrams :)

[jonalfcam]

Added a commutative diagram. It would maybe be nice to have a way to collapse these things in vscode? I have no idea how that works.

[fizruk]

Added a commutative diagram. It would maybe be nice to have a way to collapse these things in vscode? I have no idea how that works.

If you indent the contents of <svg>, then you would be able to fold it by clicking the button to the left of <svg> tag:

[jonalfcam]

Haha. Fantastic! I'm sorry for not knowing such an easy fix!

[fredrik-bakke]

Sorry, here are some corrections on formatting as well.

By the way, are you planning on doing the refactoring of homotopies in this PR, or some other work? If so, it would be helpful if you marked it as a draft so it's easier for us to spot that it is unfinished.

[jonalfcam]

I have finished with the homotopy coherence I wanted to work on. @fredrik-bakke if it is ok, I will update the homotopy and dependent-homotopy in a PR of its own. Also, thank you for recommending the rainbow-indent plugin!

[fredrik-bakke]

I have finished with the homotopy coherence I wanted to work on. @fredrik-bakke if it is ok, I will update the homotopy and dependent-homotopy in a PR of its own. Also, thank you for recommending the rainbow-indent plugin!

That's fine! Maybe just rename dependent-homotopy to dhomotopy for now, so as not to keep the misleading name for it. And I'm glad the plugin was useful to you :)

[jonalfcam]

That's fine! Maybe just rename dependent-homotopy to dhomotopy for now, so as not to keep the misleading name for it. And I'm glad the plugin was useful to you :)

Great! I'm made the change.

[emilyriehl]

I'm a bit slow to join this. It looks like this is ready to merge. Any outstanding issues I'm not aware of?

[fredrik-bakke]

There is still some formatting that could be improved in this contribution, but I will no longer comment on those. No offense meant to anyone, this is purely to preserve my own sanity and time.

Also, it should be checked that the diagrams render properly on the website. The correct approach would be to build the website locally and check it on your computer before the PR is merged. But I won't tell on anyone if the PR is merged and the diagrams are checked on the live webpage.

[fredrik-bakke]

Please let us know when you have addressed the comments, Jonathan

[emilyriehl]

@jonalfcam I see one unresolved conversation (where @fredrik-bakke suggested a potential simplification in the proof, which in any case is over-indented).

I have one other suggestion: throughout the sHoTT library it is more common to write markdown comments using code blocks than LaTeX (with the exception being cases where the code blocks are excessively ugly). Would you mind making this change where practical?

[jonalfcam]

@jonalfcam I see one unresolved conversation (where @fredrik-bakke suggested a potential simplification in the proof, which in any case is over-indented).

I have one other suggestion: throughout the sHoTT library it is more common to write markdown comments using code blocks than LaTeX (with the exception being cases where the code blocks are excessively ugly). Would you mind making this change where practical?

Ah, my two great fondnesses: over-indentation and LaTeX. Just so I understand: the preference is for writing code rather than math in explanations? Are commutative diagrams still ok?

[jonalfcam]

I might advocate for leaving some of the LaTeX in the coherences section. The idea behind including it was to explain some of the construction, and it seems appropriate for that. If we prefer not to have any LaTeX in the documentation, maybe we can revisit the zulip discussion about this.

[jonalfcam]

I think otherwise, everything is resolved now!

[emilyriehl]

I might advocate for leaving some of the LaTeX in the coherences section. The idea behind including it was to explain some of the construction, and it seems appropriate for that. If we prefer not to have any LaTeX in the documentation, maybe we can revisit the zulip discussion about this.

Great idea to discuss this there. I'll merge now.