For dependent types, I would look at Idris [1]. Adding Univalence in a satisfying way is I think still somewhat of a research question (I could be wrong, and if anyone has any additional insight would be interested to hear), i.e. see this thread about Univalence in Coq [2]. There are some implementations in Cubical Type Theory, but I am not sure what the state of the art is there [3]
[1]https://www.idris-lang.org [2]https://homotopytypetheory.org/2012/01/22/univalence-versus-... [3]https://redprl.org