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

I wish I could mechanize it somehow
Where can I define my own typing rules

@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.

Sign in to participate in the conversation

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