rzk-lang / sHoTT

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

Clean up naming in 06-contractible #109

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

I noticed that many terms in 06-contractible.rzk.md did not adhere to our naming convention and some theorems were duplicated with non-canonical names.

Tried to clean this up a bit and give more standard names to the terms. Of course this caused some ripples throughout other files.