search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Vertical calculus for homotopy cartesian squares #59

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Establish vertical pasting and cancellation laws for homotopy cartesian squares.

Additionally to the two standard laws (lower cancellation and pasting), I also formalized a statement allowing upper cancellation in the case where the upper square has a section.

I plan to use these laws to formalize the "category theoretic proof" of RS17, Theorem 8.8. This is in parallel with Cesar's #58, who will formalize the "type theoretic proof".

EDIT: I separated out the separate pull-request #61 which is minor and can be merged independently.

emilyriehl commented 1 year ago

Hi @TashiWalde I just pushed a few cosmetic edits.

You had one function defined by a λ abstraction \ a' -> f (a ') that is now just f.

All the other edits involved collapsing end parentheses to the end of the last line: collected like this))). This is our usual style.

If this all looks okay to you, I'll go ahead and merge this one.

TashiWalde commented 1 year ago

Hi @TashiWalde I just pushed a few cosmetic edits.

You had one function defined by a λ abstraction \ a' -> f (a ') that is now just f.

All the other edits involved collapsing end parentheses to the end of the last line: collected like this))). This is our usual style.

If this all looks okay to you, I'll go ahead and merge this one.

Yes, feel free to merge. Thank you.