Oh wow, they have a HoTT research group? That's very interesting, and exciting. I'd love a JetBrains automated proof assistant.