Explain/remove concepts/notations

[WhatisRT]

Unavoidable (Do later)

Things that we can either not avoid for technical reasons or because they would make things massively more difficult. These need to be explained.

• record definitions, record syntax for (de)constructing values
• What to do about Set in the PDF? #444

Potentially avoidable (Do later)

Things that can be avoided/hidden at some cost. That cost needs to be weighed against the cost of adding an explanation (which also makes the document less accessible).

• open for records
• implicit arguments
• Σ
• data
• λ where syntax
• Copatterns

Should be avoided (Do soon)

These are things which aren't too difficult to avoid, are completely custom or only used in an FP context. Those need to have a very good reason to pay the cost of adding an explanation/increasing the barrier to entry.

• module syntax
• _≗_ (fig 5)
• _⟪$⟫_ (fig 25) (afaik, this no longer appears in fig 25)
• _<$>_ (fig 25)
• sp-∘
• to-sp
• uncurry
• foldr

Need explanations/cleanup (Do soon)

Things that definitely we want to use but still should have a (potentially very short) explanation. Some things in here may also be improved by being renamed. Some renames may require type classes or other mechanisms.

Name is probably good:

• _⊎_
• _∷ʳ_
• _⁻¹
• _∣_

May benefit from a rename:

• _↾_
• _↾'_
• _⊖_
• _∘₂_

Needs rename:

• Σᵐᵛ -> ∑, maybe ∑ᵛ?
• mapˢ - since we now have a Functor class, we can make an
  instance and write map instead (this is difficult, see Make Functor instance for ℙ_ #322)
• ∅ᵐ -> ∅
• ❴_❵ᵐ -> ❴_❵
• ℚ.0ℚ -> 0ℚ (0ℚ -> 0 via literal overloading later)
• _ℚ.≥_ -> _≥_ or _≤_
• filterᵐ -> filter (or maybe something else?)
• sucᵉ -> ... + 1
• Naming of mapPartial #446

[WhatisRT]

For now, we should focus on putting out the biggest fires. This is anything in the Should be avoided and Needs rename sections.

[williamdemeo]

@WhatisRT Thank you for reorganizing this issue and making the priorities clear. 🚀 👍🏼

[williamdemeo]

@WhatisRT why do you want to be forced to use parentheses around A ⇀ B? I thought one nice feature of our ⇀ symbol was that we didn't need parens.

[omelkonian]

@WhatisRT why do you want to be forced to use parentheses around A ⇀ B? I thought one nice feature of our ⇀ symbol was that we didn't need parens.

I remember adding such parentheses in my first cleanup PR; it is very easy to confuse it with the normal function space (esp. in some fonts where they are almost identical) and I also recall the fixity to be very brittle (you don't know if you want a map from functions or an input map...). To sum up, yes please always use parantheses when a map is part of a larger (function-with-arguments) type.

[WhatisRT]

Closing in favour of #444, #446 and #447.