[FOM] A question about isomorphic structures

[Arnon Avron]

On Sun, Mar 27, 2016 at 11:36:36AM +0200, Louis Garde wrote:

> The structures in HoTT are formally defined in the same way as the
> sets in set-theory.
> So "the carrier of a structure A" in HoTT means the same thing as
> "the carrier of a set S" in set-theory.
> What is the "carrier of a set S" for you ? Some sort of meta-set ?

???

I have never heard before the expression "the carrier of a set S",
(unless S is used as a relation, in which case 
the carrier of the set S is defined as another *set*:
{x: \exists y. <x,y> \in S} (although here we usually talk
about the domain of S, not its "carrier")). 

> It's not easy to answer what "the carrier of a structure A" is, 
> just  as it is not easy to answer what "carrier of a set S" is.

The latter  question is meaningless, because nobody needs or uses 
this expression. So this "comparison" of yours makes no sense.

May I remind you that it is *you* who talked in your message
about the structure A and *its carrier*, obviously distinguishing
between the two. So again I ask, and please give this time  a direct
answer: Is "the carrier of a structure A" in HoTT another structure
(which in turn has another "carrier"?), or is it something 
different?  (In particular: is it actually an ordinary set, like those
studied in set theory?)  

Let me put the question differently: how many primitive
notions are there in HoTT? I understand that a "structure"
is a primitive notion. From what you write it seems to me
that some notion of a set (used for being "a carrier" of a structure)
is also needed, and then of course a primitive relation that associate
a structure with its carrier. Then there are isomorphisms. 
What are they? Structures? Sets? Something different?
I guess that there are also  functions which are not isomorphisms, right?
In any case, there should also be primitive relations that connect
functions (or at least isomorphisms) with their domains and ranges
(that should be structures, I guess). Is this list complete?

Note that the answer to the same question concerning set theory is clear:
we have there exactly two primitive notions: set and membership.
Being primitive, these two notions  are of course
not further defined or explained.
(As a result, there is no need to talk in set theory about 
"the carrier of a set S", and indeed nobody who works in set theory
uses this strange expression. In contrast, in HoTT it is 
obviously needed, as I infer from  the simple fact that you 
have used it!).
 


> 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.

So we have structures, and we have collections, right? (Do you
really think that using the word "collection" instead of "set"
or "class" makes any difference here?)

> 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".

I could not have put the difference  better. Indeed: in set theory
we *define* structures in terms of sets. In HoTT (according
to what you say) you only "study" the carrier of structures,
but you do not *define* these creatures - implying that you take them 
as a new type of objects.
 
> 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 different sets always have some
> different 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 ?

I do not see what is the problem with having
more than one choice. One takes the most convenient choice,
and that is. Choosing the natural numbers to be the finite
Von-Neumann ordinals is the most convenient and natural choice
(and in this case, with very good philosophical justification),
and that is. So *my* answer to your question is: yes,
0 is really the empty set - but this question has no importance
at all, so if you or other do not agree it makes no difference.

> 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". 

I completely misunderstand this extremely vague "characterization. Sorry.

> 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.

Great. But what is the price? And what ground do I have to trust
this axiom, where I at present I do not understand what this
theory is about?
 
> I can understand that in your daily work you are not interested in
> HoTT, and there is no point in arguing about it.

I am not yet at a stage of being able to say whether
I am interested  in HoTT or not.  I know very little about it, 
and so I am only at the stage of trying
to find out whether there is a reason for me to be interested in it.
The first two things I need to know for this is what is it about,
and whether it can be trusted. For the time being, 
your non-answers to my simple questions
give me very bad signs about the value and justification of HoTT.

Arnon