speed

Typechecking some thing with agda-categories can get quite slow. Here's some things to keep in mind, and then ways to mitigate.

Known reasons for slowness:

1. Asking agda to work too hard: using lots of _ in equational proofs
2. Hard implicits: when you have a term that has a f ∘ g (or equivalent) that computes away, the "middle type" might no longer be visible at all in the fully evaluated goal.
3. Large files: it sure feels like typechecking isn't linear in the size of your file. Conjecture: I think Agda 'peeks' too much when it actually knows the full definition, and doesn't do it as much cross-modules.
4. Large interfaces: remember that it's not just the fields of a record that are on its interfaces, but all conservative extensions (aka definitions) are too.
5. Convenience modules: the lure of just being able to use . is so strong.
6. Inline proofs: you know that something's a proof, but Agda doesn't. It's all just values. And Agda is awful at sharing, so it's splay those all over.
7. Lack of sharing: you know you've typed the same expression over and over, but Agda doesn't.

Mitigation (and debugging) strategies:

1. Don't be so lazy, expand out those _
2. Take a look at your goals with all implicits shown and normalize fully. If your implicits are filled with expanded records instead of the name of the thing you had expected Agda to provide, it's because Agda chose to reconstruct it. You should provide those explicitly, to turn the problem into one of checking instead of inference.
3. Split things up!
4. Split the helper routines into its own module (and its own file). Some downstream code will use these a lot, some very little. That saves a lot of time for that latter downstream code. If you have to import some huge module, then use using, this cuts things down significantly.
5. These feel like they should be no cost, but that's not true. Agda copies everything (and does some re-checking). This bloats the size of interfaces hugely. agda-categories uses a lot of these "convenience" modules (we didn't realize how expensive they were). It looks like if you make the convenience modules private then it's not as bad, as they don't appear on the interface.
6. Use a lot of where clauses where you name your proofs. Or put them in private blocks above your record. It seems that defining some things via copatterns instead of an explicit record might help too.
7. For long equational proofs, some sub-expressions might take .5 seconds to typecheck -- but they appear 25 times in your proof... Agda doesn't go hash-consing or anything like that. It's quite well-known to do the opposite (let bindings get splayed out, the horror!). Go ahead and give names (and types) to oft repeated intermediate expressions (via where not let, of course).

Lastly: reasonably often, it's not your code that is the biggest culprit, it is the library itself. There are known issues in the Monoidal and Bicategory hierarchy that have not yet been fixed. PRs for these would be most welcome.

It's also good to read NAD's AIM 32 notes on efficiency and the Performance Debugging section of the manual.