[FOM] Identity of isomorphic structures

[Steve Awodey]

Dear FOMers,

I can say a bit more for those not familiar with the article, but, obviously, the best thing would be to read the article itself.

The purpose of this article is to explain the apparent tension between the obviously false statement that “isomorphic mathematical structures are identical” (understood in classical terms, say, of ZFC) and the univalence axiom in homotopy type theory, which is demonstrably consistent, and yet apparently implies the foregoing falsehood.  It’s easy to state examples, like the one given by Prof. Davis, which make it hard to understand how such identifications are even possible.  It’s harder to explain how such identifications can be made in a way that could even be useful.

Let me first say that the univalence axiom is not “a proposal to regard isomorphic structures" — understood in the classical way within ZF — "as identical" — also understood in the usual way.  That would obviously be absurd.  Rather, it is an axiom within a new system of foundations in which everything, from identity to isomorphism, are understood in a somewhat different way, which demonstrably admits this assumption without contradiction.  The challenge is to understand what it means *in that setting* — and that’s what the paper (and even more the HoTT book) is about, and more than can be done here.  

The short answer, however, is that every property, relation, or construction that can be specified by the system "respects isomorphisms” (and more general homotopy equivalences), in the sense of coming equipped with "transport operations” along all such mappings.  As a result, if e.g. A and B are isomorphic groups via a given isomorphism h : A -~-> B and P(X) is any property of groups that can be specified within the system, then h induces an equivalence h* : P(A) -~-> P(B), so that P(A) will hold iff P(B) does.  The specific isomorphism h is quite important in this, as is moreover the object Iso(A, B) of all such isos.  In particular, the object Id(A, B) of identities between A and B is itself equivalent to Iso(A, B), by the univalence axiom.  That is the precise sense in which it can be said informally that “isomorphic objects can be identified” in this setting: isomorphic groups A and B, will "have all the same properties" P in this sense.

A more careful explanation is to be found in the article in question or, even better, in the HoTT book, which is freely available here:

	http://homotopytypetheory.org/book/

Regards,

Steve

PS: what I have to say about the particular isomorphism mentioned by Prof. Davis is that it induces a transport operation on any property definable in homotopy type theory, so that anything that holds for the group of positive reals under multiplication also holds — in a suitably modified form specified by the transport operation — for the group of all reals under addition.  The specific “modification” involved is systematically provided by the system. This fact is precisely what makes the discovery of this isomorphism important. Properties that don’t behave well with respect to it are not definable in the system.


On Apr 7, 2014, at 3:48 PM, Martin Davis <martin at eipye.com> wrote:

> Steve Awodey's provocative and interesting article "Structuralism, Invariance, and Univalence" in the February 2014 issue of Philosophica Mathematica discusses the proposal to regard isomorphic structures as identical. (This proposition is a consequence of an even more widely embracing proposed axiom.)  Examples are given of situations in which mathematicians routinely "identify" two isomorphic structures with one another, such as identifying the Cauchy-sequence-of-rationals real numbers with the Dedkind-cuts-in-rationals real numbers. 
> 
> I would be interested to learn what proponents of this view would say about the well-known isomorphism between the group of positive real numbers under multiplication and the group of all real numbers under addition. Note that in this case it's the isomorphic mapping itself that is important: it underlies the use of logarithms in computation that  had such a significant role before modern computers. 
> 
> Martin
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom