A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to describe their values more precisely. For example, the type list A can be refined to a type vec A n classifying vectors of length n. Then, when you forget the extra information, you get a type that is isomorphic to the original. For example, list A is isomorphic to Σ n:nat.vec A n (vectors of an existentially quantified length).
As an example of a context, consider a monoid structure on a type A, represented represented by the type family
Monoid A =
Σ (m : A → A → A).
Σ (u : A).
Σ (assoc : Π x y z. Id (m (m x y) z)…
View original post 743 more words