我有点不确定这是一个 math.SE 问题还是一个 SO 问题，但我怀疑数学家一般不太可能特别了解或关心这一类别，而 Haskell 程序员可能会这样做。
因此，我们知道Hask 或多或少有产品（当然，我在这里使用的是理想化的 Hask）。我对它是否有均衡器很感兴趣（在这种情况下它会有所有有限的限制）。
直觉上似乎不是，因为你不能像在集合上那样进行分离，所以子对象通常似乎很难构造。但是对于您想提出的任何特定情况，似乎您可以通过在Set中计算均衡器并对其进行计数来破解它（毕竟，每种 Haskell 类型都是可数的，并且每个可数集都是同构于有限类型或自然数，Haskell 都有）。所以我看不出我将如何寻找反例。
现在，Agda 似乎更有希望了：在那里形成子对象相对容易。明显的 sigma 类型Σ A (λ x → f x == g x)是均衡器吗？如果细节不起作用，它在道德上是一个均衡器吗？
tl;博士提议的候选人不是一个均衡器，但它不相关的对应物是
Agda 的均衡器候选人看起来不错。所以让我们试试吧。我们需要一些基本的工具包。这是我的拒绝 ASCII 依赖对类型和同质内涵平等。
record Sg (S : Set)(T : S -> Set) : Set where
constructor _,_
field
fst : S
snd : T fst
open Sg
data _==_ {X : Set}(x : X) : X -> Set where
refl : x == x
这是您的两个功能均衡器的候选人
Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S \ s -> f s == g s
随着fst投影发送Q f g到S。
它说什么：元素 ofQ f g是s源类型的元素，以及f s == g s. 但这是均衡器吗？让我们试着做到这一点。
要说均衡器是什么，我应该定义函数组合。
_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)
所以现在我需要证明任何h : R -> S可以识别f o h并且g o h必须通过候选人的因素fst : Q f g -> S。我需要提供其他组件u : R -> Q f g以及确实h因素为fst o u. 图片如下：(Q f g , fst)是一个均衡器，如果每当图表通勤时没有u，有一种独特的方式可以添加u图表仍然通勤。
这就是中介的存在u。
mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
(q : (f o h) == (g o h)) ->
Sg (R -> Q f g) \ u -> h == (fst o u)
S显然，我应该选择相同的元素h。
mediator f g h q = (\ r -> (h r , ?0)) , ?1
留给我两项证明义务
?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)
现在，?1可以就像reflAgda 的定义等式具有函数的 eta 定律一样。因为?0，我们是被祝福的q。同等功能尊重应用
funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl
所以我们可以采取?0 = funq q r。
但是让我们不要过早地庆祝，因为中介态射的存在是不够的。我们还需要它的独特性。而这里的轮子很可能会变得不稳定，因为==它是内涵的，所以唯一性意味着只有一种方法可以实现中介映射。但是，我们的假设也是内涵的……
这是我们的证明义务。我们必须证明任何其他中介态射等于 选择的那个mediator。
mediatorUnique :
{R S T : Set}(f g : S -> T)(h : R -> S) ->
(qh : (f o h) == (g o h)) ->
(m : R -> Q f g) ->
(qm : h == (fst o m)) ->
m == fst (mediator f g h qh)
我们可以立即替换 viaqm并得到
mediatorUnique f g .(fst o m) qh m refl = ?
? : m == (\ r -> (fst (m r) , funq qh r))
看起来不错，因为 Agda 有记录的 eta 定律，所以我们知道
m == (\ r -> (fst (m r) , snd (m r)))
但是当我们尝试制作时? = refl，我们得到了投诉
snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))
这很烦人，因为身份证明是唯一的（在标准配置中）。现在，您可以通过假设外延性并使用其他一些关于平等的事实来摆脱这种情况
postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g
sndq : {S : Set}{T : S -> Set}{s : S}{t t' : T s} ->
t == t' -> _==_ {Sg S T} (s , t) (s , t')
sndq refl = refl
uip : {X : Set}{x y : X}{q q' : x == y} -> q == q'
uip {q = refl}{q' = refl} = refl
? = ext (\ s -> sndq uip)
但这太过分了，因为唯一的问题是烦人的等式证明不匹配：实现的可计算部分在鼻子上匹配。所以解决方法是使用无关紧要的工作。我用 istential 量词代替Sg，Ex它的第二个分量用点标记为不相关。现在，我们使用哪种证据证明证人是好的并不重要。
record Ex (S : Set)(T : S -> Set) : Set where
constructor _,_
field
fst : S
.snd : T fst
open Ex
并且新的候选均衡器是
Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S \ s -> f s == g s
整个施工过程和以前一样，除了最后一个义务
? = refl
被接受！
所以是的，即使在内涵设置中，eta 定律和将字段标记为不相关的能力也给了我们均衡器。
在这个构造中没有涉及不可判定的类型检查。
Hask 没有均衡器。要记住的重要一点是，考虑类型（或任何类别中的对象）及其同构类确实需要考虑箭头。您对基础集的说法是正确的，但是具有同构基础集的类型当然不一定是同构的。Hask 和 Set 之间的一个区别是 Hask 的箭头必须是可计算的，实际上对于理想化的 Hask，它们必须是全部的。
我花了一段时间试图提出一个真正可以辩护的反例，并发现一些参考资料表明它无法做到，但没有证据。但是，如果您愿意，我确实有一些“道德”反例；我无法证明 Haskell 中不存在均衡器，但这似乎是不可能的！
f, g: ([Int], Int) -> Int
f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0
均衡器“应该”是所有对 (p,n) 的类型，其中 p(n) = 0，以及将这些对注入 ([Int], Int) 的函数。由希尔伯特的第 10 个问题，这个集合是不可判定的。在我看来，这应该排除它是 Haskell 类型的可能性，但我无法证明这一点（是否有可能有一些奇怪的方法来构建这种没有人发现的类型？）。也许我没有连接一两个点——也许证明这是不可能的并不难？
假设您有一种编程语言。你有一个编译器，它接受源代码和输入并生成一个函数，函数的固定点是输出。（虽然我们没有这样的编译器，但类似这样的指定语义并非闻所未闻）。所以你有了
compiler : String -> Int -> (Int -> Int)
(Un)curry 到一个函数中
compiler' : (String, Int, Int) -> Int
并添加一个功能
id' : (String, Int, Int) -> Int
id' (_,_,x) = x
那么编译器的均衡器“id”将是源程序、输入、输出的三元组的集合——这是不可计算的，因为编程语言是完全通用的。
选择你最喜欢的不可判定问题：它通常涉及判定一个对象是否是某个集合的成员。您通常有一个总函数，可用于检查特定对象的此属性。您可以使用此函数创建一个均衡器，其中类型应该是您不可判定集合中的所有项目。这就是前两个例子的来源，而且还有很多。
我对Agda不太熟悉。我的直觉是你的 sigma-type 应该是一个均衡器：你可以写下类型，以及必要的注入函数，它看起来完全满足定义。但是，作为一个不使用 Agda 的人，我觉得我真的没有资格去查看细节。
但真正的实际问题是对 sigma 类型的类型检查并不总是可计算的，因此这样做并不总是有用的。在上面的所有示例中，您可以写下您提供的 Sigma 类型，但是如果没有证明，您将无法轻松检查某物是否属于该类型的成员。
顺便说一句，这就是为什么 Haskell 不应该有均衡器的原因：如果有，类型检查将是不可判定的！依赖类型是让一切都打勾的原因。他们应该能够在其类型中表达有趣的数学结构，而 Haskell 则不能，因为它的类型系统是可决定的。所以，我自然会期望理想化的 Agda 具有所有有限的限制（否则我会感到失望）。其他依赖类型的语言也是如此。例如，Coq 绝对应该有所有限制。