haskell - Hask或Agda是否有均衡器？

对于这是一个数学问题还是一个SE问题，我并不确定，但是我怀疑，一般而言，数学家不太可能特别了解或特别关心这一类别，而Haskell程序员则可能会做得很好。

因此，我们知道 Hask 或多或少都有产品(我在这里与Idealized-Hask一起工作)。我对它是否具有均衡器感兴趣(在这种情况下，它将具有所有有限的极限)。

从直觉上看似乎不是，因为您不能像在集合上那样进行分离，因此通常很难构造子对象。但是对于您想提出的任何特定情况，似乎您都可以通过在设置中计算均衡器并对其进行计数来破解(毕竟，每种Haskell类型都是可数的，并且每种可数set是同构的，要么是有限类型的，要么是自然的，Haskell都具有)。因此，我看不到如何找到反例。

现在，Agda似乎更有希望:形成子对象相对容易。明显的sigma类型Σ A (λ x → f x == g x)是均衡器吗？如果细节不起作用，从道德上讲是均衡器吗？

最佳答案

拟议的候选人不是一个均衡者，但不相关的候选人是

阿格达均衡器的候选人看起来不错。因此，让我们尝试一下。我们需要一些基本的工具包。这是我拒绝的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中。

它说的是:Q 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可以只是refl，因为Agda的定义相等性具有函数的eta-law。对于?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。

但是，让我们不要过早地庆祝，因为存在中介态态是不够的。我们还需要它的独特性。而且由于==是内涵性的，因此这里的轮子很可能会出现问题，因此唯一性意味着只有一种方法可以实现中介 map 。但是然后，我们的假设也是故意的...

这是我们的证明义务。我们必须证明，任何其他中介态与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)

我们可以立即通过qm替换并获取

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (\ r -> (fst (m r) , funq qh r))

看起来不错，因为阿格达有记录的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)

但这太过分了，因为唯一的问题是令人讨厌的相等证明不匹配:实现的可计算部分在 Nose 上匹配。因此，解决方法是不相关地工作。我将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法则和将字段标记为不相关的能力也使我们获得了均衡。

此构造中不涉及不确定的类型检查。

关于haskell - Hask或Agda是否有均衡器？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/15047775/