[logicchains]

IntelliJ Arend probably has the most comprehensive support for HOTT among the proof systems: https://arend-lang.github.io/ . Not a lot in the way of tutorials though, just the official documentation.