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
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.