对为什么所有单型形态与身份形态不相同的原因感到困惑

Question

我正忙于阅读Bartosz Milewski的程序员类别理论书籍，而我在描述非身份形态的描述是在描述单型物体作为一组和单型类别时的描述。

我了解到，当在的背景下查看单型（例如字符串）时，我们有兴趣描述使用“附加”特征的各种功能，例如一个函数附加“狗”或将“ mmm”附加到收到的输入的功能。这些功能将分别将其输入映射到字符串集中的另一个元素。这显然包括任何一无所有的可能性。

据我所知，当我们在的背景下查看此MONOID 时，据我了解，我们正在缩放到一个抽象级别，其中这种单体对象代表整个“字符串”类型，而我们没有对这种类型中元素互相映射的方式感兴趣，因为我们已经将整个类型表示为单数点/对象。

之后，我认为在此抽象级别上，“集合”上下文中描述的所有函数看起来都相同，因为它们都映射了字符串 - ＆gt;细绳。在我看来，这意味着在类别的上下文中，身份函数（无附加）看起来与附录狗或附录函数相同，或者与此相关的任何其他函数。

不过，我的理由显然是不正确的，如看书中的这张图，从单型物体到自身的态度显示为独特的实体：

作为结尾语句/摘要： 我不明白为什么一旦我们将其提取为类别，我们仍然对在单体集中描述功能感兴趣。一旦集合成为一个类别中的对象，该对象代表整个类型，该集合中的所有功能都将不像身份函数，因为从我们的新优势开始，它们似乎都是从该类型开始的，并返回到此类型。

我希望我已经清楚地表明了我的困惑。 在此先感谢您的任何帮助！

Answer 1

我相信您正在观察到的事实是，每个单人物都对微不足道的单体都是同态的。如果您只查看任何单体的点和箭头图，它也是微不足道的单体的有效图，但是该图不是整个图片。

当您“抽象”时，您实际上是在抛弃对单体的等价关系，并补充最弱的关系。附加“ mm”和附加“” 是不同的，但该图并未说明这一点。可以想象它们是平等的，您将获得有效的单体，但这会改变等效关系。

即使我们丢弃了一些细节，它们是不平等（或至少可能是不平等）的事实，也不应丢弃。这对结构很重要。

Answer 2

也许一个具体的例子会使这更容易讨论。因此，这是我的具体示例：

   t
┌────┐
│    ▼
└─── • ◀──┐
     │    │
     └────┘
       f

这是一个具有一个对象（•）和两个形态（t和f）的类别。这是一个完整的类别定义吗？不，我们需要另一件事，即构图的定义。我将其作为查找表。

f ∘ f = f
f ∘ t = t
t ∘ f = t
t ∘ t = f

这是一个完整的类别定义吗？不，我们还需要一件事，即我们需要确定每个对象的形态，以作为一个身份。对于此类别，只有一个对象，f具有适合该对象的正确行为。

这是一个完整的类别定义吗？是的！您可能需要验证类别定律 - f x = x f f = x ，然后（ x y ）∘ z = x ∘（） y z ） - 但是，您也欢迎您相信我。 如果它有助于您对这些证明的直觉，则可能需要将f读为“ false”，t为“ true”，而为Xor。）

（ 那是一个对象类别。希望很明显，并非所有的形态都是一样的。肯定是正确的和错误似乎是不同的概念！

现在，将类别的上述定义与monoid的以下定义进行比较。要定义一个单体，我们必须给出一个集合的三重（M， +，0），二进制操作和身份。定义：

M = {f, t}
f + f = f
f + t = t
t + f = t
t + t = f
0 = f

这指定了XOR下的布尔值。请注意我们的两个发展有多相似。对于类别，我们给出了一个点和箭头图，该图确定了两个箭头，f和t，而对于monoid定义，我们给出了一个包含两个元素的集合， f和t。对于该类别，我们给了一个组成操作员，将两个形态结合在一起，而对于Monoid来说，我们给了一个操作员，该操作员占据了两个元素并返回了一个元素。对于类别，我们将f识别为身份形态，而对于monoid，我们将f确定为身份元素。对于该类别，我们证明了∘是关联的，而对于Monoid来说，我们证明了 +是关联的。对于该类别，我们证明了具有f的构图什么都不做，而对于Monoid，我们证明了添加到f中，没有任何作用。

我们需要提供的数据来定义一个单体，并且我们需要提供的数据来定义单对象类别是相同的！