For the last few years we have been working on a book about session types. Thinking about how to present the basic definitions and material has led us to a new understanding of several topics, including: coinductive definitions of infinite session types; the definitions of linear and sharable session types; some small new ideas about subtyping; the details of the propositions-as-types approach to session types. This talk will summarise and highlight a few insights that we have gained along the way.