Lectures on Agda

This is a course on Agda I gave at Dalhousie University in Winter 2021. Unlike most other such materials that I have seen, this course focuses on using Agda for mathematics, rather than program verification. I deliberately did not use the standard library, focusing instead of developing all concepts from scratch. Frank Fu was the teaching assistant for this course, and he developed many of the materials, including the installation instructions, homeworks, and projects.

This is a basic course. One important topic I did not cover is the use of setoids, i.e., sets equipped with an equivalence relation. One arguably needs this to do "real" mathematics in Agda, because sooner or later one will need to take a quotient of a set, which is basically impossible if one works with the native Agda equality. Many other topics were also not covered, such as proof irrelevance, coinduction, and more.

If a "+" sign appears after a lecture link below, you can click on it to see a list of Agda topics covered in the lecture, with links to the relevant Agda documentation.

Agda is named after a chicken, just like Coq. The picture above is of one of my chickens, Vanilla. Maybe one day I will name a proof assistant after her. Vanilla and some of her fellow chickens are also mentioned in the lectures on "records" below.

Installation instructions

• Installing Agda on Linux:
  • Video instructions
  • Written instructions
• Installing Agda on Mac:
  • Video instructions
  • Written instructions
• Installing Agda on Windows:
  • Video instructions
  • Written instructions

1. Introduction

• Lecture 1.1 - Agda demo and questions (17:55)

Agda files from class:

• Demo.agda

2. Sets vs. types, lambda calculus

• Lecture 2.1 - Sets vs. types (32:29)
• Lecture 2.2 - Lambda calculus introduction (17:56)
• Lecture 2.3 - Student questions (9:07)
• Lecture 2.4 - Lambda calculus introduction, continued (9:58)
• Lecture 2.5 - Lambda calculus: Types (30:39)
• Lecture 2.6 - Lambda calculus: Terms (9:50)
• Lecture 2.7 - Student questions (9:04)
• Lecture 2.8 - Typing judgements: examples (50:01)
• Lecture 2.9 - Student questions (9:42)

Lecture notes:

• lecture2.pdf

3. Typing rules, Curry-Howard isomorphism

• Lecture 3.1 - Typing rules (16:36)
• Lecture 3.2 - Typing rules example (19:37)
• Lecture 3.3 - The Curry-Howard isomorphism (14:58)
• Lecture 3.4 - Student questions (5:23)
• Lecture 3.5 - The BHK interpretation (25.48)
• Lecture 3.6 - The remaining logical connectives (25:57)
• Lecture 3.7 - Student questions (27:24)

Lecture notes:

• lecture3.pdf

4. Inductive types

• Lecture 4.1 - Inductive types (53:36)
• Lecture 4.2 - Student questions (19:59)

Lecture notes:

• lecture4.pdf

5. Agda basics

• Lecture 5.1 - Emacs tutorial and Agda mode (5:25)
• Lecture 5.2 - Lambda terms in Agda (17:49)

  Agda topics covered:

  • Postulates
  • Refinement: working with terms with "holes".
  • Lambda notation
  • Agda mode Emacs commands: (C-c C-l), (C-c C-,), (C-c C-r), (C-c C-.)
  • Backslash escape sequences for typing Unicode characters: \lambda
• Lecture 5.3 - Booleans, some functions, double negation theorem (21:30)

  Agda topics covered:

  • Inductive datatypes: Bool
  • Writing comments in Agda files (using "--")
  • Defining functions by case distinction
  • Evaluating an expression: C-c C-n
  • Automatic splitting into cases: C-c C-c
  • ∀ notation
• Lecture 5.4 - The natural numbers, addition (7:46)

  Agda topics covered:

  • Backslash escape sequences for typing Unicode characters: \bN
  • Inductive datatypes: the natural numbers
  • Recursive functions and termination checking
• Lecture 5.5 - Student questions (4:31)

  Agda topics covered:

  • Importing another file (we will cover this in more detail later)
• Lecture 5.6 - Recap of booleans and BHK interpretation of equality (7:42)

  Agda topics covered:

  • The BHK interpretation of equality
  • Show the type of an expression: C-c C-d
  • The collection of all types is called Set
• Lecture 5.7 - Natural numbers, commutativity of addition (38:40)

  Agda topics covered:

  • The BUILTIN NATURAL pragma: writing 2 instead of succ (succ zero)
  • Comments in Agda: block comments "{- ... -}" and one-line comments "-- ..."
  • Alternative notations for quantifiers
  • Definitions local to a function body: "where" syntax
  • Agda's use of indentation to delimit blocks of code
• Lecture 5.8 - Student questions (9:34)
• Lecture 5.9 - Recap from last time (1:44)
• Lecture 5.10 - Emacs split window and Agda documentation (5:13)

  Agda topics covered:

  • Emacs command for split windows: C-x 2
  • Where to find the Agda documentation
• Lecture 5.11 - Implicit arguments (underscore) (8:29)

  Agda topics covered:

  • Implicit arguments using underscore "_"
  • C-c C-, will sometimes show constraints
• Lecture 5.12 - Identifiers (11:22)

  Agda topics covered:

  • Identifiers can consist of almost any characters
• Lecture 5.13 - Infix operators and precedence (15:43)

  Agda topics covered:

  • Infix operators and precedence
• Lecture 5.14 - Student questions (6:27)

Agda files from class:

• Lambda.agda
• Equality.agda
• Bool.agda
• Nat.agda

6. Inductive predicates

• Lecture 6.1 - What is a predicate? (3:34)
• Lecture 6.2 - An inductive family of sets: Fin n (12:07)

  Agda topics covered:

  • Inductive families of sets, an example of an indexed datatype
• Lecture 6.3 - Implicit arguments (curly braces) (17:21)

  Agda topics covered:

  • Implicit arguments using curly braces {x : A}
• Lecture 6.4 - An inductive predicate: Even n (10:42)

  Agda topics covered:

  • Inductive predicates, and example of an indexed datatype
• Lecture 6.5 - Equality on ℕ and Bool (5:47)

  Agda topics covered:

  • Equality is also an example of an indexed datatype
• Lecture 6.6 - Recap of inductive predicates (9:01)
• Lecture 6.7 - Equality on any set (12:05)

  Agda topics covered:

  • Inductive predicates
  • Implicit arguments
• Lecture 6.8 - Theorems on transitivity, symmetry, context (30:37)

  Agda topics covered:

  • Dot patterns
• Lecture 6.9 - Student questions (4:42)
• Lecture 6.10 - Dot patterns: evenness predicate (26:57)

  Agda topics covered:

  • Dot patterns
  • Emacs commands: C-c C-a to auto-complete a goal
• Lecture 6.11 - Equality: substitution, and using equality in a proof (19:17)
• Lecture 6.12 - Student questions (4:43)

  Agda topics covered:

  • Implicit arguments
• Lecture 6.13 - Recap of equality (6:05)
• Lecture 6.14 - Syntactic sugar for equational proofs (9:29)

  Agda topics covered:

  • Syntactic sugar

Agda files from class:

• Predicate.agda
• Equality-new.agda
• Even.agda
• Nat.agda

7. Logical connectives, part 1

• Lecture 7.1 - True and False (11:58)
• Lecture 7.2 - Conjunction ("and") (15:41)
• Lecture 7.3 - Student questions (9:44)
• Lecture 7.4 - Recap (3:42)
• Lecture 7.5 - Ex falsum quodlibet (7:52)

  Agda topics covered:

  • Absurdity patterns
• Lecture 7.6 - Disjunction (20:17)
• Lecture 7.7 - Negation (11:27)

  Agda topics covered:

  • Lambda notation

Agda files from class:

• Proposition.agda
• Nat.agda

8. Interlude: The Stone-Tarski interpretation of intuitionistic logic

• Lecture 8.1 - Constructive logic part 1 (8:00)
• Lecture 8.2 - Recap (2:30)
• Lecture 8.3 - Open subsets of ℝ² (18:51)
• Lecture 8.4 - The Stone-Tarski interpretation of intuitionistic logic (9:45)
• Lecture 8.5 - Examples of Stone-Tarski interpretation (16:49)
• Lecture 8.6 - Student questions (5:07)

Lecture notes:

• lecture8.pdf

9. Logical connectives, part 2

• Lecture 9.1 - Recap (1:50)
• Lecture 9.2 - The "exists" quantifier (8:44)
• Lecture 9.3 - Example: there exists an even number (3:43)
• Lecture 9.4 - Syntactic sugar for "exists" (4:26)
• Lecture 9.5 - Redefining "and" as a special case of "exists" (9:51)
• Lecture 9.6 - Example: divisibility (10:00)
• Lecture 9.7 - Student questions (8:53)

Agda files from class:

• Proposition.agda

10. More Agda features

• Lecture 10.1 - Alternate notation for indexed data types (13:56)

  Agda topics covered:

  • Indexed datatypes
• Lecture 10.2 - Namespaces: the Agda module system (30:38)

  Agda topics covered:

  • The module system
• Lecture 10.3 - Student questions (10:50)
• Lecture 10.4 - More on modules: private, public, using, renaming, module assignment (29:27)

  Agda topics covered:

  • Private definitions ("private")
  • Name modifiers ("using" and "renaming")
  • Re-exporting names ("public")
• Lecture 10.5 - "With" abstraction, part 1 (21:21)

  Agda topics covered:

  • "With" abstraction
  • NATPLUS and NATTIMES pragmas
• Lecture 10.6 - "With" abstraction, part 2 (15:43)

  Agda topics covered:

  • "With" abstraction
• Lecture 10.7 - "Rewrite" (12:30)

  Agda topics covered:

  • "Rewrite"
  • (Not to be confused with the --rewriting option, which we will not cover)
• Lecture 10.8 - Case split on implicit arguments (6:04)

  Agda topics covered:

  • Implicit arguments
• Lecture 10.9 - Pattern matching lambda (11:36)

  Agda topics covered:

  • Pattern matching lambda
• Lecture 10.10 - Overlapping patterns (8:15)

  Agda topics covered:

  • Overlapping patterns: see case trees

Agda files from class:

• Lecture18.agda
• Modules.agda
• Lecture19.agda

11. Tactics and decidability

• Lecture 11.1 - Tactics using equality (33:19)
• Lecture 11.2 - Tactics using Maybe, part 1 (20:53)
• Lecture 11.3 - Tactics using Maybe, part 2 (27:13)
• Lecture 11.4 - Decidability (16:11)
• Lecture 11.5 - Caution about auto-complete (2:02)

  Agda topics covered:

  • Auto-completion
• Lecture 11.6 - A better datatype for Decidability (6:36)
• Lecture 11.7 - Lists (21:32)
• Lecture 11.8 - Example: decidable equality for lists, using Bool (13:13)
• Lecture 11.9 - Example: decidable equality for lists, using Decidable (6:02)
• Lecture 11.10 - Student questions (1:26)

  Agda topics covered:

  • How to change the timeout for automatic proof search.
• Lecture 11.11 - A better version of decidable equality for lists (11:02)
• Lecture 11.12 - Decidable equality for lists of lists (6:56)

Agda files from class:

• Tactics.agda
• Decidable.agda

12. Records and overloading

• Lecture 12.1 - Motivation for overloading (8:09)
• Lecture 12.2 - Overloading, part 1 (3:43)
• Lecture 12.3 - Records, part 1 (20:19)

  Agda topics covered:

  • Record types
• Lecture 12.4 - Student questions (2:19)
• Lecture 12.5 - Records, part 2 (26:08)

  Agda topics covered:

  • Record types
• Lecture 12.6 - Records: Student questions (5:19)
• Lecture 12.7 - Two example monoids (4:48)
• Lecture 12.8 - Monoid structure on a set (8:19)
• Lecture 12.9 - Using monoids, naively: without instance arguments (12:52)
• Lecture 12.10 - Introduction to instance arguments (19:30)

  Agda topics covered:

  • Instance arguments
• Lecture 12.11 - Instance declarations (7:40)

  Agda topics covered:

  • Instance declarations
• Lecture 12.12 - Monoids with infix notation (14:08)
• Lecture 12.13 - Recap of monoids (7:13)
• Lecture 12.14 - Monoid instance for cartesian product (24:58)

  Agda topics covered:

  • Instance declarations

Agda files from class:

• Overloading.agda
• Records.agda
• Monoids.agda

13. Universes

• Lecture 13.1 - Universes, part 1: Set, Set₁, Set₂, etc. (8:25)

  Agda topics covered:

  • The Agda sort system
• Lecture 13.2 - Universes, part 2: lists of sets and other large things (33:57)

  Agda topics covered:

  • The Agda sort system
• Lecture 13.3 - Universe polymorphism (12:00)

  Agda topics covered:

  • Universe levels
• Lecture 13.4 - Student question (4:34)

  Agda topics covered:

  • Universe levels
• Lecture 13.5 - Recap (3:25)
• Lecture 13.6 - Example: Monoids as a proper class (11:31)
• Lecture 13.7 - Student questions: Emacs commands for copy and paste (2:25)

  Agda topics covered:

  • Emacs commands for copy and paste: C-k and C-y

Agda files from class:

• Universes.agda

14. Application: Generators and relations for monoids

• Lecture 14.1 - Remarks about formalizing mathematics in Agda (3:34)
• Lecture 14.2 - Introduction to generators and relations (24:53)
• Lecture 14.3 - Student questions (3:06)
• Lecture 14.4 - Generators, relations, contexts, entailment (47:25)

  Agda topics covered:

  • Parameterized modules
• Lecture 14.5 - Recap and proof of cong-power (5:01)
• Lecture 14.6 - Grouplike monoids (16:18)
• Lecture 14.7 - A tactic for associativity (24:04)
• Lecture 14.8 - Examples of general-assoc (5:59)
• Lecture 14.9 - Student questions (1:28)

Lecture notes:

• lecture14.pdf

Agda files from class:

• Word.agda

Exercises

This course had a number of problem sets, designed by Frank Fu and me. Some of them were called "homework", which the students were allowed to collaborate on, and others were called "projects", which the students had to do individually, like an exam.

If you are learning Agda, you might find these homeworks and projects fun. Each of them consists of one or more files with "holes" for you to fill in. In some of them, you also have to come up with your own definitions and/or lemmas. I will not post the solutions, and I ask that you do not publicly post the solutions either. But of course you can use Agda to check whether you did the problems correctly.

• Homework 1 - Booleans and natural numbers
• Homework 2 - Propositional logic and inductive predicates
• Homework 3 - Subtraction, divisibility, and factorials
• Homework 4 - Lists, sorting, and tactics
• Project 1 - Natural numbers: properties of multiplication and less-than
• Project 2 - Propositional logic: derivations and the soundness theorem
• Project 3 - Integers and group theory
• Project 4 - Induction principles