Proof of the naturality equation (Prop 6.6)

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

Proof of the naturality equation (Prop 6.6) #40

Closed kyoDralliam closed 1 year ago

kyoDralliam commented 1 year ago

Fixes #9

I guess all the "local" names in the section eq-from-square will be polluting the global environment which sounds bad. What should I do about them ?

fredrik-bakke commented 1 year ago

naturality-nat-trans-is-segal is good! 👍