category_theory.functor.ext

Proving equality between functors. This isn't an extensionality lemma, because usually you don't really want to do this.