范畴论（Category Theory）是数学中一门高度抽象的学科，被誉为"数学的数学"。它研究数学结构之间的共同模式和关系，提供了一种统一的语言来思考和描述不同数学领域中的概念。本文从基础概念出发，逐步深入到函子、自然变换、极限、伴随函子、Yoneda引理等重要主题，并探讨范畴论在编程和逻辑中的应用。
范畴论由 Saunders Mac Lane 和 Samuel Eilenberg 于 1945 年在其开创性论文《Natural Equivalences in General Mathematics》中正式引入。最初作为代数拓扑中处理自然变换的一种形式化工具，后来逐渐发展成为贯穿现代数学的基础语言。
范畴论的核心思想是：与其研究一个对象内部的结构，不如研究它与其他对象之间的关系 。这种"关系优先"的视角被称为"关系相对论"——它聚焦于对象之间的映射（称为态射），而非对象本身的内部构造。
在集合论中，我们关心集合的元素；
在范畴论中，我们关心集合之间的函数，而非元素本身。
这一视角的转变使得范畴论能够跨越不同数学分支，发现它们之间的深层联系。例如，群论中的群同态、拓扑学中的连续映射、序理论中的单调函数——在范畴论的框架下，它们都是不同范畴中的态射，遵循相同的结构规律。
一个 范畴 C C
对象（Objects） ：一类对象，记作 Ob ( C ) Ob ( C ) 态射（Morphisms/Arrows） ：对于任意两个对象 A , B ∈ Ob ( C ) A , B ∈ Ob ( C ) Hom C ( A , B ) Hom C ( A , B ) f : A → B f : A → B A A B B 复合（Composition） ：对于任意态射 f : A → B f : A → B g : B → C g : B → C g ∘ f : A → C g ∘ f : A → C 单位态射（Identity Morphism） ：对于每个对象 A A id A : A → A id A : A → A
以上数据必须满足以下公理：
结合律 ：对于 f : A → B f : A → B g : B → C g : B → C h : C → D h : C → D ( h ∘ g ) ∘ f = h ∘ ( g ∘ f ) ( h ∘ g ) ∘ f = h ∘ ( g ∘ f ) 单位律 ：对于 f : A → B f : A → B f ∘ id A = f f ∘ id A = f id B ∘ f = f id B ∘ f = f
可以将范畴想象为一个有向图：
节点 = 对象有向边 = 态射边的复合 = 沿着路径走自环 = 单位态射（每个节点一个）结合律 = 路径顺序不影响最终结果
范畴
对象
态射
Set 集合
函数
Grp 群
群同态
Top 拓扑空间
连续映射
Vectₖ 向量空间
线性映射
Ring 环
环同态
Poset 偏序集
单调函数
Hask Haskell类型
Haskell函数
态射 f : A → B f : A → B 同构 ，如果存在 g : B → A g : B → A g ∘ f = id A g ∘ f = id A f ∘ g = id B f ∘ g = id B A A B B A ≅ B A ≅ B g g f f
核心洞见 ：在同构的意义下，范畴论不区分结构相同的对象——"同构的对象在范畴论眼中是相同的"。这一原则被称为"范畴论公理"（The Principle of Equivalence）。
态射 f : A → B f : A → B 单态射 （或单射性的范畴推广），如果对任意平行态射 g 1 , g 2 : X → A g 1 , g 2 : X → A f ∘ g 1 = f ∘ g 2 f ∘ g 1 = f ∘ g 2 g 1 = g 2 g 1 = g 2 Set 中，单态射恰好是单射函数。
态射 f : A → B f : A → B 满态射 （或满射性的范畴推广），如果对任意平行态射 h 1 , h 2 : B → Y h 1 , h 2 : B → Y h 1 ∘ f = h 2 ∘ f h 1 ∘ f = h 2 ∘ f h 1 = h 2 h 1 = h 2 Set 中，满态射恰好是满射函数。
自同态（Endomorphism） ：f : A → A f : A → A 自同构（Automorphism） ：既是自同态又是同构的态射。
如果范畴有零对象（既是始对象又是终对象），则任意两个对象之间可以定义零态射。在 Grp 中，零态射是映射所有元素到单位元的群同态。
对象集任意，态射只有单位态射的范畴。称为"离散"是因为它没有任何非平凡的结构性联系。可以理解为没有边（只有自环）的有向图。
如果对任意 A , B A , B Hom ( A , B ) Hom ( A , B ) A ≤ B A ≤ B A → B A → B
小范畴（Small Category） ：对象集和态射集都是集合（而非真类）。大范畴（Large Category） ：对象集是真类（proper class），例如 Set 、Grp 、Top 等都是大范畴。
如果对任意 A , B A , B Hom C ( A , B ) Hom C ( A , B ) C C Set 、Grp ）都是局部小范畴。
对范畴 C C D D 积范畴 C × D C × D
对象：( C , D ) ( C , D ) C ∈ Ob ( C ) C ∈ Ob ( C ) D ∈ Ob ( D ) D ∈ Ob ( D )
态射：( f , g ) : ( C 1 , D 1 ) → ( C 2 , D 2 ) ( f , g ) : ( C 1 , D 1 ) → ( C 2 , D 2 ) f : C 1 → C 2 f : C 1 → C 2 g : D 1 → D 2 g : D 1 → D 2
复合和单位态射分量定义
范畴 C C 箭头范畴 C → C → C C ( f : A → B ) → ( g : C → D ) ( f : A → B ) → ( g : C → D ) ( h : A → C , k : B → D ) ( h : A → C , k : B → D )
A --f--> B
| |
h k
v v
C --g--> D
即 k ∘ f = g ∘ h k ∘ f = g ∘ h
逗号范畴是箭头范畴的推广。给定函子 F : A → C F : A → C G : B → C G : B → C 逗号范畴 ( F ↓ G ) ( F ↓ G ) ( A ∈ A , B ∈ B , f : F ( A ) → G ( B ) ) ( A ∈ A , B ∈ B , f : F ( A ) → G ( B ) ) C / C C / C A = C A = C B = 1 B = 1 F = id C F = id C G G C C
泛性质（Universal Property）是范畴论最强大的概念之一。它通过对象和态射之间的关系来刻画一个对象，而不依赖该对象的内部构造。
始对象（Initial Object） 0 0 X X 0 → X 0 → X 终对象（Terminal Object） 1 1 X X X → 1 X → 1 零对象（Zero Object） ：既是始对象又是终对象的对象。
示例 ：在 Set 中，空集 ∅ ∅ { ∗ } { ∗ } Grp 中，平凡群 { e } { e }
始对象和终对象在同构意义下是唯一的——这是泛性质最典型的结论之一。
积（Product） ：对象 A A B B ( P , p A : P → A , p B : P → B ) ( P , p A : P → A , p B : P → B ) ( X , f : X → A , g : X → B ) ( X , f : X → A , g : X → B ) ⟨ f , g ⟩ : X → P ⟨ f , g ⟩ : X → P
X
/|\
/ | \
f / | \ g
/ | \
v v v
A <-- P --> B
p_A p_B
记 P P A × B A × B Set 中它就是笛卡尔积。
余积（Coproduct） ：对偶于积的概念，即反转所有态射方向。记 A ⊔ B A ⊔ B Set 中它是无交并（disjoint union）。
范畴
积
余积
Set 笛卡尔积 A × B A × B
无交并 A ⊔ B A ⊔ B
Grp 直积 G × H G × H
自由积 G ∗ H G ∗ H
Vectₖ 直和 V ⊕ W V ⊕ W
直和 V ⊕ W V ⊕ W
Top 乘积拓扑
不交并拓扑
关键性质 ：在 Vectₖ 中，积和余积是同构的（有限维情况），这反映了向量空间范畴的自对偶性。
等化子（Equalizer） ：对平行态射 f , g : A → B f , g : A → B e : E → A e : E → A f ∘ e = g ∘ e f ∘ e = g ∘ e f ∘ h = g ∘ h f ∘ h = g ∘ h h : X → A h : X → A u : X → E u : X → E e ∘ u = h e ∘ u = h
在 Set 中，E = { a ∈ A ∣ f ( a ) = g ( a ) } E = { a ∈ A ∣ f ( a ) = g ( a ) } e e
余等化子（Coequalizer） ：对偶概念。在 Set 中，它是对 A A f ( a ) ∼ g ( a ) f ( a ) ∼ g ( a )
函子（Functor）是范畴之间的"映射"，它保持范畴结构。
给定范畴 C C D D F : C → D F : C → D
对每个 C C X X D D F ( X ) F ( X )
对每个态射 f : X → Y f : X → Y F ( f ) : F ( X ) → F ( Y ) F ( f ) : F ( X ) → F ( Y )
满足：
F ( id X ) = id F ( X ) F ( id X ) = id F ( X ) F ( g ∘ f ) = F ( g ) ∘ F ( f ) F ( g ∘ f ) = F ( g ) ∘ F ( f )
反变（逆变）函子 F : C op → D F : C op → D f : X → Y f : X → Y F ( f ) : F ( Y ) → F ( X ) F ( f ) : F ( Y ) → F ( X )
有时也表示为 F : C → D F : C → D C op C op D D
遗忘函子（Forgetful Functor）"忘记"结构信息。例如：
U : Grp → Set U : Grp → Set U : Top → Set U : Top → Set
遗忘函子看似平凡，但在伴随函子理论中扮演重要角色。
自由函子（Free Functor）是遗忘函子的左伴随。它构建"最自由"的代数结构。例如从集合到自由群的函子：给定集合 S S F ( S ) F ( S ) S S a a − 1 = e a a − 1 = e
核心的构造性函子。对于局部小范畴 C C
共变 Hom 函子 Hom ( A , − ) : C → Set Hom ( A , − ) : C → Set X X Hom ( A , X ) Hom ( A , X ) f : X → Y f : X → Y f ∗ : Hom ( A , X ) → Hom ( A , Y ) f ∗ : Hom ( A , X ) → Hom ( A , Y ) 反变 Hom 函子 Hom ( − , B ) : C op → Set Hom ( − , B ) : C op → Set X X Hom ( X , B ) Hom ( X , B ) f : X → Y f : X → Y f ∗ : Hom ( Y , B ) → Hom ( X , B ) f ∗ : Hom ( Y , B ) → Hom ( X , B )
Set Set P : Set op → Set P : Set op → Set S S P ( S ) P ( S ) S S f : S → T f : S → T P ( f ) : P ( T ) → P ( S ) P ( f ) : P ( T ) → P ( S )
一个范畴 C C 具体范畴 （Concrete Category），如果存在忠实（faithful）的遗忘函子 U : C → Set U : C → Set C C Grp 、Top 、Ring ）都是具体范畴。
自然变换（Natural Transformation）是函子之间的态射，是范畴论中最核心的概念之一——Mac Lane 曾言"范畴论最初就是为了定义自然变换而发明的"。
给定两个共变函子 F , G : C → D F , G : C → D F F G G η : F → G η : F → G
η X : F ( X ) → G ( X ) ( 对每个 X ∈ Ob ( C ) ) η X : F ( X ) → G ( X ) ( 对每个 X ∈ Ob ( C ) )
使得对 C C f : X → Y f : X → Y
F(X) --F(f)--> F(Y)
| |
η_X η_Y
v v
G(X) --G(f)--> G(Y)
即 η Y ∘ F ( f ) = G ( f ) ∘ η X η Y ∘ F ( f ) = G ( f ) ∘ η X
如果自然变换 η η η X η X η η 自然同构 （Natural Isomorphism），记为 F ≅ G F ≅ G
双重对偶 ：有限维向量空间到其双重对偶空间的映射 V → V ∗ ∗ V → V ∗ ∗ V → V ∗ V → V ∗ 不是 自然的——它依赖于基的选择。行列式 ：一般线性群到非零乘法的行列式映射 det : GL n → R × det : GL n → R × 列表反转 ：在函数式编程中，reverse :: [a] -> [a] 是恒等函子到自身的自然变换。
给定范畴 C C D D C C D D [ C , D ] [ C , D ] D C D C 函子范畴 ：
对象：函子 F : C → D F : C → D
态射：自然变换 η : F → G η : F → G
函子范畴是范畴论中的高级结构，它把"函子之间的关系"也纳入范畴化框架。
Yoneda 引理是范畴论中最深刻的结果之一，被誉为"范畴论的基石"。
对于局部小范畴 C C A ∈ C A ∈ C F : C → Set F : C → Set
Nat ( Hom ( A , − ) , F ) ≅ F ( A ) Nat ( Hom ( A , − ) , F ) ≅ F ( A )
即从 Hom 函子 Hom ( A , − ) Hom ( A , − ) F F F ( A ) F ( A ) A A F F
Yoneda 引理最重要的推论是Yoneda 嵌入 ：
C ↪ [ C op , Set ] C ↪ [ C op , Set ]
它将每个对象 A A Hom ( − , A ) Hom ( − , A ) f : A → B f : A → B Hom ( − , f ) : Hom ( − , A ) → Hom ( − , B ) Hom ( − , f ) : Hom ( − , A ) → Hom ( − , B )
Yoneda 嵌入是全忠实 的（fully faithful），即：
Hom C ( A , B ) ≅ Nat ( Hom ( − , A ) , Hom ( − , B ) ) Hom C ( A , B ) ≅ Nat ( Hom ( − , A ) , Hom ( − , B ) )
这意味着：范畴中的对象完全由其与其他对象的关系决定 。这与范畴论的"关系优先"视角完全一致。
Yoneda 引理告诉我们：
知之全在于其关联 ：一个对象完全由它到其他对象的所有态射决定。交换图即证明 ：如果某性质对 A A B B 替换原理 ：在范畴论中，可以用自然变换 η η A A η A η A F ( A ) F ( A ) x ∈ F ( A ) x ∈ F ( A )
在 Haskell 中，Yoneda 引理体现为 Yoneda 数据类型：
data Yoneda f a = Yoneda (forall b. (a -> b) -> f b)
Yoneda f a 与 f a 同构，但 Yoneda 上的 fmap 是 O ( 1 ) O ( 1 ) pipes 和 conduit）中有实际应用。
极限（Limit）和余极限（Colimit）是范畴中统一处理数学构造的通用框架。
图表（Diagram） 是类型范畴 J J C C D : J → C D : J → C J J 索引范畴 ，通常是小范畴。
锥（Cone） 到图表 D D C ∈ C C ∈ C α j : C → D ( j ) α j : C → D ( j ) j ∈ J j ∈ J J J u : j → k u : j → k D ( u ) ∘ α j = α k D ( u ) ∘ α j = α k α α
余锥（Cocone） 是方向反转的锥。
图表 D : J → C D : J → C 极限 （Limit）是一个锥 ( L , π j : L → D ( j ) ) ( L , π j : L → D ( j ) ) 泛性质 ：对任意其他锥 ( C , α j ) ( C , α j ) u : C → L u : C → L j j π j ∘ u = α j π j ∘ u = α j L = ← D L = lim ← D lim D lim D
索引范畴
极限
具体构造（在 Set 中）
空范畴
终对象
单点集 { ∗ } { ∗ }
两个离散对象
积
A × B A × B
平行态射 A ⇉ B A ⇉ B
等化子
{ a ∈ A ∣ f ( a ) = g ( a ) } { a ∈ A ∣ f ( a ) = g ( a ) }
拉回图 A → C ← B A → C ← B
拉回（Fiber product）
{ ( a , b ) ∣ f ( a ) = g ( b ) } { ( a , b ) ∣ f ( a ) = g ( b ) }
索引范畴
余极限
具体构造（在 Set 中）
空范畴
始对象
∅ ∅
两个离散对象
余积
A ⊔ B A ⊔ B
平行态射
余等化子
B / ∼ B / ∼ f ( a ) ∼ g ( a ) f ( a ) ∼ g ( a )
推出图 A ← C → B A ← C → B
推出（Pushout）
( A ⊔ B ) / ∼ ( A ⊔ B ) / ∼
如果范畴中所有小极限都存在，称该范畴是完备的 （Complete）。
如果所有小余极限都存在，称该范畴是余完备的 （Cocomplete）。
Set 、Grp 、Top 、Vectₖ 等常见范畴都是完备且余完备的。
拉回（Pullback） ：给定 f : A → C f : A → C g : B → C g : B → C A × C B A × C B p A , p B p A , p B
A ×_C B --p_B--> B
| |
p_A g
v v
A ---- f ----> C
在 Set 中，A × C B = { ( a , b ) ∣ f ( a ) = g ( b ) } A × C B = { ( a , b ) ∣ f ( a ) = g ( b ) }
推出（Pushout） ：拉回的对偶。在 Set 中，它是无交并的商。
伴随函子（Adjoint Functor）是范畴论中最优雅的构造之一，它在不同范畴之间建立了双向的、自然的关系。
给定函子 F : C → D F : C → D G : D → C G : D → C F F G G 左伴随 （F ⊣ G F ⊣ G
Hom D ( F ( A ) , B ) ≅ Hom C ( A , G ( B ) ) ( 对 A ∈ C , B ∈ D ) Hom D ( F ( A ) , B ) ≅ Hom C ( A , G ( B ) ) ( 对 A ∈ C , B ∈ D )
伴随对 ( F , G ) ( F , G ) η : id C → G ∘ F η : id C → G ∘ F ϵ : F ∘ G → id D ϵ : F ∘ G → id D
G ϵ ∘ η G = id G G ϵ ∘ η G = id G ϵ F ∘ F η = id F ϵ F ∘ F η = id F
左伴随 F
右伴随 G
范畴
自由群函子
遗忘函子 U : Grp → Set U : Grp → Set
Set ⟷ Grp
自由向量空间
遗忘 U : Vect k → Set U : Vect k → Set
Set ⟷ Vectₖ
离散拓扑
遗忘 U : Top → Set U : Top → Set
Set ⟷ Top
积 ( − ) × A ( − ) × A
Hom [ A , − ] [ A , − ]
任意有幂的闭范畴
张量积 ( − ) ⊗ A ( − ) ⊗ A
[ A , − ] [ A , − ] Vectₖ
F ⊣ G F ⊣ G η : id C → G ∘ F η : id C → G ∘ F X ∈ Ob ( C ) X ∈ Ob ( C ) f : X → G ( Y ) f : X → G ( Y ) g : F ( X ) → Y g : F ( X ) → Y G ( g ) ∘ η X = f G ( g ) ∘ η X = f
这给出了伴随的泛元刻画 ：η X : X → G ( F ( X ) ) η X : X → G ( F ( X ) ) X X G G
重要事实 ：左伴随保持所有存在的余极限（即 F ( colim D ) ≅ colim ( F ∘ D ) F ( colim D ) ≅ colim ( F ∘ D )
在 Haskell 中，curry 和 uncurry 是一对伴随：
curry :: ((a, b) -> c) -> (a -> b -> c)
uncurry :: (a -> b -> c) -> ((a, b) -> c)
这对应了指数对象 C B C B B × A B × A ( − × B ) ⊣ ( − ) B ( − × B ) ⊣ ( − ) B
函子 F : C → Set F : C → Set 可表示的 （Representable），如果它自然同构于某个 Hom 函子 Hom ( A , − ) Hom ( A , − ) ( A , ρ ) ( A , ρ ) F F ρ : Hom ( A , − ) ≅ F ρ : Hom ( A , − ) ≅ F
由 Yoneda 引理，ρ ρ ρ A ( id A ) ∈ F ( A ) ρ A ( id A ) ∈ F ( A ) 泛元 。
函子
表示对象
含义
Hom ( G , − ) : Grp → Set Hom ( G , − ) : Grp → Set 整数群 Z Z
群同态由生成元决定
( − ) × : Ring → Set ( − ) × : Ring → Set Z [ x , x − 1 ] Z [ x , x − 1 ] 单位群泛环
P : Set op → Set P : Set op → Set { 0 , 1 } { 0 , 1 } 子集由特征函数决定
可表示函子是范畴论连接具体数学对象的关键桥梁。许多构造（自由对象、极限、伴随函子）都可以等价的用可表示性来刻画。例如，说"范畴 C C Hom ( X , − ) : C → Set Hom ( X , − ) : C → Set
范畴上的单子由三元组 ( T , η , μ ) ( T , η , μ )
T : C → C T : C → C η : id C → T η : id C → T μ : T 2 → T μ : T 2 → T
满足以下公理（类似于幺半群中的单位元和结合律，但适用于函子）：
T^3 --Tμ--> T^2 T --ηT--> T^2 <--Tη-- T
| | | | |
μT μ \ μ /
v v \ v /
T^2 --- μ ---> T \ T /
\ η /
\ / /
T /
即：
μ ∘ T μ = μ ∘ μ T μ ∘ T μ = μ ∘ μ T μ ∘ η T = id T = μ ∘ T η μ ∘ η T = id T = μ ∘ T η
每个伴随对 ( F ⊣ G ) ( F ⊣ G ) T = G ∘ F : C → C T = G ∘ F : C → C
η : id → T η : id → T μ = G ϵ F : T 2 → T μ = G ϵ F : T 2 → T ϵ ϵ
反之，每个单子都可以由至少一个伴随对产生（有 Eilenberg-Moore 和 Kleisli 两种标准构造）。
给定单子 ( T , η , μ ) ( T , η , μ ) C C Eilenberg-Moore 范畴 C T C T T T ( A , h : T ( A ) → A ) ( A , h : T ( A ) → A ) h h
h ∘ η A = id A h ∘ η A = id A h ∘ T ( h ) = h ∘ μ A h ∘ T ( h ) = h ∘ μ A
态射 f : ( A , h ) → ( B , k ) f : ( A , h ) → ( B , k ) C C f : A → B f : A → B f ∘ h = k ∘ T ( f ) f ∘ h = k ∘ T ( f )
遗忘函子 U T : C T → C U T : C T → C F T F T ( F T ⊣ U T ) ( F T ⊣ U T ) T T
在 Haskell 中，Monad 类型类定义如下：
class Applicative m => Monad m where
return :: a -> m a -- η
(>>=) :: m a -> (a -> m b) -> m b
-- join :: m (m a) -> m a -- μ
常见单子：
Maybe ：处理可能的失败（空值）List ：非确定计算IO ：副作用管理State ：可变状态Reader ：只读环境Writer ：日志写入Either ：带错误信息的异常处理
余单子是单子的对偶："反转所有箭头"得到的结构。余单子 ( K , ϵ , δ ) ( K , ϵ , δ )
函子 K : C → C K : C → C
余单位 ϵ : K → id C ϵ : K → id C
余乘法 δ : K → K 2 δ : K → K 2
在编程中，余单子表示"抽取值上下文"的模式。常见有余单子包括：(E, -)（Writer 对偶）、Stream（无限流）、Store（类似可以通过焦点访问的数据结构）。
Kan 扩张是许多范畴论构造的统一定义，包括极限、伴随函子、Yoneda 嵌入等。
给定函子 F : A → C F : A → C K : A → B K : A → B F F K K 左 Kan 扩张 是一个函子 Lan K F : B → C Lan K F : B → C η : F → Lan K F ∘ K η : F → Lan K F ∘ K G : B → C G : B → C γ : F → G ∘ K γ : F → G ∘ K α : Lan K F → G α : Lan K F → G α K ∘ η = γ α K ∘ η = γ
右 Kan 扩张 Ran K F Ran K F
许多范畴论构造都可以视为 Kan 扩张的特例：
构造
Kan 扩张的形式
余极限
Lan Δ F Lan Δ F Δ Δ
极限
Ran Δ F Ran Δ F
左伴随
Lan K F Lan K F K K K = id K = id
Yoneda 嵌入
F ( A ) → Lan Y F F ( A ) → Lan Y F Y Y
阿贝尔范畴（Abelian Category）是线性代数可以在其中进行的范畴。它是同调代数的基础。
一个范畴 A A 阿贝尔范畴 ，如果满足：
A A A A 每个态射有核和余核
每个单态射是某个态射的核，每个满态射是某个态射的余核
一组态射 A → f B → g C A f B g C 正合 （Exact）于 B B im ( f ) = ker ( g ) im ( f ) = ker ( g )
一个形如 0 → A → B → C → 0 0 → A → B → C → 0
A → B A → B 0 0 B → C B → C 0 0 im ( A → B ) = ker ( B → C ) im ( A → B ) = ker ( B → C )
在阿贝尔范畴中，给定交换图：
0 --> A' --> B' --> C' --> 0
| | |
α β γ
v v v
0 --> A --> B --> C --> 0
其中上下行都是正合序列，则存在正合序列：
ker ( α ) → ker ( β ) → ker ( γ ) → ∂ coker ( α ) → coker ( β ) → coker ( γ ) ker ( α ) → ker ( β ) → ker ( γ ) ∂ coker ( α ) → coker ( β ) → coker ( γ )
其中 ∂ ∂
阿贝尔范畴是导出函子（Derived Functor）理论的基础：
Ext n ( A , B ) Ext n ( A , B ) Hom ( − , B ) Hom ( − , B ) A A Tor n ( A , B ) Tor n ( A , B ) ( − ) ⊗ B ( − ) ⊗ B A A
一个 2-范畴 包含：
0-细胞（对象）
1-细胞（态射，即通常的态射）
2-细胞（态射之间的态射，即自然变换的泛化）
除了标准的复合律，2-范畴还要求交换律 （Interchange Law）：
( β ′ ∘ β ) ∗ ( α ′ ∘ α ) = ( β ′ ∗ α ′ ) ∘ ( β ∗ α ) ( β ′ ∘ β ) ∗ ( α ′ ∘ α ) = ( β ′ ∗ α ′ ) ∘ ( β ∗ α )
其中 ∘ ∘ ∗ ∗
所有小范畴构成一个 2-范畴 Cat ：
0-细胞：小范畴
1-细胞：函子
2-细胞：自然变换
垂直复合：自然的自然复合。水平复合：函子复合后的自然变换诱导。
严格 2-范畴 ：结合律和单位律严格成立。弱 2-范畴（双范畴） ：结合律和单位律只成立到 2-同构（即自然同构）。
在大多数应用中，弱版本更自然。例如范畴的范畴 Cat 实际上是双范畴，因为函子复合的严格结合律在集合论意义下不成立。
双范畴（Bicategory） 是弱化的 2-范畴，其中：
水平复合只是在同构意义下结合：( h ∘ g ) ∘ f ≅ h ∘ ( g ∘ f ) ( h ∘ g ) ∘ f ≅ h ∘ ( g ∘ f )
单位律在同构意义下成立：f ∘ id ≅ f ≅ id ∘ f f ∘ id ≅ f ≅ id ∘ f
这些同构满足余律条件 （Coherence Conditions）：五边形公理和三角形公理
∞-范畴 （无穷范畴）是包含任意维度的态射的范畴。根据"组合"规则的不同，有多种 ∞-范畴的概念：
拟范畴（Quasi-category） ：最常见的形式，用单纯集合（Simplicial Set）建模。严格 ∞-范畴 ：每一维的结合律都严格成立。弱 ∞-范畴 ：所有结合律只成立到更高维的同构。
高阶范畴是现代拓扑学、代数几何和理论物理的基础工具，在 Langlands 纲领、镜像对称等前沿领域有重要应用。
在程序语言理论中，可以将类型视为范畴的对象，纯函数视为态射：
Hask 范畴：Haskell 类型和函数复合是函数复合：( g ∘ f ) ( x ) = g ( f ( x ) ) ( g ∘ f ) ( x ) = g ( f ( x ) )
单位态射是 id
class Functor f where
fmap :: (a -> b) -> f a -> f b
函子定律（函子必须遵守）：
fmap id = id -- 保持单位态射
fmap (g . f) = fmap g . fmap f -- 保持复合
常见函子：
Maybe a：可能为空的值[a]：列表IO a：I/O 操作Either e a：带错误类型的值
在 Haskell 中，参数多态函数 f :: forall a. F a -> G a 通常就是自然变换（参数性保证了自然性条件）。
自由定理 ：Reynolds 的抽象定理指出，任何纯的、完全参数多态的函数自然满足自然性条件。这意味着编译器可以在不证明的情况下安全地依赖这些性质进行优化。
-- Maybe 单子处理链式空值
lookupUser :: Int -> Maybe User
lookupPost :: User -> Maybe Post
lookupComment :: Post -> Maybe Comment
getComment :: Int -> Maybe Comment
getComment uid = do
user <- lookupUser uid
post <- lookupPost user
lookupComment post
Monad 可以理解为"可编程的分号"——它允许程序员自定义计算的组合方式。这正是函数式编程中 monad 如此强大的原因：它们提供了控制流的抽象。
Haskell ：从范畴论中借鉴了 Functor、Monad、Applicative、Arrow、Monoid 等概念Scala ：通过 cats 库引入范畴论概念Rust ：通过 Iterator 等 trait 体现了函子的思想Agda/Idris ：依赖类型语言将范畴论概念直接嵌入类型系统Purescript ：Haskell 风格的语言，范畴论概念更贴近实际
语言
库/框架
提供的范畴论抽象
Haskell
标准库（base）
Functor, Monad, Applicative, Monoid
Scala
Cats
完整的范畴论抽象库
Scala
ZIO
基于函子和单子的 Effect System
Rust
futuresFuture = 单子（类似 Haskell 的 IO Monad）
Rust
itertools函子化的迭代器组合
TypeScript
fp-ts函数式编程的类型安全库
Swift
Swift 标准库
Optional / Result 等内建单子模式
Kotlin
Arrow
函数式编程库，含 Monad 等
Python
returns类型安全的函数式库
Java
Vavr
JVM 上的函数式编程库
-- 左单位律
return a >>= f = f a
-- 右单位律
m >>= return = m
-- 结合律
(m >>= f) >>= g = m >>= (\x -> f x >>= g)
可能单子（Maybe）的验证：
maybeLeftUnit :: a -> Maybe a -> (a -> Maybe b) -> Bool
maybeLeftUnit a _ f = (return a >>= f) == f a
-- True
maybeAssoc :: Maybe a -> (a -> Maybe b) -> (b -> Maybe c) -> Bool
maybeAssoc m f g = ((m >>= f) >>= g) == (m >>= (\x -> f x >>= g))
-- True
范畴论、类型理论和逻辑之间存在深刻的对应关系：
范畴论
类型论
逻辑
对象
类型
命题
态射
函数/项
证明（蕴涵）
复合
函数复合
假言推理
积
积类型
∧（与）
余积
和类型
∨（或）
终对象
单元类型
⊤（真）
始对象
Void 类型
⊥（假）
指数对象
函数类型
→（蕴涵）
笛卡尔闭范畴
STLC
IPL（直觉主义命题逻辑）
一个范畴 C C 笛卡尔闭范畴 （CCC），如果：
存在二元积（终端对象 + 所有有限积）
每个对象 B B ( − ) × B ( − ) × B ( − ) B ( − ) B
CCC 对应于直觉主义逻辑 的纯类型理论（Simply Typed Lambda Calculus）。它意味着：
每个类型都可以解释为一个对象
每个项都可以解释为一个态射
每个证明对应一个构造
拓扑斯 是一种特殊的范畴，它允许在其内部发展数学理论。一个（Grothendieck）拓扑斯是 Set Set
进行集合论推理（有幂对象、指数对象、子对象分类器）
构造内部逻辑（higher-order intuitionistic logic）
进行 Sheaf 论（层论）和逻辑验证
逻辑学家已经证明，在一个拓扑斯内部，即使排中律不成立，也可以发展全部的数学结构。这为构造性数学 和直谓主义逻辑 提供了理想的语义框架。
每个拓扑斯 E E 内部语言 （Internal Language），即一种高阶直觉主义类型理论。它使得我们可以用"普通的"逻辑和集合论记号在拓扑斯内部推理，而不必显式地写出范畴论公式。
这在实际应用中非常有用——例如，在代数几何中，通过变换拓扑斯（即改变"层"的基底空间），同样的逻辑公式可以在不同的几何设置下解释。
入门 ：能理解定义和基本示例
《Category Theory for Computing Science》- Barr & Wells
《Category Theory for Programmers》- Bartosz Milewski（有中文译本）
进阶 ：能从范畴论角度思考数学
《Basic Category Theory》- Tom Leinster
《Categories for the Working Mathematician》- Mac Lane（经典，较难）
《Conceptual Mathematics》- Lawvere & Schanuel
高阶 ：能开展范畴论研究或应用
《Sheaves in Geometry and Logic》- Mac Lane & Moerdijk
《Higher Topos Theory》- Jacob Lurie
nLab ：范畴论的社区维基百科，覆盖面极广Bartosz Milewski 的讲稿和视频 ：编程视角的范畴论入门Category Theory Zulip ：活跃的范畴论社区论坛The Stacks Project ：代数几何中范畴论的全面参考
对象 ──→ 范畴 ──→ 函子 ──→ 自然变换
| |
v v
泛性质 Yoneda引理
|
v
极限/余极限
|
v
伴随函子
|
v
单子/余单子
|
v
Kan 扩张
|
v
2-范畴/∞-范畴
范畴论从朴素的观察出发——"关系比属性更重要"——发展出了一整套改变现代数学面貌的理论体系。它的核心贡献在于：
统一性 ：将不同数学分支的共同模式提取出来，提供通用的语言和工具。关系优先 ：强调对象之间的关系而非内部结构，这导致了更抽象、更深刻的数学洞察。泛性质 ：通过外部关系唯一确定对象，避免了内部构造带来的无关细节。伴随性 ：揭示了"自由-遗忘"、"构造-保持"等普遍的对偶关系。
在编程中，范畴论提供了概念框架来理解和设计抽象接口（Functor、Monad、Applicative 等），极大地推动了纯函数式编程的发展和实用化。虽然初学者可能觉得范畴论过于抽象，但它就像"数学的望远镜"——将散落的领域收入同一视野，发现了之前无法想象的深层联系。
延伸阅读 ：本文是数学知识库的一部分。了解基础数学背景可参阅集合论 和数理逻辑 ；更深入的代数结构可参阅抽象代数 。