It's worth noting that Univalent Foundations (and type theory in general) really has nothing to do with computers. You can do it on paper like traditional set t

It's worth noting that Univalent Foundations (and type theory in general) really has nothing to do with computers. You can do it on paper like traditional set theory based math, and you can formalize set theory on a computer. The reason type theory is primarily done using proof assistants is that is a constructive theory, or in other words, you can actually compute with the functions you define. This is something you can't do with set theory, which is why doing type theory on a computer lets the computer do a lot more things for you than it easily could doing set theory on the computer.