alternating face map deduplication

Stream: condensed mathematics

[Johan Commelin]

I just replace all my ad hoc alternating face maps by the definition that Adam made, which is functorial and the one that should end up in mathlib.