At a very high level the univalence axiom says that set operations may not look at the elements of a set. Consider the cartesian product versus set union. The cartesian product does not look at the elements of the sets, but the union does. If A and B share an element then this element will appear only once in A union B, so the number of elements in the union depends on the actual elements in A and B. In contrast, the number of elements in A x B only depends on the number of elements in A and B. The cartesian product does not care about the internals of elements themselves. With infinite sets it's not clear what number of elements means. Mathematicians say that the number of elements in A and B is the same if there is a way to pair each element in A with an unique element in B. The condition that set operations don't depend on the elements in the set can then be expressed as follows. If there is a pairing of elements between A and A' and between B and B' then there is a pairing between op(A,B) and op(A',B'). The univalence axiom basically says that all set operations in HoTT are of this type.
To connect with the conventional terminology: we call A and A' equivalent if there exists such a pairing. Equality is the relation that all operations must respect: if A = A' and B = B' then op(A,B) = op(A',B'). The univalence axiom says that equality of sets is equivalence of sets.
To connect with the conventional terminology: we call A and A' equivalent if there exists such a pairing. Equality is the relation that all operations must respect: if A = A' and B = B' then op(A,B) = op(A',B'). The univalence axiom says that equality of sets is equivalence of sets.