The HTS language proposed by Voevodsky exposes two different presheaf models of type theory: the inner one is homotopy type system presheaf that models HoTT and the outer one is traditional Martin-Löf type system presheaf that models set theory with UIP. The motivation behind this doubling is to have an ability to express semisemplicial types. Theoretical work on merging meta-theoretical and homotopical languages was continued in 2LTT [Anenkov, Capriotti, Kraus, Sattler].
While we are on our road to HTS with Lean-like tactic language, currently we are at the stage of regular cubical (HoTT) type checker with CHM-style primitives, or more general CCHM type checker. You may try it at Github: groupoid/anders.
$ opam install anders $ anders Anders theorem prover [PTS][MLTT][CCHM-4][HTS]. invoke = anders | anders list list =  | command list command = check filename | lex filename | parse filename | help | cubicaltt filename | girard | trace
Anders is idiomatic and educational. We carefully draw the favourite Lean-compatible syntax to fit 130 LOC in Menhir, the MLTT core (based on Mini-TT) is 500 LOC and pretypes presheaf is another 500 LOC.