请求解析范畴等价三角等式的Globular图示证明
嘿，这个Globular图示其实是用**高维范畴论里的“粘贴图”**来可视化自然变换之间的复合与交换关系，我给你拆解一下，把它转成直白的自然语言证明：
首先先明确已知条件：
我们有函子$F:C\to D$、$G:D\to C$，自然同构$\eta:1_C\cong GF$（单位变换）、$\epsilon:FG\cong 1_D$（余单位变换），而且已知**$F$对应的三角等式成立**：也就是自然变换的复合$F \xrightarrow{F\eta} FGF \xrightarrow{\epsilon F} F$是恒等变换（这里$F\eta$是$\eta$沿着$F$的左复合，$\epsilon F$是$\epsilon$沿着$F$的右复合）。
我们要证的是：$G$对应的三角等式$G \xrightarrow{\eta G} GFG \xrightarrow{G\epsilon} G$也是恒等自然变换。
图示的核心含义
这个Globular图是用2维的“粘贴”方式，把自然变换的复合、自然性条件串起来：
- 每个节点代表一个自然变换（比如最左/最右的$G$其实是恒等自然变换$1_G$）；
- 箭头代表自然变换之间的“修改”（2-变换），正方形区域则表示一组自然变换的复合是可交换的。
转成自然语言的证明步骤
从已知的$F$三角等式入手
已知$(\epsilon F) \circ (F\eta) = 1_F$，这个等式对每个对象$Y\in C$都成立：$\epsilon_{F(Y)} \circ F(\eta_Y) = 1_{F(Y)}$。关联到$G$的复合映射
对任意对象$X\in D$，我们取$Y=G(X)$代入上面的等式，得到：
$\epsilon_{FG(X)} \circ F(\eta_{G(X)}) = 1_{FG(X)}$应用函子$G$到等式两边
因为$G$是函子，它保持映射的复合和恒等映射，所以对上面的等式两边应用$G$后，左边变成$G(\epsilon_{FG(X)}) \circ G(F(\eta_{G(X)}))$，右边变成$G(1_{FG(X)}) = 1_{GFG(X)}$。利用自然变换的自然性
自然变换$\eta$的自然性告诉我们：对任意对象$Z$，$GF(\eta_Z) = \eta_{GF(Z)}$。这里$Z=G(X)$，所以$GF(\eta_{G(X)}) = \eta_{GFG(X)}$，而$G(F(\eta_{G(X)}))$其实就是$GF(\eta_{G(X)})$，也就是$\eta_{GFG(X)}$。推导目标复合的恒等性
我们的目标是证明$(G\epsilon_X) \circ (\eta_{G(X)}) = 1_{G(X)}$。结合上面的结论，我们可以看到：
$G(\epsilon_X) \circ \eta_{G(X)}$这个映射，在经过$F$作用后得到的是$1_{FG(X)}$。而因为$F$是范畴等价的一部分，它是忠实且满的（简单说就是$F$能区分不同的映射，不会把非恒等映射变成恒等），所以如果$F(f)=1_{FG(X)}$，那$f$本身一定是$1_{G(X)}$。
由此可得，$(G\epsilon_X) \circ (\eta_{G(X)}) = 1_{G(X)}$对所有$X\in D$都成立，也就是自然变换的复合$(G\epsilon) \circ (\eta G) = 1_G$。
本质上，这个Globular图就是把这些逻辑步骤用可视化的粘贴方式呈现，核心是借助已知的三角等式，通过函子的保复合性和自然变换的自然性，推导出另一组三角等式成立。
备注：内容来源于stack exchange，提问作者onRiv
