Course material 2010–11

Categorical Logic

Principal lecturer: Dr Sam Staton
Taken by: MPhil ACS
Syllabus

Exercises

• First exercise sheet.
• Second exercise sheet.
• Third exercise sheet.
• Fourth exercise sheet.

Online resources

I have recommended some texts in the syllabus. Here are some additional links:

• Categorical Logic by Andy Pitts.
• nLab.

Agda

The Agda language is available here and is already installed on the MPhil machines.

You may like to read these Agda notes by Ulf Norell.

There is also a guide to Unicode input for the Agda emacs mode.

I will put sample source code and exercises in this directory.

Exams

• 25% of the marks for this course will be awarded for completing the assessed Agda exercises.
• 75% of the marks will be given for a take-home exam.