我正在通过Bartosz Milewski关于类别理论的精彩博客。我被卡在products and coproducts上。
Bartosz说，两个物体a和b的产物是c的对象，配备两个投影，对于任何其他物体c'配备两个投影，有一个独特的态射m从c'到c，这是对这些投影的影响。
当然，我们可以在集合和函数的类别中找到合适的示例。 Int和Bool两种类型的产品是(Int, Bool)对。这两个投影是p (int, _) = int和q (_, bool) = bool。然而，还有Int和Bool产品的另一个候选者：它是Int类型，具有投影p' int = int和q' _ = True。正如巴托斯所说：“这很蹩脚，但它符合标准。”请注意，产品类型Int包含的值小于产品类型(Int, Bool)。确切地说是一半。尽管两种产品类型都可以映射到整个Int类型，但产品类型Int只能映射到Bool类型的一半。这不是满足的（如果这是正确的话）！
因为我们可以想出一个mormphism m :: (Int, Bool) -> Int（其中m只能被唯一地实现为m (int, _) = int）我们知道产品类型(Int, Bool)比Int更好。在这一点上我想知道：难道我们不能像m那样容易地实施m (int, _) = int + 1吗？这不是第二种态射吗？或者这是不允许的，因为产生的产品Int实际上根本不是Int，但是Int“转移”了1？
该
m中的箭头指向错误的方向。我们知道(Int, Bool)比Int“更好”，因为我们有一个态射m :: Int -> (Int, Bool)，m x = (x, True)。它满足条件p . m == p'和q . m == q'，这就是m分解p'和q'的含义。如果以任何其他方式定义m，则此条件将不成立。
例如，如果它被定义为m x = (x + 1, True)，那么p (m 0) == 1，但p' 0 == 0。
你的地图m' :: (Int, Bool) -> Int，如果它分解p和q，将指向Int也是一个合适的产品。但组成q' . m' :: (Int, Bool) -> Bool总是返回True，所以它不能等于q。