tt101 An introduction to dependent types with Agda. Integers, booleans, lists, vectors and their properties.