And if you want to see worked examples elaboration of dependent types then the `elaboration-zoo` is a great thing to look at:

https://github.com/AndrasKovacs/elaboration-zoo

I've also got an incomplete project that aims to present a more expanded set of implementations then the elaboration zoo: https://github.com/solomon-b/lambda-calculus-hs