Generalize funS_id.
Add and prove canS_id_{l,r}, bijS_id.

MonoidComp:
Propagate new APi (from Function_sub).