English
Category theory studies objects through the mappings between them and the laws of composition. For a programmer, ordinary functions provide a starting example: if f : A → B and g : B → C, their composite g ∘ f : A → C first applies f, then g. The same pattern occurs with other kinds of structure-preserving mappings.
The benefit is the ability to recognize shared constructions and transfer arguments between settings once their assumptions have been checked. Lists, optional values, and stateful computations differ, yet some operations on them obey common laws. Those laws explain which compositions and rewrites preserve meaning. Category theory complements concrete algorithms and data representations; it does not determine their running time or implementation by itself.
Begin with sets, functions, products, and some functional programming. Follow each abstract definition with a small example and its equations. Functors, natural transformations, adjunctions, and monads become more understandable when introduced through operations you can already perform.
How the Language of Structure Was Invented
Eilenberg and Mac Lane introduced categories, functors, and natural transformations in 1945 while studying connections between constructions in algebraic topology. Naturality expressed that a comparison was compatible with the relevant mappings, rather than depending on arbitrary choices of presentation. This need to compare entire constructions explains why the subject begins with several levels of mappings.
Connections to logic and computation developed later. Work associated with Lambek connected cartesian closed categories to typed lambda calculus with products, under appropriate equations. Scott’s domain theory supplied models for recursive and partial computation. These developments gave language designers ways to compare syntax, computation, and mathematical meaning.
Moggi’s account of computational monads distinguished values from computations that may have effects; Wadler and others helped develop the connection to functional programming. The historical contribution was to make a common compositional structure explicit across several effects. It was not the invention of exceptions, state, or input/output, which already had concrete implementations.
Applied category theory extends similar methods to systems, databases, and other mathematical models. The useful question is always which structure is being preserved and what that preservation allows us to conclude. A categorical description earns its place when it makes a construction, equivalence, or composition easier to state and justify.
Functors, Adjunctions, and Monads
The definitions build on one another. A category specifies objects and composable arrows. A functor maps one such setting into another while preserving composition. A natural transformation compares two functors coherently. An adjunction relates two mapping problems, and a monad captures a particular structure that can arise from an adjunction. The examples below give each definition a concrete role.
Categories and Functors: The Basic Vocabulary
A category has objects, arrows with specified sources and targets, an identity arrow for each object, and associative composition. Associativity means (h ∘ g) ∘ f = h ∘ (g ∘ f); identity means composing with id changes nothing. Sets with total functions form a category. A preorder gives a different example: take an arrow from a to b when a ≤ b; reflexivity supplies identities and transitivity supplies composition. Arrows therefore need not be functions between data structures.
A functor F maps objects and arrows, preserving identities and composition: F(id) = id and F(g ∘ f) = F(g) ∘ F(f). For lists, it maps a type A to List A and a function f : A → B to map f : List A → List B. Mapping “add one” and then “double” over [1,2] produces [4,6], just as mapping their composite does. The functor law justifies this equality for all lists, not only the example; an implementation may use it to combine two traversals when the semantic assumptions permit.
A type constructor alone is not enough to supply a functor. The arrow mapping must exist and obey the laws. For predicates A → Bool, a function f : A → B lets us turn a predicate on B into one on A by precomposition. The direction reverses. This is contravariant behavior, rather than the covariant mapping used by lists.
A natural transformation compares two functors in a way compatible with every arrow. Consider first : List A → Maybe A, which returns the first element or None. For any total f, taking the first element and mapping f over the optional result agrees with mapping f over the list and then taking the first element. This equation is the naturality condition. It formalizes that first depends on list structure, not on inspecting the particular element type.
Products also have a description in terms of arrows. A pair A × B has projections to each component; given f : X → A and g : X → B, there is a unique map x ↦ (f(x),g(x)) with those projections. This is a universal property: it characterizes how the object interacts with all possible X, rather than choosing one internal representation. Such descriptions identify constructions up to the appropriate isomorphism.
Adjunctions: Two Descriptions of a Mapping Problem
An adjunction between F : C → D and U : D → C gives a natural bijection between arrows F(A) → B in D and arrows A → U(B) in C. “Natural” requires compatibility when A or B changes through an arrow. The two sides describe the same mapping problem in different settings; the functors need not undo each other.
Currying provides a familiar example in sets: functions X × A → B correspond exactly to functions X → (A → B). A function taking a pair can be rewritten as one that takes its first argument and returns a function awaiting the second. Uncurrying reverses the translation. Thus forming a product with A is left adjoint to forming a function space from A.
Another example connects sets and monoids. A monoid has an associative operation and an identity element; lists with concatenation and the empty list form one. The free-monoid construction turns a set A into finite lists of its elements. The forgetful functor retains the underlying set of a monoid while forgetting the named operation and identity. A function from A into that underlying set extends uniquely to a monoid homomorphism from lists: map each element, then combine the results using the monoid operation.
For numbers with addition, interpreting each element as itself gives summation; interpreting each element as one gives length. The empty list must map to zero, and concatenation must map to addition. Once the element interpretation is chosen, the preservation requirements determine the whole fold. This explains the practical content of the universal property and the free/forgetful adjunction.
Monads: Functors with Algebraic Structure
A monad consists of a functor T, a unit η : A → T A, and a multiplication μ : T(T A) → T A, with naturality, identity, and associativity laws. In programming, the multiplication is often called join. For lists, the unit makes a singleton list and join concatenates a list of lists. This monad arises from the free-monoid/forgetful adjunction above; “free monoid” should not be confused with the separate construction called a free monad.
An equivalent programming interface uses bind : T A → (A → T B) → T B. Ordinary function composition cannot directly combine f : A → T B with g : B → T C, because g expects a B, not a T B. Bind handles that intermediate structure. For Maybe, it applies the next function to a successful value and propagates None without applying it. A number parser followed by a reciprocal operation can therefore fail either on invalid text or on zero, while using the same sequencing operation.
The laws say that supplying a value through the unit adds no computational effect, and regrouping a chain of binds does not change its meaning. Associativity permits regrouping; it does not permit reordering effects. Writing a file and then deleting it generally differs from deleting it and then writing it.
The state monad represents a computation returning A as a function S → (A × S): it consumes an initial state and returns a value with the next state. Bind passes that returned state to the next computation. Its categorical construction comes from the product/function-space adjunction. This representation makes state flow explicit while allowing the sequencing operation to manage the repeated plumbing.
Combining effects requires additional structure. S → Maybe (A × S) loses the resulting state when it fails; S → (Maybe A × S) can retain a state even on failure. These types describe different choices about failure and state, which matter when an operation changes state before failing. Arbitrary monads do not automatically compose into another monad. Transformers and distributive laws provide constructions under specified conditions; the order of combination remains meaningful.
What Studying This Changes
The useful habit is to ask which laws an interface promises. An operation named map is not automatically lawful, and an operation named bind does not automatically provide associative sequencing. Proving the equations for a concrete implementation tells you which generic reasoning applies.
Implement list mapping, Maybe sequencing, and a small state computation, then check the identity and composition laws on paper before using tests to find mistakes. Follow with the product and free-monoid universal properties. These examples provide a basis for reading categorical semantics without treating vocabulary alone as understanding.
Resources
Books and Texts
Awodey’s Category Theory (2nd ed., 2010) introduces the core mathematical definitions through examples and exercises. It is a possible first mathematical text for readers comfortable with functions and proofs. Work through the categories of sets, preorders, and algebraic structures before attempting the more abstract constructions.
Mac Lane’s Categories for the Working Mathematician (2nd ed., 1998) is a mathematical reference covering universal constructions, adjunctions, monads, and further topics. Its algebraic examples and concise presentation assume more mathematical preparation. Use it to deepen a specific topic once the basic definitions are familiar.
Milewski’s Category Theory for Programmers uses Haskell examples to connect programming operations to categorical definitions. It can accompany a more mathematical text. When translating an example into an actual language, pay attention to totality, effects, and which equations the model assumes.
Pierce’s Basic Category Theory for Computer Scientists (1991) is a short CS-oriented introduction. Its limited scope can be useful for a first pass through the basic vocabulary and selected applications before moving to a longer text.
Barr and Wells’s Category Theory for Computing Science (free online, 3rd ed.) covers the same core material as Awodey with heavier CS emphasis. It is more comprehensive than Pierce for CS applications, covering algebraic automata theory, categorical semantics of programming languages, and other CS-specific topics that Awodey treats only briefly. The combination of Awodey (for mathematical foundations and clarity) and Barr-Wells (for CS applications) is more effective than either alone.
Riehl’s Category Theory in Context (Dover, 2016, free at math.jhu.edu/~eriehl/context.pdf) is a graduate-level mathematical treatment that is nevertheless clearly written and accessible to motivated readers who have completed Awodey. It covers representability, limits and colimits, adjunctions, and monads with fuller treatment than Awodey, and it bridges the gap between Awodey-level mathematics and the contemporary research literature.
For applied category theory, Fong and Spivak’s Seven Sketches in Compositionality (free at arxiv.org/abs/1803.05316) is the entry. It covers preorders, resource theories, databases, co-design, signal flow graphs, and electrical circuits — all from a categorical perspective — at a level accessible to non-mathematicians. It is a useful text for learners interested in applying category theory to engineering and scientific domains.
For categorical logic and programming language semantics, Lambek and Scott’s Introduction to Higher-Order Categorical Logic (Cambridge, 1986) is the canonical reference. It develops the correspondence between Cartesian closed categories, the typed lambda calculus, and intuitionistic logic, and explains why PLT and category theory are so deeply connected.
| Book | Role | Type |
|---|---|---|
| Awodey, Category Theory (2nd ed.) | Standard accessible entry | Entry |
| Mac Lane, Categories for the Working Mathematician (2nd ed.) | Canonical mathematical reference | Reference |
| Milewski, Category Theory for Programmers (free) | Programmer-oriented introduction | Entry |
| Pierce, Basic Category Theory for Computer Scientists | Brief CS-oriented entry | Entry |
| Barr & Wells, Category Theory for Computing Science (free) | Comprehensive CS-oriented text | Depth |
| Riehl, Category Theory in Context (free) | Graduate-level treatment | Depth |
| Fong & Spivak, Seven Sketches in Compositionality (free) | Applied category theory entry | Entry |
| Lambek & Scott, Introduction to Higher-Order Categorical Logic | Categorical logic and PLT | Depth |
| Mac Lane & Moerdijk, Sheaves in Geometry and Logic | Topos theory beyond the CS learning path | Auxiliary |
Courses and Lectures
Milewski’s Category Theory for Programmers video lectures accompany the book with Haskell examples. Pause to implement the examples and check the stated laws, rather than relying only on recognizing the terminology during a lecture.
MIT 18.S097: Applied Category Theory, January IAP 2019 provides course materials and problems connected to applied categorical models. Use the year and title with the course number, since MIT reuses special-subject numbers for different topics.
The Applied Category Theory School (ACT, held annually with accompanying reading groups) produces accessible introductory material aimed at learners outside pure mathematics. ACT reading groups cover Seven Sketches and related texts; the school lectures are available on YouTube.
Emily Riehl’s lectures on category theory at various summer schools (freely available on YouTube) cover the mathematical content of her book at a level accessible to advanced undergraduates. Her treatment of the Yoneda lemma and adjunctions is particularly clear.
The Catsters videos (free on YouTube) are an older but still useful collection of short pedagogical explanations of core category theory concepts. They are not CS-specific, but they often make definitions such as products, coproducts, adjunctions, and natural transformations easier to hear before reading them formally.
The Topos Institute produces talks and seminars on applied category theory, including examples connected to systems, databases, probability, and scientific modeling. The material is uneven in level, but it is a good current-source stream for readers who want to see where applied category theory is being used now.
| Course | Platform | Type |
|---|---|---|
| Milewski, Category Theory for Programmers lectures (free) | YouTube | Entry |
| ACT School lectures (free) | YouTube / ACT site | Entry |
| Emily Riehl lectures on category theory (free) | YouTube | Depth |
| The Catsters category theory videos (free) | YouTube | Auxiliary |
| Topos Institute talks (free) | YouTube / topos.institute | Reference |
Practice, Tools, and Current Sources
nLab (ncatlab.org) is a reference wiki for categorical definitions and connections. Entries vary in assumed background. Use it to clarify a specific term and follow its references, alongside a textbook with a planned sequence of examples.
Working through the Haskell Functor, Applicative, and Monad typeclasses with explicit attention to the categorical structure — deriving the functor laws, verifying the monad laws for specific instances, implementing the Kleisli composition — builds intuition that reading does not. Implement the State, Maybe, and Reader monads from scratch and verify that they satisfy the monad laws.
Agda can express a functor as a record containing an object map, an arrow map, and proofs of the identity and composition laws. Formalize a small example after proving it on paper. This makes omitted obligations visible, while requiring familiarity with the proof assistant itself.
Catlab.jl provides Julia tools for applied category theory, including categorical data structures and diagrammatic constructions. Choose a documented example whose underlying mathematics you understand, then inspect how the package represents it.
| Resource | Platform | Type |
|---|---|---|
| nLab (free) | ncatlab.org | Reference |
| Haskell typeclass implementations (functor laws, monad laws) | Local | Practice |
| Agda category theory formalization | Local / agda.readthedocs.io | Practice |
| Catlab.jl (free) | Julia package | Practice |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
Giving every type constructor a covariant map |
Some constructions reverse arrows or need extra conditions. | Specify the arrow mapping and prove its laws. |
| Treating naturality as a vague absence of choices | It is a precise compatibility equation. | Write the equation for first : List A → Maybe A and check both routes. |
| Calling adjoint functors approximate inverses | An adjunction relates mapping sets; it need not recover the original objects. | Work through currying or the free-monoid example. |
| Confusing free monoids with free monads | They are distinct constructions. | Identify the categories and the relevant free/forgetful adjunction. |
| Reading associativity as permission to reorder effects | Regrouping preserves order; swapping operations can change behavior. | Keep the sequence of effects fixed when applying the law. |
| Assuming arbitrary monads compose | State and failure already reveal different possible combinations. | Specify the construction, combination order, and required laws. |
中文
范畴论通过对象之间的映射以及复合规律来研究对象。对程序员来说，普通函数就是一个起点：如果 f : A → B、g : B → C，它们的复合 g ∘ f : A → C 先应用 f，再应用 g。其他保持结构的映射也会出现这种模式。
它的作用是识别共同构造，并在核对假设后，把论证从一个场景用于另一个场景。列表、可选值与带状态计算各不相同，但它们的一些操作遵守共同规律。这些规律解释哪些组合与改写保持含义。范畴论补充具体算法和数据表示，本身并不决定运行时间或实现方式。
从集合、函数、积以及一些函数式编程经验开始。每遇到一个抽象定义，就配上一个小例子和对应等式。通过已经会做的操作引入函子、自然变换、伴随与单子，会更容易理解。
结构语言如何被发明
Eilenberg 与 Mac Lane 在 1945 年研究代数拓扑中各种构造的联系时，引入了范畴、函子与自然变换。自然性表达的是：一种比较与相关映射相容，而不依赖任意的表示选择。需要比较整个构造，解释了为什么这门学科一开始就出现多个层次的映射。
与逻辑和计算的联系随后发展起来。与 Lambek 相关的工作，在适当等式下把笛卡尔闭范畴连接到带积的有类型 lambda 演算。Scott 的域论则为递归与部分计算提供模型。这些发展使语言设计者能够比较语法、计算与数学含义。
Moggi 对计算性单子的论述区分了值与可能带副作用的计算；Wadler 等人进一步发展了它与函数式编程的联系。历史贡献在于明确多种副作用所共有的组合结构，而不是发明异常、状态或输入输出；后者此前已经有具体实现。
应用范畴论把类似方法用于系统、数据库和其他数学模型。始终值得追问的是：保持了什么结构，这种保持允许得出什么结论？当范畴描述使某个构造、等价关系或组合更容易陈述和论证时，它就有具体用途。
函子、伴随与 Monads
这些定义逐步建立。范畴规定对象与可复合的箭头；函子在两个这样的场景之间映射，并保持复合；自然变换协调地比较两个函子；伴随连接两个映射问题；单子刻画一种可以由伴随产生的结构。下面的例子分别说明它们的作用。
范畴与函子：基本词汇
范畴包含对象、带明确起点与终点的箭头、每个对象的恒等箭头，以及满足结合律的复合。结合律是 (h ∘ g) ∘ f = h ∘ (g ∘ f)；恒等律表示与 id 复合不改变原箭头。集合与全函数构成一个范畴。预序给出另一种例子：当 a ≤ b 时，放置一条从 a 到 b 的箭头；自反性提供恒等箭头，传递性提供复合。因此，箭头不一定是数据结构之间的函数。
函子 F 映射对象与箭头，并保持恒等和复合：F(id) = id、F(g ∘ f) = F(g) ∘ F(f)。列表函子把类型 A 映射到 List A，把函数 f : A → B 映射到 map f : List A → List B。在 [1,2] 上先映射“加一”，再映射“乘二”，得到 [4,6]，与直接映射二者的复合相同。函子律对所有列表建立这种相等，而不只针对这个例子；在语义假设允许时，实现可以据此把两次遍历合并。
仅有类型构造子，还不足以提供函子。还必须有箭头映射，并满足相应规律。对于谓词 A → Bool，函数 f : A → B 可以通过预复合，把 B 上的谓词变成 A 上的谓词。方向反了。这是逆变行为，而不是列表采用的协变映射。
自然变换以与每条箭头相容的方式比较两个函子。考虑 first : List A → Maybe A，它返回首元素或 None。对于任意全函数 f，先取首元素、再对可选结果映射 f，与先在列表上映射 f、再取首元素相同。这个等式就是自然性条件。它形式化地表达了：first 依赖列表结构，而不需要检查具体元素类型。
积也可以用箭头描述。二元组 A × B 有通向各分量的投影；给定 f : X → A 与 g : X → B，存在唯一映射 x ↦ (f(x),g(x))，使投影分别得到这两个函数。这是一种泛性质：它通过对象与所有可能的 X 的交互来刻画对象，而不指定某一种内部表示。这类描述在适当的同构意义下确定构造。
伴随：映射问题的两种描述
F : C → D 与 U : D → C 之间的伴随，提供一个自然双射：一边是 D 中的箭头 F(A) → B，另一边是 C 中的箭头 A → U(B)。“自然”要求在 A 或 B 通过箭头变化时仍然相容。两边在不同场景中描述同一个映射问题；这两个函子不必互相撤销。
集合中的柯里化是一个熟悉例子：函数 X × A → B 与函数 X → (A → B) 一一对应。接收二元组的函数，可以改写为先接收第一个参数、再返回一个等待第二个参数的函数。反柯里化逆转这个转换。因此，与 A 构成积，左伴随于构成从 A 出发的函数空间。
另一个例子连接集合与幺半群。幺半群具有结合运算与单位元；带拼接操作和空列表的列表就构成一个幺半群。自由幺半群构造把集合 A 变成其元素构成的有限列表。遗忘函子保留幺半群的底层集合，忘掉指定的运算和单位元。从 A 到该底层集合的函数，可以唯一扩展为从列表出发的幺半群同态：先映射每个元素，再用幺半群运算合并结果。
对于采用加法的数，把每个元素解释为它本身，得到求和；把每个元素解释为一，得到长度。空列表必须映射为零，拼接必须映射为加法。一旦选定元素解释，保持结构的要求就决定了整个折叠。这说明了泛性质以及自由／遗忘伴随的实际内容。
Monads：带有代数结构的函子
单子由函子 T、单位 η : A → T A 与乘法 μ : T(T A) → T A 构成，并满足自然性、恒等律和结合律。编程中常把这个乘法称为 join。对于列表，单位构造单元素列表，join 则拼接列表的列表。这个单子来自上面的自由幺半群／遗忘伴随；“自由幺半群”不能与另一种称为自由单子的构造混淆。
等价的编程接口使用 bind : T A → (A → T B) → T B。普通函数复合不能直接组合 f : A → T B 与 g : B → T C，因为 g 需要的是 B，不是 T B。Bind 处理这个中间结构。对于 Maybe，它把下一函数应用于成功值；遇到 None 则直接传播失败，不应用该函数。因此，把数字解析器与取倒数操作串联起来，既可以在文本无效时失败，也可以在数值为零时失败，而使用同一个顺序组合操作。
这些规律表示：通过单位提供一个值，不增加计算副作用；重新分组一串 bind，不改变其含义。结合律允许重新分组，却不允许调换副作用的顺序。先写文件再删除，一般不同于先删除再写入。
状态单子把返回 A 的计算表示成函数 S → (A × S)：接收初始状态，返回值与下一状态。Bind 把返回的状态交给下一计算。它的范畴构造来自积／函数空间伴随。这种表示明确写出状态流动，同时让顺序组合操作负责反复传递状态的工作。
组合副作用需要额外结构。S → Maybe (A × S) 在失败时不提供结果状态；S → (Maybe A × S) 即使失败也可以保留状态。这些类型表达了失败与状态之间的不同选择；如果操作先修改状态、随后失败，这个区别就很重要。任意单子并不会自动复合成另一个单子。变换器与分配律在指定条件下提供构造，而组合顺序仍然有意义。
学习这个主题会改变什么
有用的习惯是追问接口承诺哪些规律。名为 map 的操作不会自动满足函子律，名为 bind 的操作也不会自动提供满足结合律的顺序组合。对具体实现证明这些等式，才能知道哪些通用推理适用。
实现列表映射、Maybe 串联和一个小型状态计算，先在纸上检查恒等律与复合规律，再用测试寻找错误。随后学习积与自由幺半群的泛性质。这些例子为阅读范畴语义提供基础，而不把认识术语当成理解。
资源
书籍与文本
Awodey 的 Category Theory（第 2 版，2010）通过例子和练习介绍核心数学定义。对于熟悉函数与证明的读者，可以把它作为第一本数学教材。先推演集合、预序与代数结构的范畴，再学习更抽象的构造。
Mac Lane 的 Categories for the Working Mathematician（第 2 版，1998）是数学参考书，覆盖泛构造、伴随、单子及进一步主题。代数例子与紧凑写法需要较多数学准备。熟悉基本定义后，可以用它深入某个具体主题。
Milewski 的 Category Theory for Programmers 用 Haskell 例子连接编程操作与范畴定义，可以配合数学教材学习。把例子用于实际语言时，应注意全定义性、副作用以及模型假定的等式。
Pierce 的 Basic Category Theory for Computer Scientists（1991）是简短的 CS 导向入门。它范围较集中，适合在进入较长教材之前，先学习基本词汇与部分应用。
Barr 和 Wells 的 Category Theory for Computing Science（免费在线，第 3 版）覆盖与 Awodey 相同的核心材料，但更强调 CS。它比 Pierce 更全面地处理 CS 应用，覆盖代数自动机理论、编程语言的范畴语义，以及其他 CS 专门主题，而这些在 Awodey 中只被简要处理。Awodey（用于数学基础和清晰性）与 Barr-Wells（用于 CS 应用）的组合，比单独读任一本更有效。
Riehl 的 Category Theory in Context（Dover，2016，可在 math.jhu.edu/~eriehl/context.pdf 免费获取）是研究生水平数学处理，但写作清楚，对完成 Awodey 的积极读者而言可以进入。它以比 Awodey 更完整的方式覆盖 representability、极限与余极限、伴随和 monads，并在 Awodey 水平的数学与当代研究文献之间架桥。
对于 应用范畴论，Fong 和 Spivak 的 Seven Sketches in Compositionality（arxiv.org/abs/1803.05316 免费）是入口。它从范畴视角覆盖预序、资源理论、数据库、co-design、信号流图和电路，且非数学家也可以进入。对于有兴趣把范畴论应用到工程和科学领域的学习者，这是可选教材。
对于 范畴逻辑和编程语言语义，Lambek 和 Scott 的 Introduction to Higher-Order Categorical Logic（Cambridge，1986）是经典参考。它发展了 Cartesian closed categories、类型化 λ 演算和直觉主义逻辑之间的对应，对于理解 PLT 与范畴论为何如此深度连接是必要的。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Awodey，Category Theory（第 2 版） | 标准且易进入的入口 | 入门 |
| Mac Lane，Categories for the Working Mathematician（第 2 版） | 经典数学参考 | 参考 |
| Milewski，Category Theory for Programmers（免费） | 面向程序员的导论 | 入门 |
| Pierce，Basic Category Theory for Computer Scientists | 简短 CS 向入口 | 入门 |
| Barr & Wells，Category Theory for Computing Science（免费） | 综合 CS 向文本 | 深入 |
| Riehl，Category Theory in Context（免费） | 研究生水平处理 | 深入 |
| Fong & Spivak，Seven Sketches in Compositionality（免费） | 应用范畴论入口 | 入门 |
| Lambek & Scott，Introduction to Higher-Order Categorical Logic | 范畴逻辑与 PLT | 深入 |
| Mac Lane & Moerdijk，Sheaves in Geometry and Logic | 超出 CS 学习路径的 Topos 理论 | 辅助 |
课程与讲座
Milewski 的 Category Theory for Programmers 视频讲座配合书籍使用 Haskell 例子。可以暂停讲座，实现例子并检查所述规律，而不只在听讲时辨认术语。
MIT 18.S097：Applied Category Theory，2019 年 January IAP 提供应用范畴模型相关的课程材料与习题。引用时应同时保留年份和标题，因为 MIT 会把专题课编号用于不同主题。
Applied Category Theory School（ACT，每年举办，并配有 reading groups）产出面向纯数学之外学习者的易进入导论材料。ACT reading groups 会覆盖 Seven Sketches 和相关文本；学校讲座可以在 YouTube 获取。
Emily Riehl 的讲座，包括各种 summer school 中关于范畴论的讲座（YouTube 免费），以高级本科生可进入的层级覆盖她书中的数学内容。她对 Yoneda lemma 和伴随的处理尤其清楚。
The Catsters 视频（YouTube 免费）是一组较早但仍有用的短教学解释，讲解核心范畴论概念。它们不面向 CS，但在正式阅读定义前，常能让积、余积、伴随和自然变换等定义更容易被“听懂”。
Topos Institute 产出关于应用范畴论的报告和研讨会，包括与系统、数据库、概率和科学建模相关的例子。材料层级不一，但对于想了解应用范畴论当前使用方向的读者来说，这是良好的当前来源。
| 课程 | 平台 | 类型 |
|---|---|---|
| Milewski，Category Theory for Programmers lectures（免费） | YouTube | 入门 |
| ACT School lectures（免费） | YouTube / ACT site | 入门 |
| Emily Riehl category theory lectures（免费） | YouTube | 深入 |
| The Catsters category theory videos（免费） | YouTube | 辅助 |
| Topos Institute talks（免费） | YouTube / topos.institute | 参考 |
实践、工具与当前来源
nLab（ncatlab.org）是查询范畴定义与联系的参考维基，各条目预设的背景不同。可以用它澄清具体术语并查阅所引文献，同时配合有明确例子顺序的教材。
带着对范畴结构的明确关注，推导 Haskell 的 Functor、Applicative 和 Monad typeclasses——推导函子律，验证具体实例的 monad 律，实现 Kleisli composition——可以建立阅读无法提供的直觉。从零实现 State、Maybe 和 Reader monads，并验证它们满足 monad 律。
Agda 可以把函子表达为一个记录，包含对象映射、箭头映射，以及恒等律和复合律的证明。可以先在纸上证明一个小例子，再将它形式化。这会显示遗漏的义务，但也需要熟悉证明助手本身。
Catlab.jl 提供应用范畴论的 Julia 工具，包括范畴数据结构与图式构造。选择一个已经理解其数学内容的文档例子，再检查包怎样表示它。
| 资源 | 平台 | 类型 |
|---|---|---|
| nLab（免费） | ncatlab.org | 参考 |
| Haskell typeclass 实现（函子律、monad 律） | 本地 | 实践 |
| Agda 范畴论形式化 | 本地 / agda.readthedocs.io | 实践 |
| Catlab.jl（免费） | Julia package | 实践 |
陷阱
| 陷阱 | 为什么会误导 | 更好的做法 |
|---|---|---|
给每个类型构造子配上协变 map |
有些构造会反转箭头，或需要额外条件。 | 明确箭头映射并证明规律。 |
| 把自然性理解成含糊的“没有任意选择” | 自然性是精确的相容等式。 | 为 first : List A → Maybe A 写出等式，检查两条路径。 |
| 把伴随函子称为近似逆 | 伴随连接映射集合，不一定恢复原对象。 | 推演柯里化或自由幺半群的例子。 |
| 混淆自由幺半群与自由单子 | 它们是不同构造。 | 指明范畴以及相应的自由／遗忘伴随。 |
| 把结合律读成可以重排副作用 | 重新分组保持顺序，交换操作可能改变行为。 | 应用规律时保持副作用次序不变。 |
| 认为任意单子都能复合 | 状态与失败已经展示了不同组合结果。 | 说明构造、组合次序与所需规律。 |