I just realized an impredicative universe on top of a predicative one is still inconsistent
Hurkens' paradox uses two impredicative universe layers but the impredicativity of the bottom one is never exploited... I think
Hard to check this mechanically
@ionchy yeah. But docs are outdated, and we don’t have great abstractions for universes. I walk through adding them in my Every Proof Assistant talk.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.