Recent roadmap (2)

[ice1000]

What have we done?

Since #362, we have done a lot! We have:

• Successfully replaced visitors, including an overhaul of ulift! Thank you @wsx-ucb
• Replaced rwc with cubical features (initially)!
• Started working on classes! Some work is done by tsao-chi, but there are much more.
• Impredicative, definitionally irrelevant Prop is also implemented. This also involves tsao-chi.
• Literate mode overhaul! Thank you @imkiva

For tactics, we have not done much.

What's next?

• We want to further overhaul cubical to be Cartesian cubical! This means we need a set of fancier Kan operations and a simplified interval type.
• The class system needs to be done (Typeclass Inheritance #43, Unification in Typeclass Resolution #44, Overhaul struct #386, Struct WIP #419, Struct WIP #429). We need a way to resolve instances, and I believe the locally enabled named instances proposed by Bob (https://www.cs.cmu.edu/~rwh/papers/mtc/short.pdf) and the tabled instance resolution algorithm proposed by the Lean developers sound very promising.
• We need a new overhaul on definitional irrelevance (cf. https://proofassistants.stackexchange.com/q/1970/32). I now consider rule-based impredicativity totally fucked up and should be dropped immediately, especially when you have a termination check based function definition syntax (so Coq & Lean are probably fine). Impredicativity is implied by LEM hence implied by AC, so why not use classical axioms when we want them? If we want to work constructively, we may also work with resizing axioms. Predicative assumption (Predicativity assumption for terck #908) is essential for defining W types and Trebor's Brouwer tree type.
• I want to upgrade constraint solving to support more features. Currently, it cannot find the type of sth like ∀ a b → a = b (4b6fff2) but we can generate a fake term like FnSort xxx and compute via PiTerm.max.
• The rest of this list