[FOM] Formal verification

[Urs Schreiber]

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