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