Cup product is natural, unital and associative

Face restriction commutes with postcomposition. On a $(p+q)$-simplex $\sigma$, evaluation of $f^{\mathrm{♯}}(\phi ⌣\psi )$ is $\phi (f\sigma [0,\dots ,p])\psi (f\sigma [p,\dots ,p+q])$, which is the evaluation of $f^{\mathrm{♯}}\phi ⌣f^{\mathrm{♯}}\psi$. Precomposition is linear and commutes with positive coboundary because each face does; it therefore induces the same multiplicative equality on cocycle classes. On a vertex $x$, $f^{\mathrm{♯}}\mathbf{1}(x)=\mathbf{1}(f(x))=1$, giving the unit identity on classes.

On a $(p+q+r)$-simplex $\sigma$, both $(\phi ⌣\psi )⌣\eta$ and $\phi ⌣(\psi ⌣\eta )$ evaluate to $\phi (\sigma [0,\dots ,p])\psi (\sigma [p,\dots ,p+q])\eta (\sigma [p+q,\dots ,p+q+r])$. Associativity in $R$ makes the results equal. Bilinearity extends this identity to finite sums of homogeneous cochains; descent gives associativity in the cohomology ring. Together with step 1.1 this proves the graded-ring homomorphism claim.

If $f$ and $g$ are homotopic, [F3] gives equality on each homogeneous group. Every element of the graded direct sum has finite support, so the two ring homomorphisms are equal. Degree-zero factors in step 2.1 merely shorten blocks to vertices. The same formula covers degenerate simplices and points. Empty spaces and the zero ring give zero cochains and the stipulated zero-ring unit; any existing pullback still preserves this unit. All formulas are prescribed, so no AC is required.