search

rzk-lang / sHoTT

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

Interchange law for homotopies (RS17, Proposition 5.15) #71

Closed kyoDralliam closed 1 year ago

kyoDralliam commented 1 year ago

Closes #6