tl;dr提案された候補はイコライザーではありませんが、その無関係な対応物は
Agda のイコライザーの候補は良さそうです。それでは、試してみましょう。基本キットが必要です。これが私の rejectnik 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
2つの関数のイコライザーの候補は次のとおりです
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 hanyを示す必要があります。他のコンポーネントと、実際にとして因数分解する証明の両方を提供する必要があります。これが図です:ダイアグラムが なしで交換するときはいつでも、ダイアグラムがまだ交換されている状態で追加する独自の方法がある場合、 はイコライザーです。g o hfst : Q f g -> Su : R -> Q f ghfst o u(Q f g , fst)uu
ここに仲介の存在が入り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
2つの立証義務を残して
?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)
さて、Agda の定義上の等価性が関数の eta-law を持っているの?1と同じようにできます。reflというのは?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。
しかし、時期尚早に祝うのはやめましょう。媒介射の存在だけでは十分ではないからです。その独自性も必要です。==そして、ここではホイールが不安定になる可能性があります。これはintensional であるためです。一意性とは、仲介マップを実装する方法が 1 つしかないことを意味します。しかし、私たちの仮定は意図的なものでもあります...
これが私たちの証明義務です。他の仲介射は によって選択されたものと等しいことを示さなければなりません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)
qmviaと getをすぐに置き換えることができます
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)
唯一の問題は厄介な等式証明の不一致です: 実装の計算可能な部分がノーズで一致します。したがって、修正は irrelevance で動作することです。Sg2 番目のコンポーネントが無関係であるとドットでマークされているExistential 量指定子に置き換えます。さて、証人が優れているという証拠をどのように使用するかは問題ではありません。
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
受け入れられます！
そうです、意図的な設定であっても、イータの法則と、フィールドを無関係としてマークする機能により、イコライザーが得られます。
この構築には決定不能な型チェックは含まれていません。