[FOM] 1. Re: foundations meeting/FOMUS/discussion (martdowd at aol.com)

[Louis Garde]

Le 26 mars 2016 à 20:22, "John Corcoran" <corcoran at buffalo.edu> a écrit :
> (3) Why should anyone identify two structures? What is achieved?

Here is an extract of HoTT book's introduction that tries to explain it:

''From the logical point of view, however, it is a radically new idea: it says that isomorphic things can be identified! Mathematicians are of course used to identifying isomorphic structures in practice, but they generally do so by “abuse of notation”, or some other informal device, knowing that the objects involved are not “really” identical. But in this new foundational scheme, such structures can be formally identified, in the logical sense that every property or construction involving one also applies to the other. Indeed, the identification is now made explicit, and properties and constructions can be systematically transported along it. Moreover, the different ways in which such identifications may be made themselves form a structure that one can (and should!) take into account.''

Louis.