search

rzk-lang / sHoTT

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

Weak ext ext and paths in contractible types #47

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

I added a proof that in contractible types paths can be identified. I also had two easy lemmas in the extension extensionality section

emilyriehl commented 1 year ago

Hi @jonalfcam. Your first term already exists and is called eq-is-contr.

emilyriehl commented 1 year ago

I like leaving the new terms in the contractible types file in the new section. Just reference the existing definition of eq-is-contr from the contractible types data section. Otherwise this looks ready to merge.