Oops I spent the entire day on nonsense. At least after today I will no longer wonder about strong impredicative pairs

So uh why is two impredicative universes inconsistent again


Ok I've got it. I'll have to walk through it because there is no proof assistant for which I can turn on impredicativity for Type as I wish but I've got it

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.