为什么基于构造微积分的语言如此多地使用 Setoids？

如何解决为什么基于构造微积分的语言如此多地使用 Setoids？

有人发现 Setoids 广泛用于 Agda、Coq 等语言中……事实上，Lean 等语言认为它们可以帮助避免“Setoid Hell”。首先使用 Setoids 的原因是什么？ 转向基于 HoTT 的外延类型理论（例如立方 Agda）是否减少了对 Setoids 的需求？

解决方法

正如 Li-yao Xia 的回答所描述的，当我们没有或不想使用商时，使用 setoids。

在 HoTT 书中和精益商数（基本上）是公理化的。 Lean 和 HoTT 书之间的一个区别在于，后者具有更多更高的归纳类型，而精益只有商和（常规）归纳类型。如果我们只关注商数（在 HoTT 书中设置商数），它在 Lean 和 Book HoTT 中的作用相同。在这种情况下，您只需假设给定类型 A 和 R 上的等价 A，您有一个商 Q，以及一个具有属性的函数 [-] : A → Q ∀ x y : A,R x y → [x] = [y]。它带有以下消除原则：要为某种类型g : Q → X（或HoTT中的hSet X）构造一个函数X，我们需要一个函数f : A → X，以便我们可以证明∀ x y : A,R x y → f x = f y。这与计算规则一起提供，该规则声明 ∀ x : A,g [x] ≡ f x（这是 Lean 和 Book HoTT 中的定义相等）。

这个商的主要缺点是它破坏了规范性。 Canonicity 指出（比如说）自然数中的每个封闭项（即没有自由变量的项）都归一化为零或某个自然数的后继。这个商打破规范的原因是我们可以将 = 的消除原理应用于商中的新等式，并且这样的术语不会减少。精益的观点是这并不重要，因为在我们关心的所有情况下，我们仍然可以证明相等，即使它可能不是定义的相等。

立方类型理论有一种奇特的方式来处理商，同时保持规范性。在 CTT 中，相等的工作方式不同，这意味着可以在保持规范性的同时引入更高的归纳类型。 CTT 的潜在缺点是类型理论要复杂得多，而且你必须接受 HoTT（尤其是放弃证明无关性）。

,

[Lia-yao Xia 和 Floris van Doorn 的回答都很棒，所以我会尝试添加更多信息。]

另一种观点认为，虽然在古典数学中经常使用商，但毕竟可能并不是那么好。不取商但坚持 Groupoids 正是非交换几何的起点！它告诉我们，有些商的行为非常糟糕，我们最不想做的事情（在这些情况下！）就是实际计算商。但是，如果您使用“正确”的工具来对待它，那么事情本身并没有那么糟糕，甚至还不错。

可以说，它也深深植根于所有范畴论中，其中人们不会对等价的对象进行商数。在范畴论中采用“骨架”被认为是不合时宜的。严格也是如此，还有许多其他事情，所有这些都归结为试图压制那些最好保持原样的东西，因为它们根本没有伤害。我们只是习惯于希望在我们的表现中体现“独特性”——这是我们应该克服的。

Setoid 地狱的出现并不是因为必须证明某些连贯性（您需要证明它们以表明您具有适当的等价性，并且每当您在原始表示而不是商版本上定义函数时再次证明）。当您在定义不可能“出错”的函数时被迫一次又一次地证明这些一致性时，就会出现这种情况。所以Setoid地狱实际上是由于没有提供适当的抽象机制造成的。

换句话说，如果您正在做足够简单的数学运算，其中商数表现良好，那么应该有一些自动化可以让您顺利进行。目前，在类型理论中，正在研究到底它可能是什么样子。弗洛里斯的回答很好地概括了一个陷阱：在某些时候，你放弃了计算将是良性的，从那时起，被迫通过证明来做所有事情。

,

理想情况下，人们当然希望能够将任意等价关系视为莱布尼茨等式 (eq)，从而能够在任意上下文中进行重写。这意味着通过等价关系定义类型的商。

我不是该主题的专家，但我一直在思考同样的问题，我认为对 setoids 的依赖源于这样一个事实，即商在类型理论中仍然是一个鲜为人知的概念。

>

1. 当我们没有/不需要商类型时，我们就会陷入困境。
2. 我们可以公理化商数类型，我相信（我可能会误会）这就是精益所做的。
3. 我们可以开发一种可以自然表达商的类型理论，这就是 HoTT/Cubical TT 对更高归纳类型所做的。

此外，商类型（或我对它们的天真想象）迫使我们以一种可能不太理想的方式将程序和证明打包在一起：两个商类型之间的函数是一个普通函数以及它尊重的证明潜在的等价关系。虽然从技术上讲可以做到这一点，但这种编程和证明的交织可以说是不可取的，因为它使程序不可读：人们经常寻求将程序和证明保存在两个完全独立的世界中（以便强制使用 setoid，将类型与其等价关系分开） ，或者改变一些表示，使程序和证明是同一个实体（所以我们甚至可能不需要首先明确地推理等价性）。