search

rzk-lang / sHoTT

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

Naive extext #75

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

For some applications an even weaker version of extension extensionality suffices, which just that pointwise equality of extensions can always be glued to an equality. (Without asserting that this reconstruction be an equivalence).

I have added a type for this, called NaiveExtExt.