[FOM] A question about isomorphic structures

[Louis Garde]

Le 26/03/2016 18:01, Arnon Avron a écrit :
> By the way,  is "the carrier of a structure A" not
> a *set*? If not - what is it? And if yes - does not it means that
> we still need some set theory for the alleged "alternative foundations"?
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 ?
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.

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.

> I guess that I'll get here answers of the type "you are trying
> here to understand things from the set-theoretical point of view,
> using the set-theoretical language, instead of trying to understand
> them from the internal HoTT point of view, using its own language".
> This might well be true. But then I see no point in arguing with a
> camp with which I do not share even my basic  language and concepts.
That's a strange point of view ! For sure if we start from the 
assumption that "ZFC is the foundation", then there is not much to argue.
I can understand that in your daily work you are not interested in HoTT, 
and there is no point in arguing about it.
But from the "philosophical" or "metamathematical" point of view, there 
are concepts in HoTT that you cannot just ignore, unless you think that 
HoTT is not valid mathematics (which would be a very restrictive point 
of view), or you admit that you are not interested in foundation of 
-all- mathematics, but only in foundation of -set-theoretic- mathematics.
If you are interested in foundation of all mathematics, and think that 
set-theory explains everything, then it is a challenge for you to show 
how to re-write in set-theory the basic concepts of HoTT, including its 
definition of logical consequence, and logical negation.

Louis.