Category Theory and Coalgebra (NWIIMC036), spring 2020
Lecturers:
Jurriaan Rot,
Bart Jacobs
General information on this course can be found in the
studiegids.
Contents of this course webpage

Please register for this course in order to receive (email)
announcements. Relevant course information will be provided here.

The first graded homework has been posted on brightspace, deadline April 15th.

In the fourth quarter, the course will continue online, with prerecorded video lectures, notes, exercises offered via brightspace.
There will be no lectures, but there is a weekly online question hour on Wednesdays 10:30. All details and material will be provided
via brightspace.
 The course runs officially in weeks 612 and 1622 of 2019.
 Lectures take place in HG00.086 on Mondays 13:30  15:15. The first lecture takes
place on February 3rd.
 Exercise classes take place in MERC I 00.28 on Wednesdays 10:30  12:15
 Lectures will be in taught in English.
 The final exam will be held on Monday 22 June, 12:4515:45, in HG00.071.
 The resit will be held on Monday 13 July, 12:4515:45.
 There will be two assignments, which also count towards the final grade and are
mandatory, one halfway during the course and one by the end. These will be announced in due time.
For general information about coalgebras see Bart Jacobs' book,
a draft of which is available here
(referred to as [Jacobs] below),
or Jan Rutten's book
(referred to as [Rutten] below).
We will refer to parts of both books.
We also use additional material, such as slides, handouts, and
research papers on coalgebra. All material will be made available electronically
via this webpage, or distributed during class. Pointers to the relevant literature
are in the Lectures Overview section below.
We also recommend the tutorial on coalgebras and coinduction by Bart Jacobs and Jan Rutten. See here.
 Basic theory of category theory and coalgebras (5 lectures)
 streams
 categories, functors, natural transformations
 coalgebras
 Coinduction: applications and advanced topics (4 lectures)
 relation lifting and bisimulation
 coinduction
 algorithms for equivalence and minimisation of automata
 Monads and probability (3 lectures)
 probabilistic computation
 monads
Details for each lecture and suggested exercises will be posted here during the course.
For a rough impression see the webpage of 2018; the programme
will change however.

Lecture 1, Monday 3 February, 13:3015:15, in HG00.086
 Topic: Course overview, introduction to coalgebra, first examples.
 Literature: tba
slides (first part), notes
(second part). Optional, for more background: Preface and section 1.1 of [Jacobs], Chapter 6 of
[Rutten].
No exercise class on Wednesday 5 February
 Lecture 2, Monday 10 February, 13:3015:15, in HG00.086
 Topic: Streams and coinduction
 Defining streams.
 Proving equivalence with bisimulation and coinduction.
 Stream systems.
 Literature: notes. Also see 7.1  7.4 of [Rutten], for now excluding the parts we haven't covered, in particular the stuff on bisimulations of stream systems in 7.1. Theorem 96 in 7.4 is the same as our coinduction principle: the relation ~ is defined
by s ~ t iff there is a bisimulation containing (s,t).)
Exercise class, Wednesday 12 February, 10:3012:15, in MERC I 00.28
 See here for the exercises. If you can't get enough of it, there's plenty more in [Rutten]...
 Lecture 3, Monday 17 February, 13:3015:15, in HG00.086
 Topic: Coalgebras for Set functors
 Functorial constructions.
 Functors on Set, polynomial functors.
 Coalgebras for a functor.
 Literature: 2.2 (polynomial functors, basic examples of coalgebras: deterministic automata, trees) and a bit of 2.1 in [Jacobs]; also, for the first part, see section 1.4 of the tutorial by Jacobs and Rutten
Exercise class, Wednesday 19 February, 10:3012:15, in MERC I 00.28
 See here for the exercises.
No lecture on Monday 24 February. Also no exercise class on Wednesday 26th.
 Lecture 4, Monday 2 March, 13:3015:15, in HG00.086
 Topic: Intro category theory (I)
 The definition of the notion of category
 Many elementary examples of categories
 Functors, as arrows between categories
 Literature: we recommend Steve Awodey's book Category theory.
Exercise class, Wednesday 4 March, 10:3012:15, in MERC I 00.28
 See here for the exercises.
 Lecture 5, Monday 9 March, 13:3015:15, in HG00.086
 Topic: Intro category theory (II)
 List functor from Sets to the category of monoids
 Initial, final objects
 Isomorphisms; initial&final objects unique up to isomorphism
 Products, coproducts
 Category of coalgebras; Lambek's lemma (the final coalgebra is an isomorphism)
 Literature: we recommend Steve Awodey's book Category theory.
Exercise class, Wednesday 11 March, 10:3012:15, in MERC I 00.28
 See here for the exercises.
 Lecture 6 (scheduled Monday 16 March, but lecture notes only)
 Topic: Final Coalgebras and Bisimulation
 Final coalgebras
 Bisimulations, coinduction
 Automata as coalgebras
 Literature: notes.
Exercise class and question hour, Wednesday 18 March, 10:3012:15, online
 See here for the exercises.
 Lecture 7 (short lecture), week 16:
 Topic: Natural transformations
 Final coalgebras
 Bisimulations, coinduction
 Automata as coalgebras
Exercise class and question hour, Wednesday 15 April, 10:3012:15, online
 Lecture 8, week 17:
 Topic: Nondeterministic systems
 Labelled transition systems, bisimulations
 Nondeterministic automata and determinisation
 Equivalence of nondeterministic automata via bisimulations up to congruence
Exercise class and question hour, Wednesday 22 April, online
 Lecture 9, week 19:
 Topic: Algebras
 Algebras for a functor
 Induction and recursion by initiality
 Terms as an initial algebra
Exercise class and question hour, Wednesday 6 May, online
Course description:
In this course, you will learn how to use category theory and coalgebra to study the foundational structure underlying several core concepts in computer science, such as statebased systems and automata and the behaviour of programs and programming languages. Category theory is an abstract mathematical language which organises and unifies numerous concepts in computer science and logic. For instance, it underlies the functional programming language Haskell, allows us to formulate datatypes such as streams and trees, and it provides a clear distinction between specification and implementation. The language of category theory has become standard throughout theoretical computer science.
The theory of coalgebras uses category theory to provide an elegant and very general notion of statebased system, such as automata and finitestate machines. Statebased systems are used widely to model, e.g., digital hardware, software programs, network protocols, distributed systems, programming language semantics, and in program correctness and verification.
In coalgebra, a system is viewed as a black box where knowledge of the system's state can only be obtained by observing the external behaviour. The type of observations and transitions in the external behaviour is specified by the system type. The theory of universal coalgebra provides general definitions of observable behaviour and bisimilarity that can be instantiated for concrete system types, as well as a powerful and fascinating reasoning principle called coinduction (a notion that is dual to the well known induction principle). The principle of coinduction has led to new, efficient algorithms for, e.g., language equivalence of nondeterministic automata.
This course develops the basics of category theory, with a strong emphasis on their use in coalgebra. We will see how various types of systems can be modelled as coalgebras, and how coinduction can be applied to them. These systems include basic datatypes, such as infinite streams and trees, and many types of automata (deterministic, nondeterministic, probabilistic, ...). Next, a number of fundamental notions such as language equivalence of automata, bisimilarity of processes and determinisation of nondeterministic automata, will be treated coalgebraically. You will learn how to combine coinduction and induction to derive effective specification and reasoning techniques for automata, and how these lead to concrete algorithms. The coalgebraic framework will then be used to obtain generalisations of these constructions to other types of systems. Besides coalgebra, we will also discuss the role of category theory, and specifically monads, in functional programming; in particular, this will include probabilistic computation.
The study of computer science at this level of abstraction is valuable in itself, and strengthens the foundation for numerous more concrete skills: e.g. specification, implementation, programming language design, functional programming, and perhaps most prominently abstraction and identification of relevant structure. Coalgebra is a rather recent field of research, existing for a mere two decades, and it is attracting an enthusiastic community. Being relatively young, it still has many elementary and exciting research questions to offer.
Prerequisites:
The course is selfcontained with respect to category theory: no prior knowledge of category theory or algebra is assumed. We assume that you are well acquainted with basic notions in (discrete) mathematics and propositional logic, and have some familiarity with basic automata theory. These are typically taught in introductory courses at a computer science programme, for example, in the following bachelor CS courses at Radboud University: Languages and Automata, Mathematical Structures, Logic and Applications.
There will a final exam, and two extended homework assignments (completely separate from
the weekly homework, which is not graded), the first due in April,
and the second in June.
The final grade will be given by (H+E)/2, where H is the grade given for the homework
assignments and E is the grade given for the final exam.