Is there any book that teaches the basics of Type Theory and Calculus of Inductive Constructions (CIC) and also shows a construction of ZFC (or preferably NBG) in CIC?

I only found the paper "Sets in types, types in sets" by Benjamin Werner, but it assumes that the reader knows type theory.

Thank you for your attention!