Equivalence of weak and strict extension types

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

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

45 stars 12 forks source link

Closed jonweinb closed 1 year ago

jonweinb commented 1 year ago

I'm working on this currently, namely the equivalence stipulated in [BW23, Section 2.4].

TashiWalde commented 1 year ago

@jonweinb This Issue should be closed now, correct? Or is there more to do here?