Given an equivalence between (all the values of) two types, you can assume the types are equal, i.e. substitute one for the other in any value, no matter how co

Given an equivalence between (all the values of) two types, you can assume the types are equal, i.e. substitute one for the other in any value, no matter how complex (including functions on values/types etc.). The value/function conversion is called a "transport" and it actually depends on which equality you've chosen (called "paths" in HoTT). E.g. bool <-> bit can map false => 0, true => 1 or false => 1, true => 0. So `(a: bool, b: bool) => a && b` can be "transported" to `(a: bit, b: bit) => a & b` or to `(a: bit, b: bit) => !(!a & !b)` (which is `a | b`). Of course, bit tricks aren't that useful, but two types which are defined differently (e.g. from different libraries, or different versions of the same library), yet contain the same information, would be interchangeable given a "path" (in the case of the Univalence Axiom, a proof of equivalence). The other important addition in HoTT is defining non-trivial "paths" (equalities) between values of a type when you define the type - this is used in the HoTT book to describe integer, rational and real numbers, in a way reminiscent of quotient sets.