All the frames you are mentioning are good for intuition. I would say the deepest one is 4. and that everything falls into place cleanly once you formulate things in the language of infinity-category theory (at the price of a lot of technicalities to establish the “right” language). For example,
singular homology with coefficients in A can be characterised as the unique colimit-preserving infinity-functor from the infinity-category of spaces/homotopy types/infinity-grpoids/anima to the derived infinity-category of abelian groups which sends a one-point space (equivalently any contractible space) to A[0].
The derived infinity-category of abelian groups is itself in some sense the “(stable presentable) Z-linearization” of the infinity-category of spaces, although this is more tricky to state precisely and I won’t try to do this here.
Here are two more closely related results in the same circle of ideas. The first one gives a description (a kind of fusion of Dold-Thom and Eilenberg-Steenrod) of homology purely internal to homotopy theory, and the second explains how homological algebra falls out of infinity-category theory:
Consider functors E:S_* --> S_* from the infinity-category of spaces to itself which commutes with filtered colimits, carries pushout squares to pullback squares, sends the one-point space to itself, and the 0-sphere (aka two points!) to a discrete space. Then A=E(S^0) has a natural structure of abelian group, and E is an (infinity-categorical version of) the Dold-Thom functor and satisfies pi_n E(X)=H_n(X,A) (reduced homology). In particular, E(S^n) is an Eilenberg-Maclane space K(A,n).
The category of functors E:S_* --> S_* satisfying all the properties above except the one about E(S^0) being discrete is a model for the infinity-category Sp of spectra, i.e. the “stabilization” (in a precise categorical sense) of the infinity-category of spaces. From this perspective, the functors from the previous points are called the Eilenberg-Maclane spectra HA. Moreover, the infinity-category of spectra has a symmetric monoidal structure (the “smash product”), HR is naturally an algebra object for this structure whenever R is a ring, and it makes sense to talk about the infinity-category LMod(HR) of left HR-modules in Sp. Then LMod(HR) is equivalent (essentially by a stable version of the Dold-Kan correspondence) to the infinity derived category of left R-modules D(R). In other words, for homotopy theorists, (chain complexes,quasi-isomorphisms) are just a funny point-set model for HR-module spectra!
All of this is discussed in the first chapter of Lurie’s Higher Algebra, except the last point which is not completely spelled out because monoidal structures and modules are only introduced later on.
I should point out that this perspective is largely a reformulation of the results you already mentioned, and in themselves certainly do not bring new computational techniques for singular homology. However they show that 1) homological algebra comes out “structurally” from homotopy theory, which itself comes out “structurally” from infinity-category theory and 2) homological algebra (including in more sophisticated contexts than just abelian groups, e.g. dg-categories), homotopy theory, sheaf theory… can be combined inside of a common flexible categorical framework, which elegantly subsumes previous point-set level techniques like model categories.
All the frames you are mentioning are good for intuition. I would say the deepest one is 4. and that everything falls into place cleanly once you formulate things in the language of infinity-category theory (at the price of a lot of technicalities to establish the “right” language). For example,
singular homology with coefficients in A can be characterised as the unique colimit-preserving infinity-functor from the infinity-category of spaces/homotopy types/infinity-grpoids/anima to the derived infinity-category of abelian groups which sends a one-point space (equivalently any contractible space) to A[0].
The derived infinity-category of abelian groups is itself in some sense the “(stable presentable) Z-linearization” of the infinity-category of spaces, although this is more tricky to state precisely and I won’t try to do this here.
Here are two more closely related results in the same circle of ideas. The first one gives a description (a kind of fusion of Dold-Thom and Eilenberg-Steenrod) of homology purely internal to homotopy theory, and the second explains how homological algebra falls out of infinity-category theory:
Consider functors E:S_* --> S_* from the infinity-category of spaces to itself which commutes with filtered colimits, carries pushout squares to pullback squares, sends the one-point space to itself, and the 0-sphere (aka two points!) to a discrete space. Then A=E(S^0) has a natural structure of abelian group, and E is an (infinity-categorical version of) the Dold-Thom functor and satisfies pi_n E(X)=H_n(X,A) (reduced homology). In particular, E(S^n) is an Eilenberg-Maclane space K(A,n).
The category of functors E:S_* --> S_* satisfying all the properties above except the one about E(S^0) being discrete is a model for the infinity-category Sp of spectra, i.e. the “stabilization” (in a precise categorical sense) of the infinity-category of spaces. From this perspective, the functors from the previous points are called the Eilenberg-Maclane spectra HA. Moreover, the infinity-category of spectra has a symmetric monoidal structure (the “smash product”), HR is naturally an algebra object for this structure whenever R is a ring, and it makes sense to talk about the infinity-category LMod(HR) of left HR-modules in Sp. Then LMod(HR) is equivalent (essentially by a stable version of the Dold-Kan correspondence) to the infinity derived category of left R-modules D(R). In other words, for homotopy theorists, (chain complexes,quasi-isomorphisms) are just a funny point-set model for HR-module spectra!
All of this is discussed in the first chapter of Lurie’s Higher Algebra, except the last point which is not completely spelled out because monoidal structures and modules are only introduced later on.
I should point out that this perspective is largely a reformulation of the results you already mentioned, and in themselves certainly do not bring new computational techniques for singular homology. However they show that 1) homological algebra comes out “structurally” from homotopy theory, which itself comes out “structurally” from infinity-category theory and 2) homological algebra (including in more sophisticated contexts than just abelian groups, e.g. dg-categories), homotopy theory, sheaf theory… can be combined inside of a common flexible categorical framework, which elegantly subsumes previous point-set level techniques like model categories.