I have never managed to understand why you need univalent foundations as opposed to just using some dependent type theory like Lean. As far as I see Lean could do all the mathematics I could imagine. I can only imagine that univalent foundations could help make things cleaner, but for now Lean seems good enough.
