[FOM] A question about isomorphic structures
louis.garde at free.fr
Wed Mar 30 17:03:36 EDT 2016
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).
More information about the FOM