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
Nice. Your github repository on lambda calculus looks quite comprehensive. If you add detailed notes on each of the items, you could easily turn it into a book titled, "Type Theories using Lambda Calculus with Implementations in Haskell" ;-)
Thanks! My goal is to turn it into an interactive website like https://1lab.dev but a book would be cool too.