为什么基于构造微积分的语言如此多地使用Setoids？
有人发现 Setoids 被广泛用于 Agda、Coq 等语言中……事实上，Lean 等语言认为它们可以帮助避免“Setoid Hell”。首先使用 Setoids 的原因是什么？转向基于 HoTT（如立方体 Agda）的外延类型理论是否减少了对 Setoids 的需求？
回答
正如夏立耀的回答所描述的那样，当我们没有或不想使用商时，使用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为某种类型X（或XHoTT 中的hSet ）构造一个函数，我们需要一个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 的回答都很棒，所以我会尝试添加更多信息。]
另一种观点认为，商虽然在古典数学中被大量使用，但毕竟可能并不是那么好。未服用商却坚持群胚是确切其中非交换几何从开始！它告诉我们，有些商的表现非常糟糕，我们最不想做的事情（在这些情况下！）就是实际计算商。但是，如果您使用“正确”的工具来对待它，那么事情本身并没有那么糟糕，甚至还不错。
可以说，它也深深植根于所有范畴论中，在范畴论中，人们不会对等价的对象进行商数。在范畴论中采用“骨架”被认为是不合时宜的。严格也是如此，还有许多其他事情，所有这些都归结为试图压制那些最好保持原样的东西，因为它们根本没有伤害。我们只是习惯于希望“独特性”反映在我们的表现中——我们应该克服这一点。
Setoid 地狱的出现并不是因为必须证明某些连贯性（您需要证明它们以表明您具有适当的等价性，并且每当您在原始表示而不是商版本上定义函数时再次证明）。当您在定义不可能“出错”的函数时被迫一次又一次地证明这些一致性时，就会出现这种情况。所以Setoid地狱实际上是由于没有提供适当的抽象机制造成的。
换句话说，如果你正在做足够简单的数学，商数表现良好，那么应该有一些自动化，让你顺利地工作。目前，在类型理论中，正在研究到底它可能是什么样子。弗洛里斯的回答很好地概括了一个陷阱是什么：在某些时候，你放弃了计算将是良好的，从那时起，被迫通过证明来做所有事情。
回答
理想情况下，人们当然希望能够将任意等价关系视为莱布尼茨等式 ( eq)，从而能够在任意上下文中进行重写。这意味着通过等价关系定义类型的商。
我不是这个主题的专家，但我一直在想同样的问题，我认为对 setoids 的依赖源于这样一个事实，即商在类型理论中仍然是一个鲜为人知的概念。
- 当我们没有/想要商类型时，Setoid Hell 就是我们陷入困境的地方。
- 我们可以公理化商数类型，我相信（我可能会误会）这就是精益所做的。
- 我们可以开发一种可以自然表达商的类型理论，这就是 HoTT/Cubical TT 对更高归纳类型所做的。
此外，商类型（或我对它们的天真想象）迫使我们以一种可能不太理想的方式将程序和证明打包在一起：两个商类型之间的函数是一个简单的函数以及它尊重潜在等价的证明关系。虽然从技术上讲可以做到这一点，但这种编程和证明的交织可以说是不可取的，因为它使程序不可读：人们经常寻求将程序和证明保存在两个完全独立的世界中（以便强制使用 setoid，将类型与其等价关系分开） ，或者改变一些表示，使程序和证明是同一个实体（所以我们可能甚至不需要首先明确地推理等价性）。