rzk-lang / sHoTT

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

Weak ext ext and prop 4.10 #42

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

Added the proof of prop 4.10.

jonalfcam commented 1 year ago

Thank you for all the suggestions!