The universal constructions works with the space of words $a_1^{-1} b_1 \dots a_n^{-1} b_n$. If you work with symmetric monoidal categories then on group completion you get canonical nontrivial isos $b a^{-1} = a^{-1} b$, which allow you to build a path $a_1^{-1} b_1 \dots a_n^{-1} b_n = a^-1 b$, $a = a_1 \dots a_n$, $b = b_1 \dots b_n$. Thus you can get a homotopy equivalence with category of pairs $a^{-1} b$ with some very complex morphisms, and the multiplication is at best homotopy equivalent to the one you would want to write.

I don't have time for a full answer atm. The best reference (to my meager knowledge) is arxiv.org/abs/0706.0531 Note that the statement of their theorem is actually quite different from yours, though related. I have an unpublished construction which looks very plausible. There a basically 3 main issues. The first is that group completion naturally lands in $(\infty, 1)$-categories. Not a big deal really since you can truncate. The second is that you cannot really define multiplication objectwise as stated by Quillen and you. cont

However, in the specific important case of classical left and right derived functors, it is a theorem that they indeed form universal delta-functors. For proof see e.g. ([1], Chapter 2), in particular theorems 2.4.6 and 2.4.7. The fact that classical derived functors factor through Kan extension along localization w.r.t. quasi-isomorphisms is proved in ([1], Th. 10.5.6). [1]: C. A. Weibel, An introduction to homological algebra.

I am pretty sure that those definitions neither coincide nor are even closely related, unless in special cases. Note that there is extra structure you are missing on the right side: passage to homology after Kan extension. Defining an analogue of homology on homotopy category requires the notion of t-structure, and there can be very different (or even none) t-structures on the same homotopy category (look up "perverse sheaves"). The notion of delta-functor on its own is just not deep enough to claim some structural properties,it is just a statement of most basic properties of derived functors.

@DylanWilson, the proof is simple only for associative algebras, while the topological result is true without restrictions.

I think that you should be a bit more specific about the class of operations that you admit, since any (stable) homotopy group of spheres determines a (stable) homotopy operation and is thus trivially generated by it.

Actually, it looks very relevant. No need to hide it in the comment tread.

@ZhenLin, not sure how you modify it. Do you mean two constant functors $c \mapsto 1$ and $c \mapsto C $ with transformation $c \mapsto c: 1 \to C $? Because it is also lax natural: $f: c \to c'$ gives 2-cell $f: c \to c'$.

@ZhenLin, nice example, but it's natural in the naturally generalized sense. For functors into $Cat $ we should consider lax naturality, and for both $F: C \to Cat, Fc := C/_c $ and $F: C^{op} \to Cat, Fc := C/_c $ the transformation $1 \to F $ is lax natural (even pseudo natural in the second case) and represented by $1 \to Cat $.

@JoelDavidHamkins, AC is manifestly non-functorial. Specifically, I have in mind HoTT, where we can prove that AC for anything more than 0-types is inconsistent. It is not surprising that a non-functorial axiom allows us to define non-functorial families. Also your statement is specific to Godel's model, while I'm interested in model-independent results.

@KarolSzumiło, my goal is not to devise some devious way to equate the non-equatable, but rather to understand what can happen when one is restricted to natural constructions. Can we quantify the unnaturality of results?

@KarolSzumiło, it's not exactly a counterexample to my point since the categories are different. In the case of $Set$ your construction would take the category of well-ordered sets with all maps. Since the equivalence requires choice, it doesn't actually help you for functors on $Set$, but the point is valid: in general it is not so clear which categories $C$ are good enough. I'd say that $C$ should be $Set$ or explicitly definable over $Set$.

You pretty much wrote the answer. $K_n = \mathrm{colim}\, \Omega^{i-n}MSO(i)$. If $X/Y$ is a finite CW-space, then it is a compact object in the category of spaces, and its stabilization $\Sigma^{\infty}(X/Y)$ is a compact object in the category of spectra. $D$ is comact if $Hom(D,\cdot)$ preserves filtered colimits, in particular colimits of towers. If $X/Y$ is infinite then the formula you wrote doesn't define a cohomology theory and the only correct way to define it is via the representing object given above.

@IianSmythe, it can't be more difficult since traditional set theory (or at least some practically relevant version of it) is contained in HoTT and can be relatively painlessly extracted. In that sense it is at least as good as traditional type theory. On the other hand, many objects which are a real pain to define set-theoretically (like groupoids and higher categories) can be defined much more concisely.