Weak ext ext - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

44 stars 12 forks source link

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

I added the proof of Prop 4.8 (ii) and the weak extension extensionality postulate. Some helper lemmas were needed for clarity.