Look into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall.

As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you.

Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it.

https://golem.ph.utexas.edu/category/2013/01/from_set_theory...

If you're specifically interested in Univalent Foundations, just read the book. https://homotopytypetheory.org/book/