Left/right derived functors. If $F$ is an additive functor from a category $A$ to another category $B$, then the left/right derived functors of $F$ go from $A$ to... where? Not to $B$ certainly, because this would require global choice on $A$ or break canonicity.
There seem to be solutions nowadays, with the notions of derived categories and anafunctors. Unfortunately, there seems to be no introductory text yet which would systematically develop homological algebra in a clean way, without cheating and speculating over one's head. I am more than glad to be proven wrong...
PS. This might be what Harry Gindi is referring to.
