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!

[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]

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.