Predicate logic of sub-C-sets

[epatters]

PR #467 implemented the bi-Heyting algebra of sub-C-sets, which is the propositional fragment of the logic of a presheaf topos. We should upgrade it to predicate logic, which would involve implementing

• the pullback functor f^*: Sub(Y) -> Sub(X) induced by a C-set homomorphism f: X -> Y
• the left and right adjoints to this functor, which are generalized forms of existential and universal quantification

[kris-brown]

The pullback part of this is called hom_inv in #605