Oops, I forgot to reply all. Below is my reply.
To follow up, by "sha256Compress : Word256 × Word512 -> Word256" I mean that sha256Compress is a function that takes two arguments, the first being a 256 bit word and the second being a 512 bit word, and returns a 256 bit word (or equivalently sha256Compress is a function that takes a pair as input, the first component being a 256 bit word and the second component being a 512 bit word, and returns a 256 bit word).
sha256Compress is meant to be the compression function defined by the SHA256 standard, though nothing here depends on anything more that its type signature.