You forestalled some of what I would have posted...
Quillen's K-theory without topology
Steenrod algebras through combinatorics and representation theory (as opposed to, through topology)
Ext and Tor defined constructively, with Haskell code
Weyl's "Classical Groups" with the proofs of 1938 but the notations of 2010
Henri Lombardi's "Algèbre Commutative" in English
A documentation to Agda
