I don't think I actually use the hom-set definition anywhere, except when I show it equivalent to the unit-counit one.  I switched to the unit-counit definition being the default when I ran in to this problem originally.

@mikeshulman: That's correct.  So it might work to have that, and then have an `IsPreCategory` type-class, and build up everything I can on pre-precategories.  Do you think it's worth it, though?  I generally don't have much of a problem with assuming funext, and this is, approximately, the only place it's bitten me so far.