Course page for Type Theory & Coq 2016–2017