Happy Programming

Although Agda hasn't supported universe polymorphism, recently an option --type-in-type is added to enable impredicativity. Modelling sets is now much, much easier. Defining the type of ℙ as Set -> Set, the type of ∈ is now simply A ← ℙ A, and the relation subset = ∈ ﹨ ∈ also has a simple type ℙ A ← ℙ A. All those annoying ₁'s are gone! Unfortunately, going back to impredicativity would make the type system inconsistent, which means every proposition can be proved in the system and the system would be considered unreliable. Therefore it is not a good idea for AoPA to switch to "impredicative sets", I guess?

--
That's unfortunate...