The article already mentions the paper, Sets in Types, Types in Sets by Benjamin Werner which maps between Set/Type theories.

Another related and more approachable paper on the evolution of Type Theory and its relation to Set/Category theories is Types, Sets and Categories by John Bell.

Finally also see, Typed Lambda Calculus / Calculus of Constructions by Helmut Brandl for an excellent book-length but concise overview of CoC/CIC.

IMO, the above is required reading to understand theorem provers and proof assistants. In particular, Brandl's work is a must-read.

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