It turns out that the usual definition of subsetoid is to general to
be used to define subcategories.  Subsetoids have an invariant that
states that if an object is in the subsetoid and that object is equal to
another, then the other object is also a member of the subsetoid. So if
we define subcategories using subsetoids, then this invariant will
enforce that if a morphism is in the subcategory and that morphism is
equal to another (strictly), then that other morphism is also member of
the subcategory, but we may not want that other arrow.

To handle this I have defined what I call restricted setoids, which are
setoids where the carriers are restricted by a predicate, very much like
subsetoids, but that predicate does not have to respect equality in the
sense discussed above.
Decided that I am sticking with my original thoughts on subcategories.
The setoid equality should be thought of as the strict equality in the
category, and not isomorphism.
A little clean up.
Merge branch 'dev'