Flattening lemma for sequential colimits

[VojtechStep]

Resolves #869

[fredrik-bakke]

You could call it a 2-cell of morphisms of arrows. Prisms would then be triangles of morphisms of arrows.

[VojtechStep]

Oh right, I think what I want is a htpy-hom-arrow https://unimath.github.io/agda-unimath/foundation.morphisms-arrows.html#homotopies-of-morphsims-of-arrows
(and there's a typo in that heading)

[VojtechStep]

May I just say that rephrasing the whole property from "two coforks with a weird coherence" to "a cofork in the category of morphisms" saved a whole 1 (one!) line, and it's now more conceptual.

Although wrestling the data into shape is a little awkward, so I'll still tweak with it a bit.

[VojtechStep]

I'm pretty happy with the proof, so I'm opening the PR for reviews

[fredrik-bakke]

Here are some initial comments from me. I'll see if I have more detailed comments/comments about the actual code tomorrow. Excellent work! ⭐️

[fredrik-bakke]

Here are some initial comments from me. I'll see if I have more detailed comments/comments about the actual code tomorrow. Excellent work! ⭐️

Apologies, time flew today and now I don't think I will have time to review this today. Maybe I can find a little bit of time tomorrow.

[VojtechStep]

Don't worry about it, it's gonna take some time before I actually need this stuff.

[fredrik-bakke]

Don't worry about it, it's gonna take some time before I actually need this stuff.

I can't help it. 😅 I think this PR is good to merge whenever you are ready.