Introduction to Type Theory in Agda

A course given at Midlands Graduate School 2024, Leicester, UK.
Todd Waugh Ambridge, April 2024


Please note that the materials on this page are subject to change.
You can do the exercises without needing to install Agda, by following these instructions:
  1. Create a new session on Agdapad,
  2. Click 'File -> Open File' and write '~/MGS2024/exercises1.lagda' (replace '1' with the exercise sheet number you wish to complete) then hit Enter,
  3. Click 'File -> Save as' and write '~/exercises1.lagda' (again replace '1' as necessary) and hit Enter,
  4. Press C-c C-l to load the file.
When you are finished, you can revisit the same session by writing down the session name and typing it in next time you use Agdapad.

Lecture 1: Introduction

Slides (spoiler-free). Handouts (with Agda spoilers). Agda code (spoilers!). Exercises. Solutions. Feedback form.

Lecture 2: Propositions as types

Slides (spoiler-free). Handouts (with Agda spoilers). Agda code (spoilers!). Exercises. Solutions. Feedback form.

Lecture 3: Dependent types and equality

Slides (spoiler-free). Handouts (with Agda spoilers). Agda code (spoilers!). Exercises. Solutions. Feedback form.

Lecture 4: Exploring equality

Slides (spoiler-free). Handouts (with Agda spoilers). Agda code (spoilers!). Exercises. Solutions. Feedback form.