[FOM] HoTT as foundations: a short account

Freek Wiedijk freek at cs.ru.nl
Fri Oct 31 07:37:40 EDT 2014

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?


More information about the FOM mailing list