CoC book like "Programming in Martin-Löf’s Type Theory"?

Stream: new members

[Dan Grigsby]

There's an out of print but freely downloadable book titled, "Programming in Martin-Löf’s Type Theory" that presents this version of type theory in roughly 100 pages, with another 100 pages of examples/applications, all using set theory and lambda calculus.

For me, this is about the right level of detail and mathematical sophistication. Is there a similar book for Calculus of Constructions? I'm enjoying learning Lean using @Heather Macbeth's book and think learning the fundamentals of how CoC works would be beneficial.

Thanks!