[FOM] A question about isomorphic structures

[Till Mossakowski]

I have a question to the HoTT community about the consequences of the 
univalence axiom:
If I understand HoTT and univalence correctly: whenever you have two 
types A and B, and there is some (definable) bijection between them, 
then already A=B. That is, while the structure of A and B usually is 
needed in order to define the bijection, the bijection need not to 
preserve this structure (example: 
http://homotopytypetheory.org/2015/01/20/ts1s1-cubically/). This means 
that the correct slogan should be "definable bijection implies 
equality", while "isomorphism implies equality" should be reserved for 
specific situations where the isomorphism type is explicitly specified 
(e.g. 
http://homotopytypetheory.org/2012/09/23/isomorphism-implies-equality/) 
- otherwise, it is even unclear what "isomorphism" should exactly mean.
This implies e.g. that integers=rationals, even though their ring 
structures are of course different. And via this identity, each then is 
equipped with two different ring structures.
Is this view correct?

Till Mossakowski

Am 27.03.2016 um 11:36 schrieb Louis Garde:
>
> But there is a different way to look at mathematical objects.
> A structure is defined with (formal) rules, and its "carrier" is any 
> collection of objects, in mathematics or anywhere else, that satisfies 
> such rules.
> Once defined, the structure can be mapped to many different possible 
> "carriers".
> With classical foundations, you first define a "carrier" - sets - and 
> then define structures above them.
> With HoTT, you first define structures, and then study their "carriers".
>
> The univalent axiom says that two equivalent structures (that share 
> the same "carriers") are identical (share the same properties).
> In a set-theoretic point of view, it does not really make sense: two 
> equivalent structures defined on differents sets always have some 
> differents properties, so they cannot be identical.
> For instance, [0, 1, ...] is equivalent to [1, 2, ...] but not 
> identical, as 0 is member of the first set, but not of the second.
> How to define natural numbers in set-theory ? There are many 
> equivalent ways to do it.
> All these definitions are equivalent, but the resulting sets are not 
> identical. So what are the 'real' natural numbers ? Is '0' really the 
> empty set, or not ?
> There can be no good answer to these questions in set theory; but 
> usually we do not really care, because we understand intuitively that 
> the 'real' natural numbers are "what is common to all the possible 
> equivalent definitions". In other words, what is interesting is the 
> structure of the natural numbers, not their possible "carriers".
> This is exactly what HoTT and its univalent axiom allows you do to.
>