search

rzk-lang / sHoTT

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

Formalise middle-four interchange law (Proposition 5.15 of RS17 paper) #6

Closed fizruk closed 1 year ago

fizruk commented 1 year ago

Should be straightforward by path induction.

kyoDralliam commented 1 year ago

working on this