G. Allais

And in `Codata.*` we use `map-map-fusion`.

:+1: That is consistent with the convention we use

I see that we also have [map-++-commute](https://agda.github.io/agda-stdlib/Data.List.Properties.html#3178) instead of `map-++`.

`Data.List.Categorical`? `foldMap` is essentially `traverse` with the writer monad.

I don't think it's a low hanging fruit. `Foldable` cannot fit in a record like Functor or Monad do because of size issues!

Should we at least have a warning (turned off by default if it is judged too verbose) whenever we shadow a previous toplevel declaration?

Isn't this the usual unification issue when you're trying to reconstruct the arguments of a function rather than a (type or data) constructors? ``` f : Nat → Nat f...

This is the relevant lossy unification bit: https://github.com/agda/agda/blob/7bda16229ef4728761a9b538f17bb63e20777618/src/full/Agda/TypeChecking/Conversion.hs#L200-L207

The fact the equality constraint is relative to a specific domain (in order to be as tight a constraint as possible) rather than absolute.

I have tried defining ``` record Sum n {ls} (as : Sets n ls) : Set _ where field index : Fin n value : Projₙ as index ``` but...