# Lectures on Agda

## Peter Selinger Dalhousie University

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:
• Installing Agda on Mac:
• Installing Agda on Windows:

## 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.