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

Question

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

Answer 1

正如夏立耀的回答所描述的那样，当我们没有或不想使用商时，使用setoids。
在 HoTT 书中和精益商数(基本上)是公理化的。 Lean 和 HoTT 书之间的一个区别在于，后者具有更多更高的归纳类型，而精益只有商和(常规)归纳类型。如果我们只关注商数(在 HoTT 书中设置商数)，它在 Lean 和 Book HoTT 中的作用相同。在这种情况下，您只需假设给定类型 A和等价 R在 A你有一个商数 Q ，以及一个函数 [-] : A → Q与属性(property)∀ x y : A, R x y → [x] = [y] .它带有以下消元原理:构造函数g : Q → X对于某些类型 X (或 hSet X 在 HoTT 中)我们需要一个函数 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(尤其是放弃证明无关性)。