Meta-issue: Revision of FunctionSurj

[TentativeConvert]

I collect here things that need to happen in FunctionSurj

• add zeroeth level to introduce notation f : A → B for functions or try make this notation visible in level 1 – see #54 (comment)
• decide whether we can implement polyrith, and if not, whether we want to keep manual linear_combination in level 6; if not: delete/replace this level
• swap levels 4 (right inverse) and 5 (left inverse): the fact that left inverse is defined in terms of right inverse is already obvious in current level 4 to anyone who cares to unfold the definition
• add hints to levels 4, 6, … ? …
• Marcus: rewrite story