Arnaud Spiwack (@aspiwack.bsky.social)

@andrejbauer.mathstodon.xyz.ap.brid.gy regarding non-Ω oracles in www.youtube.com/watch?v=DNGm... I'm reminded that in a sheafification in a quasi-topos requires such a Type-valued modality. So they'd probably be a better fit in a type theory like Rocq's where unique choice doesn't hold. Good stuff!

loading . . .

Andrej Bauer — How to use excluded middle safely YouTube video by Types and Topology Workshop https://www.youtube.com/watch?v=DNGmh02fWYY

about 2 months ago