[FOM] HoTT as foundations: a short account
P.B.Levy at cs.bham.ac.uk
Sat Nov 1 20:38:10 EDT 2014
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 Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
More information about the FOM