Formalizing and solving exercises form the book Type Theory and Formal Proof