When I started learning Agda about a year ago I think I tried all available tutorials and each taught me something new.
You should probably give Coq a try, because it has a larger user base and there are two nice books available for it:
- Coq’Art – slightly dated, but beginner friendly
- Certified Programming with Dependent Types
Software Foundations is also very nice.
The nice thing is that the theories Agda and Coq are based on are somewhat similar, so many examples can be translated from one to another. Programming in Martin-Löf’s Type Theory is a really nice and readable introduction to the dependent type theory, it can clear some things for you.
It would help to know what do you mean by “real world algorithms”. Many example developments are described in papers which mention Agda.