[FOM] HoTT as foundations: a short account

[Paul Levy]

> Date: Wed, 29 Oct 2014 14:44:58 +0100
> From: Freek Wiedijk <freek at cs.ru.nl>

> In this account the category of sets (it's called "Set",
> right?)

"Set" is the category of sets and *functions*.  Here I am talking  
about the category (groupoid) of sets and *bijections*.

> 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?

Both sentences "every endofunction on the class of sets is functorial  
on bijections" and "every endofunction on the class of topological  
spaces is functorial on homeomorphisms" are provable in HoTT and  
refutable in NBG (or ZF with universes).  I chose the former to give  
just one illustrative example for readers with a set-theoretic  
background, not to suggest that this is the only difference between  
the two systems, which it certainly isn't.

Paul



--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
http://www.cs.bham.ac.uk/~pbl