Add some pullback lemmas and prelims for subobject functor.

[b-mehta]

This is great, especially pullback.hom_ext. I wonder if we can generalise this somehow - to show hom_ext it often suffices to show the property for only some objects (eg equalizers). Thanks!