[FOM] HoTT as foundations: a short account

[Urs Schreiber]

On 10/29/14, Freek Wiedijk <freek at cs.ru.nl> wrote:
> Dear Paul,
>
> Thanks for the very clear motivation for HoTT.  However:
>
>>In traditional foundations, one can construct an
>>endofunction on the universe of sets that is not functorial
>>on bijections.  [...]
>
> In this account the category of sets (it's called "Set",
> right?) seems to have a priviledged position.  Therefore, I
> think this is too "set theoretic" to be a truely satisfactory
> motivation.
>
> What if I want to work in the category of topological spaces
> ("Top"), shouldn't I have something in the framework that
> ensures that whatever I do is functorial in _that_ category?
> What's so special about sets to get this special treatment
> in HoTT?


Indeed, sets do not get a special treatment in HoTT, and this is part
of the whole point. The universe in HoTT is not one of sets but of
homotopy types, whence the name. This contains constructive sets as
the homotopy 0-types [1], but contains much more.

The univalence axiom [2] which Paul's message secretly referred to
says that equivalences between such homotopy types (which on sets are
isomorphisms and more generally are homotopy equivalences) are
equivalent to propositional equalities between these types.

Notice that everything being constructive, even the sets appearing
here are more general than the ZFC sets, namely they may be
interpreted as sheaves of sets on any site. If the site is one of
topological spaces, then these constructive sets contain topological
spaces (via the Yoneda embedding) and then the univalence axiom
applies to these, just as you seem to imagine it should.

Notice again the important point which we already discussed elsewhere:
topological spaces, apart from being sets with "cohesive structure"
(namely with topology) are also *representatives* of bare homotopy
types. For instance the topological space R^2 - {0}  represents the
homotopy type known as BZ (the homotopy theoretic circle), as do many
other topological spaces such as the unit circle inside R^2 etc..
These topological spaces are not the same as the homotopy types which
they represent. In models of homotopy type theory in infinity-toposes
over topological spaces, both R^2 - {0} and BZ are types and they are
not equivalent.

In that model however there is an operation, a modal operator, which
takes each topological spaces to the bare homotopy type which it
represents, its shape. This modal operator is called the "shape
modality". Adding the existence of a shape modality to HoTT makes it
"cohesive HoTT" [3].

[1] http://ncatlab.org/nlab/show/h-set
[2] http://ncatlab.org/nlab/show/univalence
[3] http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory