Isomorphism Is Equality
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.Nils Anders Danielsson
Last updated Sat Feb 16 11:19:39 CET 2013.