search

rzk-lang / sHoTT

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

NaiveExtExt implies WeakExtExt #107

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

This completes the cycle of equivalence between NaiveExtExt, WeakExtExt and ExtExt.

As an intermediate step, I deduce from NaiveExtExt that all extension types in a family of propositions are themselves propositions.

Note: relies on #104 and #105 .

TashiWalde commented 1 year ago

Tagging @emilyriehl, who I believe was also interested in this result.

emilyriehl commented 1 year ago

Indeed! After our discussions in Regensburg, I had hoped this would be provable --- and was planning to investigate myself if you didn't beat me to it ;)

Anyway I'm very happy to have this figured out. We should start a discussion (perhaps over on Zulip) about whether we should simply our assumptions moving forward (eg only ever assume extext or funext, to make it clearer that globally only two hypotheses are needed, not six).

TashiWalde commented 1 year ago

Indeed! After our discussions in Regensburg, I had hoped this would be provable --- and was planning to investigate myself if you didn't beat me to it ;)

Anyway I'm very happy to have this figured out. We should start a discussion (perhaps over on Zulip) about whether we should simply our assumptions moving forward (eg only ever assume extext or funext, to make it clearer that globally only two hypotheses are needed, not six).

I have indeed started exactly that discussion :) But nobody has weighed in on it so far :(