Expliciting the homs-are-sets condition, using an alternative definition of iso

This PR factors out the homs-are-sets condition for precategories.
Also, it features an alternative definition of is_iso(f), namely is_iso(f):=forall c:C, isweq (precomp_with f c), ie. the map \lambda g:b-->c. f;;g is an equivalence, suggested by Vladimir.
The old variant of isos is still available as "z_iso".