$\DeclareMathOperator\Sq{Sq}$Chapter 75 of Haynes Miller's book on algebraic topology contains a beautiful construction of the Steenrod squares $\Sq^i$.

Roughly speaking, it goes as follows. All cohomology groups here have $\mathbb{F}_2$-coefficients. Consider a based space $X$. The cyclic group $C_2$ of order $2$ acts on the product $X^2$ by switching the factors. We can then look at the Borel equivariant cohomology $H^{\bullet}_{C_2}(X^2,X \vee X)$. This is the relative cohomology of the Borel construction $X^2 \times_{C_2} EC_2$, which is a fiber bundle over $B C_2$ with fiber $X^2$. The fiber inclusion gives a map of pairs $\iota\colon (X^2,X \vee X) \hookrightarrow (X^2 \times_{C_2} EC_2,(X \vee X) \times_{C_2} EC_2)$, and thus a map $$\iota^{\ast}\colon H^{\bullet}_{C_2}(X^2,X \vee X) \rightarrow H^{\bullet}(X^2,X \vee X).$$ What Miller does is construction a natural transformation $P\colon \tilde{H}^n(X) \rightarrow H^{2n}_{C_2}(X^2,X \vee X)$ such that $$\iota^{\ast}(P(x)) = x \otimes x \quad \text{for all $x \in \tilde{H}^n(X^2)$}.$$ He then pulls $P(x)$ back along the diagonal map $\Delta\colon X \rightarrow X \times X$ to get $$P(x) \in H^{2n}_{C_2}(X) = H^{2n}(X \times BC_2) = (H^{\bullet}(X) \otimes \mathbb{F}_2[d])_{2n}.$$ The coefficients are the Steenrod squares of $x$.

He verifies some parts of the usual properties of the squares, but he omits a lot of important verifications:

- The fact that $\Sq^1$ is nonzero.
- The Cartan formula.
- The Adem relations

My question: where can I find a construction of the Steenrod squares using this kind of definition that verifies these properties? I like the fact that this works at the space level rather than the chain level. I also prefer to not get bogged down in signs since I'm still learning the Steenrod operations, so I would prefer to just do the squares.