To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Isomorphism is equality… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Isomorphism is equality

Journal article
Authors Thierry Coquand
Nils Anders Danielsson
Published in Indagationes mathematicae
Volume 24
Issue 4
Pages 1105-1120
ISSN 0019-3577
Publication year 2013
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 1105-1120
Language en
Subject categories Theoretical computer science


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. (C) 2013 Royal Dutch Mathematical Society (KWG). Published by Elsevier B.V. All rights reserved.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?