Create a contributor's guide

[sstucki]

(Prompted by the discussion in https://github.com/agda/agda-categories/pull/304#issuecomment-905410931.)

There are some guidelines in the README.md about what idioms to use and to avoid, but there are also a bunch of non-trivial patterns (like the use of the sym-* fields, or general strategies for avoiding bad performance) that don't seem to be documented in the repo. These should probably all go into a contributors guide.

Until there's such a guide, we could maybe at least collect important points here.

[sstucki]

I'll start: apparently, its a bad idea to inline long equational proofs in record definitions.

• There's a Zulip conversation on the topic.
• There's also a short discussion in https://github.com/agda/agda-categories/pull/304#issuecomment-905410931.

[JacquesCarette]

• don't use let-in because that's just syntactic sugar, and it will get expanded out / duplicated everywhere. It might be ok for open and giving short names meant for humans.
• don't put module versions of a record in records all over the place. These make the end results a lot bigger, and make typechecking time go up quite a bit too. [Note: the paper explicitly advocates for this pattern! It is indeed super-convenient, but also very bad for efficiency.]
• be very sparing with open public. This can be convenient at times, but can also really pollute the name space and make interoperability complicated
• do use using qualifiers, both at the top and for local modules. These end up in the signature of the modules, and can have a knock-on effect on size.
• avoid putting too many utilities directly in a record. Instead, go for minimal records and a utility module that adds them all. Then users can choose to bring them in at the use site.