For core lang, MLTT+Levitation or Cubical+Levitation; haven't decided (will wait until hdtt2020 done); probably no recursive+inductive constructs, only mu and ind from levitation.
Core language feels pretty finalized as cubical + levitation, implementation of levitation is ongoing. Still have to read ABCFHL and CCHM for cubical parts. In particular, levitating HITs seems plausibly paper-worthy (though maybe it's trivial; I don't know what soundness constraints exist for HITs).
The next big thing (and a large impediment to being able to properly define/document the language) is properly implementing the elaborator. As of 2e6a9d7, there's a bit of code that's certainly called the elaborator, but is much more like a back half of the parser. In particular, it doesn't occur simultaneously with typechecking, and as such doesn't have type information to (e.g.) disambiguate literals.
Once levitation is done (enough to define the free monad, at least), I'll take a swing at fixing up the elaborator to actually be one. After that's done, the standard library can be built out to include elaborations for all the things people might expect (e.g. implicit arguments, polymorphic literals, typeclasses).