Transport of the standard nonvanishing into the ambient category

The nonvanishing of the standard super object carried into any ambient symmetric ℂ-linear category with an odd invertible line, in the three parts below: the Koszul sign of a permutation of slot labels (Signs.lean), the letter systems that make the action of the group algebra model independent (Letters.lean), and the two systems and the conclusion they force (Standard.lean).