types+grammar: finishing appendix A, which finishes first draft of the book