Lifting in the presence of excluded middle

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

GNU General Public License v3.0

220 stars 40 forks source link

Lifting in the presence of excluded middle #287

Closed tomdjong closed 3 weeks ago

tomdjong commented 3 weeks ago

This was left unformalized from my thesis: 𝓛 X ≃ (𝟙 + X) iff EM holds. As an auxiliary result, I also formalized that: 𝟚 ≃ Ω iff EM holds (obvious, of course).

martinescardo commented 3 weeks ago

Nice to have this. Feel free to merge when you are ready.

martinescardo commented 3 weeks ago

Shall I do it?

tomdjong commented 3 weeks ago

Please go ahead. I'm currently afk. Thanks!

On Sat, 22 Jun 2024, 18:47 Martin Escardo, @.***> wrote:

Shall I do it?

— Reply to this email directly, view it on GitHub https://github.com/martinescardo/TypeTopology/pull/287#issuecomment-2184126555, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKOA4ZZKSC4RNICJYBHNYS3ZIW2CFAVCNFSM6AAAAABJXQI6JOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBUGEZDMNJVGU . You are receiving this because you authored the thread.Message ID: @.***>