An isomorphism is a structural correspondence between two objects. In HoTT a type's structure is its points, paths between points, paths between paths... etc. N

An isomorphism is a structural correspondence between two objects. In HoTT a type's structure is its points, paths between points, paths between paths... etc. Note that "path" is an abstract idea: it's a construction parameterized on two points that is reflexive, symmetric, and transitive. Now, the whole universe of types itself has a path structure. Univalence says that isomorphisms of types are the same as paths between types. In a way it bridges the gap between structural isomorphism and Leibniz equality.