Category Theory Track by Bartosz Milewski Part 2
summary
Summarizes concrete identities and constructions used to write code from category theory: uses Curry/uncurry to turn A×B→C into A→(B→C) and completes the distributivity inverse by currying and applying left/right injections, defines a recursor for Nat that builds primitive recursive functions from one init and one step, and derives fold for lists as init plus step : A×C→C to implement map and traverse. Diagrams and arrow juggling produce working implementations and proofs within a Cartesian closed setting.
AI-written summary · about
chapters (12)
- 0:00Universal constructions recap
- 6:20Function objects and currying
- 13:12Distributivity via currying
- 25:03Functoriality on function arrows
- 33:29Natural numbers via mapping
- 44:34Recursor for natural numbers
- 53:29Break
- 53:50Recursive data types and lists
- 1:05:00Map for lists via recursion
- 1:16:18Generalizing recursive types
- 1:22:46Universal constructions summary
- 1:27:17Q&A on Cartesian closed categories
related talks
02h 24mCategory Theory Track
51mCategory Theory for the Working Hacker
54mCategory Theory Through Functional Programming (part 3/3)
56mCategory Theory Through Functional Programming (part 2/3)
52mCategory Theory Through Functional Programming (part 1/3)
42mWhat did category theory do for us?
01h 11mCategories for the Working Hacker
41mCategory Theory in Life