Suppose you want to prove that homotopic maps induce the same morphisms in singular homology. One way to do that is the following : you have your homotopy $X\times I \to Y$, apply $Sing$ to it to get $Sing(X)\times Sing(I)\to Sing(Y)$, and then you have a natural map $\Delta^1\to Sing(I)$ which yields $Sing(X)\times \Delta^1\to Sing(Y)$, and since homology only depends on $Sing$, it's clear that it suffices to prove the following :
let $X\times\Delta^1\to Y$ be a simplicial homotopy, then the two maps $X\to Y$ induce the same map in simplicial homology.
To do that, it's again clear that it suffices to show that $X\to X\times \Delta^1$ is a homology isomorphism. One possible method of proof is to build the beginning of simplicial homotopy theory (but some purely formal bits) as follows :
1- Show it has the lifting property against Kan fibrations, by essentially proving the pushout product axiom; for that it suffices to check that for all $n$, $\partial \Delta^n \times \Delta^1\cup_{\partial \Delta^n \times \{0\}} \Delta^n\times \{0\}\to \Delta^n\times \Delta^1$ has the given lifting property. This can be done by hand, by expressing the given map as a composition of pushouts of horn inclusions.
2- Conclude by the small object argument that $X\to X\times \Delta^1$ is a retract of a cell-complex (built on $\Lambda^n_k\to \Delta^n$'s)
3- Prove that "induces an isomorphism on homology" is stable under retracts and pushouts and transfinite compositions.
4- Prove that $\Lambda^n_k$ and $\Delta^n$ both have zero homology.
Of these steps, only 1 and 4 have some "non conceptual" content, they contain some computations (for 1, you need to express explicitely the map as a pushout of horn inclusions, so you need to find those inclusions; for 4 you need to actually compute some homology, albeit quite simple)
But it seems to me that you can do this more quickly, by actually expressing directly $X\to X\times \Delta^1$ as some relative complex of horn inclusions, if that's possible; since this sort of computation is there anyways, if you can do it, you might as well bypass the whole argument.
So my first question is :
Is there an explicit construction of $X\to X\times \Delta^1$ as obtained by pushouts and transfinite compositions (and maybe a retraction) of horn inclusions $\Lambda^n_k \to \Delta^n$ ?
My second question is about the proof I sketched above, specifically about the computational points I noted :
Is there a way to bypass the computations ? More specifically, 1- is there a way to prove that $\partial \Delta^n \times \Delta^1\cup_{\partial \Delta^n \times \{0\}} \Delta^n\times \{0\}\to \Delta^n\times \Delta^1$ has the left lifting property against Kan fibrations without having to find out which horn inclusions do the right thing ? and 2- is there a way to prove that $\Lambda^n_k\to \Delta^n$ is a homology isomorphism without computing both homologies and discovering that they are $0$ ?
(note that for all these questions, the point is to avoid using powerful stuff, because the end goal is to prove some basic property : the homotopy invariance of homology; so of course I can't accept "well $|\Delta^n|$ is contractible and simplicial homology coincides with singular homology so $H_*(\Delta^n) = 0$" as that would help in no way what I'm trying to do)
That's not an answer to my specific questions, but I just thought that if the end goal is proving that $X\to X\times \Delta^1$ is a homology isomorphism, there's a much quicker way, although perhaps less formal, through Dold-Kan.
Indeed, $\mathbb Z[X\times \Delta^1]\cong \mathbb Z[X]\otimes \mathbb Z[\Delta^1]$ (here $\otimes$ is dimensionwise), and the Dold-Kan correspondance is monoidal, so $C_*(X\times\Delta^1;\mathbb Z)\simeq C_*(X;\mathbb Z)\otimes C_*(\Delta^1;\mathbb Z)$, where now $\otimes$ is the usual chain complex tensor-product.
So we're reduced to computing $C_*(\Delta^1;\mathbb Z)$ up to homotopy (note that $C_*(X;\mathbb Z)$ is a complex of projectives, so $C_*(X;\mathbb Z)\otimes- $ preserves quasi-isomorphisms), but by Dold-Kan this is entirely explicit, and one easily checks $C_*(\Delta^1;\mathbb Z)\simeq \mathbb Z$ (in degree $0$), from which the result immediately follows.