This document is not (yet) a full course script. Instead, it is meant as an additional resource that systematizes the considered primitives, definitions, and constructions. The author invites readers to submit comments or pull requests via this GitHub Repository.