My (educated layman) understanding is that there actually is a useful thing that HoTT gives us as a foundation for mathematics. that ZFC does not. This is the t

My (educated layman) understanding is that there actually is a useful thing that HoTT gives us as a foundation for mathematics. that ZFC does not. This is the translation of proofs from one structure to an isomorphic one. For example, if I have, say, a group, and I prove something about it, you would think that the proof would hold for all isomorphic groups. Under ZFC this isn't true, or at least we don't get it for free. Under HoTT, we get this for free.