[FOM] HoTT as foundations: a short account

[Urs Schreiber]

On 11/2/14, Paul Levy <P.B.Levy at cs.bham.ac.uk> wrote:
>
> 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
>>
>>> "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.


By the way, this is because the univalent type universe in HoTT is
(just) the groupoid of types, not the category of types.

(Or rather: the infinity-groupoid, not the infinity-category.)

Discussion of how to promote the type universe groupoid to a category
in HoTT is in http://arxiv.org/abs/1303.0584 .