[FOM] A question about isomorphic structures

[Arnon Avron]

I cannot quite understand the claim that 
in mathematics "isomorphic" means  "equal". Showing that two
*different* structures are actually isomorphic is sometimes
a non-trivial mathematical theorem. It would not make much sense
to prove such theorems if the two structures are completely identified. 
It is also certainly not true that mathematicians always identify two 
structures whenever they are isomorphic. indeed, Bruno Bentzen
was careful to write: "mathematicians OFTEN identify two structures 
whenever they are isomorphic", adding the fuzzy word "often" here. So
I wonder: does HoTT make this "often" precise and does not the fact 
that mathematicians do not always make this identification
"clearly in conflict with foundational theories such as" HoTT?

But the main question I would like to pose here is the following.
The only definition I know of "isomorphic" is that there *exists
a function* which is an isomorphism. Is there any theorem, or just
a reason to believe, that this is an absolute notion, that is: that
the answer to the question whether two given structures A and B are 
isomorphic or not never depends on the universe we are working in (and so,
in my understanding, the set-theory we are working in), and what
functions between  the carrier of A and the carrier of B are available
in that universe? 

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

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. 

This brings me back to a point I have made here in the past: I often 
feel that some discussions on FOM  are pointless because people
sometimes speak completely different  languages, although
they seem to use the same words. An example I have given here several
times is that my main trouble with devoted constructivists
(as, if I am not totally mistaken, most HoTTists are)
is that the "not" they use in doing mathematics (though *not*
in ordinary life or even in describing their own work in
the metalanguage) is *not* the "not" all people normally use, and they
even pretend *not* to understand the classical "not" that all
people (including them) normally use. (All the "*not*"s above
are classical, of course).

A clarification: after writing "HoTTist" (in the style
of "constructivist") completely innocently,
I discovered that it might *sound* (especially in the
context of what I was writing about) as having an hidden second
meaning. I did not and do not mean it. Obviously, when two groups 
do not understand each other, the problem is the same for both.
 
Arnon Avron

On Fri, Mar 25, 2016 at 03:13:39AM +0000, Bruno Bentzen wrote:
> Harvey Friedman:
> > A FOUNDATION FOR MATHEMATICS
> > There is a standard classical meaning for this. Namely, to provide a
> > precise "workable" rule book for mathematical "activity", that
> > provides suitable criteria for "correctness" or "legitimacy".
> 
> If I am interpreting you correctly, a key aspect of a foundational theory's "philosophical coherence" would be the question - perhaps motivated by Wittgenstein's famous slogan "meaning is use" - of whether or not it is compatible with the way mathematics is done in practice. In this sense, I think that the set-theoretical approach has some drawbacks.
> 
> It turns out that in practice mathematicians often identify two structures whenever they are isomorphic. This is clearly in conflict with set-theoretic foundational theories such as ZFC, since, for example, if A \cong B and \empty \in A then in general \empty \notin A.
> 
> Harvey Friedman:
> > I favor the approach of carefully adding a lot of sugar to ZFC, rather
> > than bringing in foreign elements or replacing aspects of ZFC.
> 
> I believe this issue is not a matter of adding more "sugar" to ZFC or other set theory, it is a limitation of the very set-theoretical framework, since equality, as given by the axiom of extensionality, is a much stronger requirement than isomorphism.
> 
> In contrast, this idea can be embodied within type theory. It is (roughly) the univalence axiom: two structures are equal if they are isomorphic.This is made possible by the fact that type theory, like category theory, has the nice property that every definable predicate of in the system is isomorphic-invariant. Therefore, HoTT admits a structuralist (and constuctivist) foundations of mathematics.
> 
> Harvey Friedman:
> >>> Among the obvious merits of ZFC as a foundation for mathematics, there
> >>> is one that I often see not sufficiently emphasized. That is, its
> >>> PHILOSOPHICAL COHERENCE.
> >>>
> >>> ../..
> >>>
> >>> But my impression is that the more radical proposals, particularly
> >>> HOTT, philosophical coherence is proudly thrown away.
> >
> > That is my understanding, which may or may not be correct. (However,
> > see below for a pointer to an internet manuscript ).This certainly
> > prima facie precludes HOTT as any kind of reasonable "foundation for
> > mathematics" in any standard sense.
> 
> In this respect, I cannot easily understand why HoTT would lack of "philosophical coherence" while ZFC would not.
> 
> I am learning a lot with this great discussion, however, I think we cannot objectively move forward with it since a better clarification of the word "philosophical coherence" is obviously required.
> 
> Bruno Bentzen

> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom