Fun With Categories
summary
Defines category theory primitives in edct using Idris 2 with dependent types, encoding objects, morphisms, composition and identities and proved associativity plus left/right identity as compiler-checked equalities. Implements the category of Idris types-and-functions, a functor from a three-node directed-graph model of an e‑commerce flow into those types, and runs a demo that reads two product inputs and returns a generated invoice—pre‑alpha tooling but the example compiles and executes.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:35Category Theory
- 2:36Edct
- 4:31Idris
- 9:19Definition
- 11:12morphisms
- 12:52composition
- 13:29identitymorphism
- 14:47coherence conditions
- 16:22associativity
- 24:24functor
- 25:25mapping
- 36:22code walkthrough
related talks
52mCategory Theory Through Functional Programming (part 1/3)
51mCategory Theory for the Working Hacker
47mType-Driven Development in Idris
41mType-driven Development of Communicating Systems in Idris
02h 24mCategory Theory Track
56mCategory Theory Through Functional Programming (part 2/3)
57mApplied category theory and abstract algebra
01h 11mCategories for the Working Hacker