Functors and morphisms between them (natural transformations) have become powerful tools in all areas of pure and meanwhile also applied mathematics. There are lots of nontrivial constructions of functors and morphisms of functors. But I think I don't know any example where it is hard to prove that something already constructed is a functor. Therefore my question is:
What are interesting and natural examples for categories $C,D$ and functions $F : \mathrm{Ob}(C) \to \mathrm{Ob}(D)$, $F : \mathrm{Mor}(C) \to \mathrm{Mor}(D)$ with $F(f : X \to Y) : F(X) \to F(Y)$ where the proof that $F$ is a functor is nontrivial and involves interesting mathematics? Also, the proof should not just replace $F$ by a different function coming from an obvious functor.
I have put "natural" here because for example I am not interested in the case where $C,D$ are just plain monoids / groups (although there might be interesting functions between monoids where it is hard to prove that they are homomorphisms). Further non-examples include the functoriality of hom-sets, (co)limits and most of the basic cohomology and homotopy theories.
I also know that you can "encode" the verification of any equality in mathematics by the statement that something is a functor, but my question is about examples of functors that already appear in mathematics without such an encoding.
A whole class of examples is coming from the theory of Quillen model categories. For a concrete example, consider the category $Top$ of topological spaces and the category $sSet$ of simplicial sets. Recall that a localization of a category $C$ by a class of morphisms $W$ is the category resulting from $C$ by freely inverting the arrows in $W$. Keeping track of the resulting category can be extremely difficult.
Consider the localization of $Top$ at the weak equivalences and consider the localization of $sSet$ at those morphisms that the geometric realization turns into weak equivalences.
You can now consider the processes between these localizations that are inherited by the geometric realization functor and the singular complex functor. Of course, these will be messy to describe. Verifying directly that these will be functors is hard. In a sense, the whole point of Quillen model structures is to avoid working directly with the localizations and instead working with the original category. Then one can show that with respect to the appropriate model structures each of the functors I mentioned is a Quillen functor which then implies that it does indeed pass to a functor between the localizations.
Of course, the preservation of hard work is in place. We don't get anything non-trivial for free here since all the hard work goes into proving that model structures.
I should mention though that probably the 'right' way to think of Quillen model categories is not so much as tools to work with the localization indirectly but rather as presentations of $\infty $-categories: http://ncatlab.org/nlab/show/model+category#related_concepts_58 .