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.

• [x] record definitions, record syntax for (de)constructing values
• [ ] Set (could be renamed, or we could potentially even use Agda's Prop)

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).

• [x] open for records
• [ ] implicit arguments
• [x] Σ
• [x] data
• [x] λ where syntax

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.

• [ ] Copatterns
• [x] module syntax
• [x] _≗_ (fig 5)
• [x] ~_⟪$⟫_ (fig 25)~ (afaik, this no longer appears in fig 25)
• [x] _<$>_ (fig 25)
• [ ] sp-∘
• [ ] to-sp
• [x] uncurry
• [x] 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:

• [x] _⊎_
• [x] _∷ʳ_
• [x] _⁻¹
• [x] _∣_

May benefit from a rename:

• [ ] _↾_
• [ ] _↾'_
• [x] _⊖_
• [x] _∘₂_

Needs rename:

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