Isomorphism Is Equality

Isomorphism Is Equality
Thierry Coquand and Nils Anders Danielsson
Draft. [pdf, highlighted Agda code, tarball with code]

Abstract

The setting of this work is dependent type theory extended with the univalence axiom. We prove that, for a large class of algebraic structures, isomorphic instances of a structure are equal—in fact, isomorphism is in bijective correspondence with equality. The class of structures includes monoids whose underlying types are "sets", and also posets where the underlying types are sets and the ordering relations are pointwise "propositional". For instance, equality of monoids on sets coincides with the usual notion of isomorphism from universal algebra, and equality of posets of the kind mentioned above coincides with order isomorphism.