[FOM] HoTT as foundations: a short account

[Freek Wiedijk]

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?

Freek