[ ] 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
I collect here things that need to happen in FunctionSurj
unfoldthe definition