<< All Posts Feed

Stop Doing Infinite Universe Hierarchies

Posted on 2025 Mar 11


A meme using the "STOP DOING X" template. It reads: STOP DOING INFINITE UNIVERSE HIERARCHIES - Standard ML does fine without it - YEARS OF programs yet NO REAL-WORLD USE FOUND for anything above Type 2 - Wanted to internalize your type theory ? We had a tool for that: It was called adding a couple axioms - "Yes please give me u of something. Please give me the type of it" - Statements dreamed up by evil wizards LOOK at what agda users have been demanding your Respect for all this time, with all the ordinals & theory we built for them (This is REAL levels, done by REAL level arithmetic ): Then are three screenshots: (1) Someone asking a question on the Lean zulip, because they typed `#check Type 87172` and the Lean server crashed (2) Someone exploited a bug in the Lean kernel to get a definition whose type was syntactically the same as its implementation (3) Syntax from a paper about arbitrary universe posets "Hello I would like SetĪ‰ apples please" They have played us for absolute fools


Older Back to Top Newer