Isomorphism is equality

Isomorphism is equality
Thierry Coquand and Nils Anders Danielsson
In Indagationes Mathematicae 24(4), 2013. [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 monoids on sets equality coincides with the usual notion of isomorphism from universal algebra, and for posets of the kind mentioned above equality coincides with order isomorphism.