In the past recent years, I have been using string diagrams to teach basic category theory (adjunctions, Kan extensions, but also limits and Yoneda embedding). Using graphical notations is undoubtedly joyful, and brings us close to other graphical syntaxes of circuits, interaction nets, etc... It saves us from laborious verifications of naturality, which is built-in in string diagrams. On the other hand, the language of string diagrams is more demanding in terms of typing: one may need to introduce explicit coercions for equalities of functors, or for distinguishing a morphism from a point in the corresponding internal homset. So that in some sense, string diagrams look more like a language "a la Church", while the usual mathematics of, say, Mac Lane's "Categories for the working mathematician" are more "a la Curry".
展开▼
机译：在过去的几年中，我一直在使用字符串图来教授基本的范畴论（附加，Kan扩展，还包括极限和Yoneda嵌入）。使用图形表示法无疑是一件很快乐的事情，它使我们接近电路，交互网络等其他图形语法。它使我们免于费力地验证自然性（它内置在字符串图中）。另一方面，字符串图的语言在类型方面要求更高：可能需要为函子的相等性引入显式强制，或从相应内部同位点中区分态射。因此，从某种意义上讲，字符串图看起来更像是一种“ la la Church”语言，而Mac Lane的“适用于数学家的类别”的常用数学则更像是“ la la Curry”。
展开▼
