Bartosz Milewski on Nostr: The main idea of HoTT/UF is to narrow the gap between equality and isomorphism. The ...

The main idea of HoTT/UF is to narrow the gap between equality and isomorphism. The problem is that (set-thoretic) equality is a yes/no proposition, whereas there could be many different isomorphisms betwee two objects. So if we want to merge the two notions, we have to extend equality to allow for multiple witnesses. Thus in MLTT, (propositional) equality is a type whose elements are witnesses.

Set-theoretic isomorphism is itself defined using equality (two compositions must be equal to identities). So if we modify equality, we should replace isomorphism with a more general type of equivalence.

The final step is to identify the new equality with the new equivalence in the axiom of univalence, which states that equality is equivalent to equivalence.