- basics - syntax: lambda, pi, Set, Seti - datatypes: Nat - pattern matching: _+_ - implicit arguments - in lambda, pi and app - go figure - named implicit - inductive families - Vec - dot-patterns - with - parity - module system - open - import - parameterised modules - instantiation - local definitions - records - projections - eta