[FOM] HoTT as foundations: a short account

[Paul Levy]

On 31 Oct 2014, at 19:08, fom-request at cs.nyu.edu wrote:

> Date: Fri, 31 Oct 2014 12:37:40 +0100
> From: Freek Wiedijk <freek at cs.ru.nl>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] HoTT as foundations: a short account
> Message-ID: <20141031113740.GB15378 at wheezy.localdomain>
> Content-Type: text/plain; charset=us-ascii
>
> Dear Paul,
>
>> "Set" is the category of sets and *functions*.  Here I am talking
>> about the category (groupoid) of sets and *bijections*.
>
> My apologies for my confusion.  So does this mean that in
> HoTT it _is_ possible to define an "endofunction" on sets
> that is _not_ a functor on the category Set?

Yes, take the function F sending a set X to the set of all functions  
from X to 0.   In both HoTT and ZF, this function F has no extension  
to an endofunctor on Set, because there is a function from 0 to 1 but  
no function from F0 to F1.

Paul

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