add telescopes and a bit of theory about them

I think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.

Open question: Telescopes generalize hlists to the dependent case. Should we get rid of hlists? Does anyone want to attempt porting hlist users over to telescopes? Restricting the dependency can actually be useful because it makes them easier to use.