Introduction to Proof via Type Theory

Question

Is there an introduction to mathematical proofs book that uses type theory instead of set theory? I'm aware of books like Hammack's Book of Proof or Epp's Discrete Mathematics with Applications but they emphasize the "$\in$" notation and corresponding naive principles of set-theoretic reasoning. I'm also aware of the existence of lecture notes for interactive theorem provers, but i would prefer a pencil-and-paper kind of learning experience of instead the approach using compiled and programing languages. I want to see the classic topics in the transition to advanced mathematics canon being recast using type theory, for example those topics in the subgenre of books mentioned, like the ubiquitous proof of the irrationality of the square root of two, equivalent statements to the well-ordering principle and maybe some epsilon-delta arguments from differential calculus.