The standard library aims to contain all the tools needed to easily write both programs and proofs. While we always try and write efficient code, we prioritise ease of proof over type-checking and normalisation performance. If computational performance is important to you, then perhaps try agda-prelude instead.
If you would like to suggest improvements, feel free to use the Issues tab. If you would like to make improvements yourself, follow the instructions in HACKING.
You can browse the library source code in glorious clickable html here.