[FOM] New Umbrella?

[Harvey Friedman]

I want to step into this HoTT as an ignorant fool (me), with the hope
of clarifying just what would remain to be done in order to really
have a productive discussion as to what is to be gained and lost by
altering the Standard Umbrella for mathematics (ZFC).

A good place for this ignorant fool to walk into this is perhaps
suggested d by Freek/Urs latest.

On 10/24/14, Freek Wiedijk <freek at cs.ru.nl> wrote in small part:

> I know the HIT that in HoTT represents the circle, but what
> is the HIT for the real line?  Or is in HoTT the real line
> the same thing as the one point space?  (They have the
> same _homotopy,_ but surely these are different things?

Indeed, there is the real line R which is a set (i.e. an "hset", a
0-truncated homotopy type) in the usual way, and then there is is
homotopy theoretic shape, the homotopy type "shape(R)" which is
equivalent to the point.

More interestingly, there is the circle R^2 - {0}, which is a set, and
there there is its homotopy theoretic, the homotopy type shape(R^2 -
{0})   which is a 1-truncated homotopy type, also known  as the
classifying space BZ.

And so forth.

HoTT with this shape-modality added that formalizes the way that
underlying any geometric homotopy type is a bare shape homotopy type,
is called "cohesive homotopy theory" [1]. See [2] for the above kind
of examples.

[1] http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory
[2]
http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory#GeometricSpacesAndTheirHomotopyTypes

********

What does this ignorant fool have to say about how to look at the real
line and the circle, in ordinary generally understandable, ignorant
fool terms?

ORDER THEORETICALLY

(R,<) is the unique complete separable dense linear ordering up to
isomorphism. The circle is obviously not even a linear ordering, but
what is it?

(C,B) is the "point glued wrapping around of (R,<),".

(C,B) is the unique complete separable dense betweenness relation up
to isomorphism.

A second construction is to take two points 0 < 1, and get (C,B) as
"identifying 0,1". Also getting the unique complete separable dense
betweenness relation up to isomorphism.

ORDERED GROUP THEORETICALLY

(R,<,+) is the unique complete densely ordered group up to isomorphism.

We define "complete dense betweenness groups".

(C,B,+) is the unique complete dense betweenness group up to isomorphism.

Maybe we should start with (R,<,+), and then look at [0,1) and [0,2).
Then identify [1,2) with [0,1).

Or maybe we should start with (R,<,+) and then just somehow say that 0
and 1 are being identified? Should that drive us by general
considerations automatically to (C,B,+)? Or maybe just to (C,+), where
B is not regarded as fundamental, but rather a derived notion?

I think there are some interesting things here - maybe well known -
about the proper fundamental constructions that go from one
fundamental mathematical structure to others.

Generally understandable compared to the Urs response?

Harvey Friedman