General Subobjectclassifier

In the book, we called this `qinv`.  But I don't think it should be dignified with a name.  Rather than proving `PowisoFam` and then `FamequivPow`, you should just go directly to `FamequivPow`, beginning by applying `equiv_adjointify` and then reproduce the current proof of `PowisoFam`.