简而言之,所提出的等式器并不完全是一个平衡器,但它的无关对应物却是如此。
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
。
它的含义是:
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)
所以现在我需要展示任何一个将
f o h
和
g o h
鉴别为同一函数的
h : R -> S
都必须通过候选的
fst : Q f g -> S
分解。我需要提供另一个组件
u : R -> Q f g
,并证明确实
h
可以分解为
fst o u
。这是图示:
(Q f g , fst)
是一个等价器,如果当图表在没有
u
的情况下交换时,有唯一的方法可以添加
u
使图表仍然保持交换。
![equaliser diagram](https://istack.dev59.com/odrtv.webp)
这里是中介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)
显然,我应该选择与h相同的S元素。
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 规律。对于
?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)
我们可以立即通过
qm
进行替换并获得。
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)
但这有些过度,因为唯一的问题是烦人的等式证明不匹配:实现的可计算部分完全匹配。所以解决方法是使用“不相关性”。我用“存在量词”替换了“Sg”,其第二个组件用点标记为不相关。现在我们使用哪个证明证明见证者是好的并不重要。
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定律和将字段标记为不相关的能力也给我们带来了等式器。
在这个构造过程中没有涉及不可判定类型检查。