[FOM] A question about isomorphic structures

[Louis Garde]

Arnon Avron wrote:
 > The first two things I need to know for this is what is it about,
 > and whether it can be trusted.

I think that we must admit that there is no single, clear answer to 
"what it is about".

Here is what the HoTT book writes about it:
"One problem in understanding type theory from a mathematical point of 
view, however, has
always been that the basic concept of type is unlike that of set in ways 
that have been hard to make
precise. We believe that the new idea of regarding types, not as strange 
sets (perhaps constructed
without using classical logic), but as spaces, viewed from the 
perspective of homotopy theory, is
a significant step forward. In particular, it solves the problem of 
understanding how the notion
of equality of elements of a type differs from that of elements of a set."

My personal interpretation is that it is about structures, where a 
structure is defined with a list of rules.
For instance, the natural numbers is the structure defined with 2 
specific rules: the rule that such structure has an element (identified 
as '0'), and the rule that there is an operation (identified as 
'successor') taking any element of this structure, and giving as result 
an element of the same structure.
The nature of the element '0' is undefined: it is free of 
interpretation, and does not need to be a set. What matters is the 
rules, not how you interpret them.
You have many different structures that satisfy these two rules; the 
natural numbers is the unique structure that satisfies these two rules, 
and only them.
This is formally defined with the induction principle. The induction 
principle allows you to build functions between structures: if C is any 
structure that satisfies the 2 rules of N (among others), then you have 
a (constructive) function from N to C.

It is possible to define in the same way the structure of the circle, 
which has also only 2 specific rules: the circle has a point, and a path 
from this point to itself.
More complex structures can be defined, for instance with rules defining 
two inter-connected structures together.
You can also build structures above predefined structures, in the same 
way as you build structures on sets. But these are not inductive 
structures, and the uniqueness property is not guaranteed any more.

The sets are then some specific structures among others (the structure 
of the natural numbers is a set, but the structure of the circle is not).

Louis.