A repository for the material of my course on lambda-calculus and categories
Lesson 1: introduction to the course [video][notes]
Lesson 2: categories, functors, natural transformations [video][notes]
Lesson 3: the 2-category of categories [video][notes]
Lesson 4: string diagrams and adjunctions [video][notes]
Lesson 5: the free cartesian category [video][notes]
Lesson 6: introduction to the lambda-calculus [video][notes 1][notes 2]
Lesson 7: computing recursive functions using the untyped lambda-calculus [video][notes][td + video]
Lesson 8: the simply-typed lambda-calculus, Church encodings [video] [notes] [td + video]
Lesson 9: the simply-typed lambda-calculus and cartesian closed categories [video] [notes] [td + video]
Lesson 10: the free cartesian closed category [video][notes] [td + video]
Lesson 11: adjunctions in string diagrams [video] [notes]
Lesson 12: from adjunctions to monads [video] [notes] [td + video]
Extra Lesson 12+1: from monads to adjunctions [video] [notes]
Not treated here: limits, colimits, Kan extensions, presheaves, Yoneda embedding, coends, calculus of distributors
Alia: monads, comonads, monadic effects, computational lambda-calculus, polymorphic lambda-calculus, parametricity, theorems for free, lambda-calculus with dependent types, contextual categories
TD 1 : cartesian categories [td]
TD 2 : coproducts, pullbacks, monoids [td]
TD 3 : adjunctions [td]
TD 4 : another equivalent formulation of adjunctions [td]
TD 5 : equalizers, epi-mono factorization, first-order logic [td]