Universal mapping と、Free Monoid を使った例
Menu MenuUniversal mapping Problem とは
Category A, B 、B から A への Functor U 、Aの対象から Bの対象への写像 F、さらに、a から、A の対象 a から UF(a) への射を返す写像η があるとします。任意の f : a → U(b) に対して、
U(f*)η(a) = f
となるような唯一の f* : F(a) → b を Univeral mapping problem の解と言いいます。
f*
F(a) -----------→ b
UF(a) ---------→ U(b)
^
|
η(a)| f
|
a
f = U(f*)η
ηは、もちろん、随伴関手の自然変換 ηに対応するものです。F も関手になるべきものです。そして、自然変換 ε を定義できれば、Universal mapping を導くことができます。
η(a) は、a から UF(a) へのたくさんの射の中から、ただ一つを選び出す写像だと考えることができます。
この問題の定義は cat-utility に書いてあります。
record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
( F : Obj A → Obj B )
( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
field
universalMapping : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } →
A [ A [ FMap U ( f * ) o η a ] ≈ f ]
uniquness : {a : Obj A} { b : Obj B } → { f : Hom A a (FObj U b) } → { g : Hom B (F a) b } →
A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ]
record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
infixr 11 _*
field
F : Obj A → Obj B
η : (a : Obj A) → Hom A a ( FObj U (F a) )
_* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b
isUniversalMapping : IsUniversalMapping A B U F η _*
record が二つに分かれているので、何が入力なのか、存在するものは何かが明確になっています。入力は圏A,B二つそして、その間の凾手 U です。_* は普遍問題の解で、さらに写像Fと射η(a)が出てきます。
universalMapping は普遍問題の性質、
A [ A [ FMap U ( f * ) o η a ] ≈ f ]
つまり、U(f*)η = f です。
さらに、「ただ一つ」でなければなりません。つまり、U(g)η = f があったら、それは f* 。これが uniquness
A [ A [ FMap U g o η a ] ≈ f ] → B [ f * ≈ g ]
というわけです。_* を定義して、universalMapping の証明と uniquness の証明によって UniversalMapping が構成されます。Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) というめんどくさい Levvel を持っていますが、Categoryを二つ含む定理では、いつものことです。
( U : Functor B A )
( F : Obj A → Obj B )
( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
が登場要素ですが、Functor なのは U だけです。F はFunctor になりたいし、ηは自然変換になりたいわけですが、必要最小限な要求だけを書いています。あとで、_* があれば Functor と自然変換であることを示します。証明できるので、ここでは不要なわけです。
Free Mnooid の例
Monoid とは結合法則を満たすだた一つの演算と単位元を一つ持つ代数でした。集合a を与えた時に、集合a 上の List a を作ると、それは Monoid になります。この a → List a の写像を F(a) とします。
F = list a
list a は、単なる List ではなく、Agda の Monoid record でなければなりません。
F は Free と覚えることもできます。集合の要素を自由に組み合わせてできる Monoid なわけです。この文字列を自由に組み合わせた List を Kleene closure と言います。Free monoid とも呼ばれます。数学で Free と付いていると、基底から自由に組み合わせてできるものを指すようです。
A を Sets 、B を Monoid を対象とする圏だとします。 Monoid を圏して見るのではなく、Monoid 全部を集めて 作る圏です。U を Monoid b から の射の集合 (Carrier b) を得る関手だとします。U を Underlying と覚えることもできます。代数から代数構造を忘れるので忘却関手とも呼ばれます。
a から生成された List a のCarrier から基底を選び出す写像があるとします。これをη(a)とします。任意の η が普遍問題の解を導くわけではなく、特定のηとUとFの組み合わせにより解を作ります。
ここでは、
η(a) = λ (x : a ) → [x]
つまり、要素一つの List a を返す写像です。自然変換である必要ありませんが、後で、自然変換になることを示します。
ある集合 a から、ある Monoid b の Carrier への写像 f があると、集合 a から作った List a から Monoid b への準同型写像 (射を保存する写像 )が基底η(a)に対して唯一存在します。これがUniversal mapping の解 f* です。
f* : [a,b,c,d,e] → f(a) ∙ f(b) ∙ f(c) ∙ f(d) ∙ f(e)
さらに、
(f*)[a] = f(a)
となります。
つまり、 任意の集合 a から Monoid b の Carrier への射 f に対して、
f = U(f*)η(a)
となる唯一の f * : F(a) → b を与えるようなFree Monoid F(a) と、その基底 η(a) の組があるというわけです。
U(f*) は、Sets の射ですから写像です。η(a) は x から要素一つのリスト、[x]への(Setsの射である)写像です。この二つの合成が f (Sets の射) になります。つまり、U(f*) は要素一つのリストから、Monoid の Carrier への射です。つまり、u(f*)η(a) は、集合 a から Monoid b への射で、f の型と同じであることがわかります。
η(a) は恣意的に選ばれている気がしますが、Universal mapping を提供する η, U, F の要素の一つとして定義されています。
Free Monoid の使い方
Free Monooid の Universal mapping は、集合からMonoidへの写像f に関する議論ならば、Free Monoid = List で議論するので十分だということを示しています。これは、List が Monoid の Model だと考えても良いということです。Monoid の性質、
identity : [] ++ x = x
x ++ [] = x
assoc : a ++ ( b ++ c ) = ( a ++ b ) ++ c
は、List て考えて構いません。Monoid の射 (Carrier ) は、基本的な射 (a や b) か、その合成であるわけです。これは Monoid に対して極めて具体的なイメージを提供します。
Monoids の Monoid 同士の射である homomorphism は、
基本要素の射 : a → f(a)
単位元 : [] → f([]) = ε
と、その合成、
f(a) ○ f(b) ○ f(c) ○ f(d) ○ f(e)
からなると考えると、
*f : [] = f([]) = ε
*f : a ++ b = f(a) ○ f (b)
が具体的な形で見えてきます。実際、これが Universal mapping の性質です。
Agda で Free Monoid を書く
List と、その結合は、もう既に書きました。
infixr 40 _::_
data List (A : Set c ) : Set c where
[] : List A
_::_ : A → List A → List A
infixl 30 _++_
_++_ : {A : Set c } → List A → List A → List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
問題は、書かなければならないのは Monoid ではなくて、Monoid を対象にする圏 Monoids だということです。Underline Functor U によって、 Monoids は Sets に写像されます。
まず、Monoid を定義します。T = M x A で使ったものをここでも使います。Monoid は Algbra にあります。
open import Algebra.FunctionProperties using (Op₁; Op₂)
open import Algebra.Structures
open import Data.Product
record ≡-Monoid : Set (suc c) where
infixl 7 _∙_
field
Carrier : Set c
_∙_ : Op₂ Carrier
ε : Carrier
isMonoid : IsMonoid _≡_ _∙_ ε
open ≡-Monoid
_≡_ が使えるので Sets と相性が良いのが特徴です。isMnoid には単位元と結合則が入っています。Monoid の射は Carrier と呼ばれます。
これが Monoids の Obj 対象です。そして、射になるのは、Monoid 間の準同型写像 (Homomoriphism)です。Functor と同様、単位元を保存し、分配則が成立します。moprh 自体は普通の写像です。これも Sets と相性がよろしい。
record Monomorph ( a b : ≡-Monoid ) : Set (suc c) where
field
morph : Carrier a → Carrier b
identity : morph (ε a) ≡ ε b
homo : ∀{x y} → morph ( _∙_ a x y ) ≡ ( _∙_ b (morph x ) (morph y) )
open Monomorph
Monoid 毎に別な演算 _∙_ があるので、infix はうまく働きません。_∙_ と書けば、普通の関数と同じ扱いになります。単位元と結合則で、二つの法則がちゃんと成立することを証明する必要があります。
_+_ : { a b c : ≡-Monoid } → Monomorph b c → Monomorph a b → Monomorph a c
_+_ {a} {b} {c} f g = record {
morph = λx → morph f ( morph g x ) ;
identity = identity1 ;
homo = homo1
} where
identity1 : morph f ( morph g (ε a) ) ≡ ε c
-- morph f (ε b) = ε c , morph g (ε a) ) ≡ ε b
-- morph f morph g (ε a) ) ≡ morph f (ε b) = ε c
identity1 = trans ( ≡-cong (morph f ) ( identity g ) ) ( identity f )
homo1 : ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ) )
-- ∀{x y} → morph f ( morph g ( _∙_ a x y )) ≡ morph f ( ( _∙_ c (morph g x )) (morph g y) )
-- ∀{x y} → morph f ( ( _∙_ c (morph g x )) (morph g y) ) ≡ ( _∙_ c (morph f (morph g x )) (morph f (morph g y) ))
homo1 = trans (≡-cong (morph f ) ( homo g) ) ( homo f )
M-id : { a : ≡-Monoid } → Monomorph a a
M-id = record { morph = λx → x ; identity = refl ; homo = refl }
Reasoning を使うべきですが、ちょっとさぼっています。困った時には refl です。
等号は morph だけを見ます。record ごと _≡_ で見ると、identity とかも比較するので失敗してしまいます。
_==_ : { a b : ≡-Monoid } → Monomorph a b → Monomorph a b → Set c
_==_ f g = morph f ≡ morph g
あとは、これらを使って圏 Monoids を作るだけです。
isMonoids : IsCategory ≡-Monoid Monomorph _==_ _+_ (M-id)
isMonoids = record { isEquivalence = isEquivalence1
; identityL = refl
; identityR = refl
; associative = refl
; o-resp-≈ = λ{a} {b} {c} {f} {g} {h} {i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
}
where
o-resp-≈ : {a b c : ≡-Monoid } {f g : Monomorph a b } → {h i : Monomorph b c } →
f == g → h == i → (h + f) == (i + g)
o-resp-≈ {A} refl refl = refl
isEquivalence1 : { a b : ≡-Monoid } → IsEquivalence {_} {_} {Monomorph a b} _==_
isEquivalence1 = -- this is the same function as A's equivalence but has different types
record { refl = refl
; sym = sym
; trans = trans
}
Monoids : Category _ _ _
Monoids =
record { Obj = ≡-Monoid
; Hom = Monomorph
; _o_ = _+_
; _≈_ = _==_
; Id = M-id
; isCategory = isMonoids
}
refl だけでできてしまうので簡単です。
Underline Functor と Generator を作る
A = Sets {c}
B = Monoids
としましょう。Underline Functro (Forgetful functor / 忘却関手 ) は、Carrier を取ってくるだけです。Carrier は、そのまま Set
だからです。T = M x A でも、同じ方法を使いました。
open Functor
U : Functor B A
U = record {
FObj = λm → Carrier m ;
FMap = λf → morph f ;
isFunctor = record {
≈-cong = λx → x
; identity = refl
; distr = refl
}
}
忘却関手は射の集合を集合として対象にします。Monoid は対象を一つだけ持ちますが、それではありません。圏では重要なのは射です。忘れているのは、identity や homo の拘束条件です。moroph は、もう単なる写像なので関手の条件もほとんど refl です。≈-cong は等式を受け取って、そのまま返します。
関手 Generator は、list を返すわけですが、それは Monoid でなければなりません。つまり、Monoid の性質を証明する必要があります。Data の List を使っても良いですが、ここでは自分で証明します。
-- FObj
list : (a : Set c) → ≡-Monoid
list a = record {
Carrier = List a
; _∙_ = _++_
; ε = []
; isMonoid = record {
identity = ( ( λx → list-id-l {a} ) , ( λx → list-id-r {a} ) ) ;
isSemigroup = record {
assoc = λx → λy → λz → sym ( list-assoc {a} {x} {y} {z} )
; isEquivalence = list-isEquivalence
; ∙-cong = λx → λy → list-o-resp-≈ y x
}
}
}
record の identity = は、特別な構文であり、引数を付けることはできません。なので、λ式で受けています。Monoid の identity は Prouct で記述されているので、それに合わせます。
≡-cong = Relation.Binary.PropositionalEquality.cong
list-id-l : { A : Set c } → { x : List A } → [] ++ x ≡ x
list-id-l {_} {_} = refl
list-id-r : { A : Set c } → { x : List A } → x ++ [] ≡ x
list-id-r {_} {[]} = refl
list-id-r {A} {x :: xs} = ≡-cong ( λy → x :: y ) ( list-id-r {A} {xs} )
list-assoc : {A : Set c} → { xs ys zs : List A } →
( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
list-assoc {_} {[]} {_} {_} = refl
list-assoc {A} {x :: xs} {ys} {zs} = ≡-cong ( λy → x :: y )
( list-assoc {A} {xs} {ys} {zs} )
list-o-resp-≈ : {A : Set c} → {f g : List A } → {h i : List A } →
f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
list-o-resp-≈ {A} refl refl = refl
list-isEquivalence : {A : Set c} → IsEquivalence {_} {_} {List A } _≡_
list-isEquivalence {A} = -- this is the same function as A's equivalence but has different types
record { refl = refl
; sym = sym
; trans = trans
}
cong の名前が重なっているので、別に用意しています。これも、既に証明したものですが、Monoid に合わせる必要があります。
Generator : Obj A → Obj B
Generator s = list s
これが Generator です。関手には、まだなってません。Universal mapping の解と合わせて関手を構成します。
解の構成
解は基本的に、List を分解して、一つ一つ f で写像して、Monoid として合成するだけです。
open UniversalMapping
Φ : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → List a → Carrier b
Φ {a} {b} {f} [] = ε b
Φ {a} {b} {f} ( x :: xs ) = _∙_ b ( f x ) (Φ {a} {b} {f} xs )
これが *f [a,b,c] = f(a) ∙ f(b) ∙ f(c) そのものです。よく使うので抜き出してあります。 *f [] = εも、ここで定義されています。
あとは、これから Monoids の射 homo を構成すれば良いわけです。solution は新しく作られる Monoids の射ですから、identity と homo を証明する必要があります。
solution : (a : Obj A ) (b : Obj B) ( f : Hom A a (FObj U b) ) → Hom B (Generator a ) b
solution a b f = record {
morph = λ(l : List a) → Φ l ;
identity = refl ;
homo = λ{x y} → homo1 x y
} where
_*_ : Carrier b → Carrier b → Carrier b
_*_ f g = _∙_ b f g
homo1 : (x y : Carrier (Generator a)) → Φ ((Generator a ∙ x) y) ≡ (b ∙ Φ x) (Φ y)
homo1 [] y = sym (proj₁ ( IsMonoid.identity ( isMonoid b) ) (Φ y))
homo1 (x :: xs) y = let open ≡-Reasoning in
sym ( begin
(Φ {a} {b} {f} (x :: xs)) * (Φ {a} {b} {f} y)
≡⟨⟩
((f x) * (Φ {a} {b} {f} xs)) * (Φ {a} {b} {f} y)
≡⟨ ( IsMonoid.assoc ( isMonoid b )) _ _ _ ⟩
(f x) * ( (Φ {a} {b} {f} xs) * (Φ {a} {b} {f} y) )
≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
(f x) * ( Φ {a} {b} {f} ( xs ++ y ) )
≡⟨⟩
Φ {a} {b} {f} ( x :: ( xs ++ y ) )
≡⟨⟩
Φ {a} {b} {f} ( (x :: xs) ++ y )
≡⟨⟩
Φ {a} {b} {f} ((Generator a ∙ x :: xs) y)
∎ )
射 Φ の定義に従って証明します。list と Monoid が混在するので、演算を定義しなおして infix で使っています。++ は Generator a の演算 _∙_ でした。Φの定義の展開は ≡⟨⟩ で自動的に行われます。見やすいように変形しているだけです。
homo1 は、List の constructor ( [], _::_ ) で場合分けして証明します。List の証明の定番です。Monoid の identity は Product であり、さらに引数を取るので、それに合わせて呼び出しています。list-id-r をそのまま呼び出すこともできます。
≡⟨ sym ( (IsMonoid.∙-cong (isMonoid b)) refl (homo1 xs y )) ⟩
で、homo1 を再帰的に呼び出しています。より短い射への証明を呼び出すわけです。「より短い」を Agda が認識できない場合は「黄色」が出て「証明の停止性に問題がある」ことを示します。Agda のλ式では、無限ループは許されないわけです。これは、型の unification で x = f ( x ) が許されないことに対応します。f ( f ( f ( ... ) ) ) = x になってしまうわけです。
f ( [] ) = []
f ( x :: xs ) = f ( xs )
なら大丈夫です。
Φの暗黙の引数は、Reasoing の中では省略できません。さぼると黄色くなってしまいます。
次に (insertion function と呼ばれるらしい) ηを構成します。これは楽勝です。[x] つまり、x :: [] を返すだけです。
eta : (a : Obj A) → Hom A a ( FObj U (Generator a) )
eta a = λ( x : a ) → x :: []
Universal mapping を構成する
これで役者はそろったので、f = U(f*)ηと、その唯一性を証明して、UniversalMapping record を構成します。Sets を扱うので、Functional Extensinality (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) を仮定します。
-- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
-- postulate extensionality : { a b : Obj A } {f g : Hom A a b } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g )
postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta
FreeMonoidUniveralMapping =
record {
_* = λ{a b} → λf → solution a b f ;
isUniversalMapping = record {
universalMapping = λ{a b f} → universalMapping {a} {b} {f} ;
uniquness = λ{a b f g} → uniquness {a} {b} {f} {g}
}
} where
universalMapping : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } → FMap U ( solution a b f ) o eta a ≡ f
universalMapping {a} {b} {f} = let open ≡-Reasoning in
begin
FMap U ( solution a b f ) o eta a
≡⟨⟩
( λ (x : a ) → Φ {a} {b} {f} (eta a x) )
≡⟨⟩
( λ (x : a ) → Φ {a} {b} {f} ( x :: [] ) )
≡⟨⟩
( λ (x : a ) → _∙_ b ( f x ) (Φ {a} {b} {f} [] ) )
≡⟨⟩
( λ (x : a ) → _∙_ b ( f x ) ( ε b ) )
≡⟨ ≡-cong ( λ g → ( ( λ (x : a ) → g x ) )) (extensionality lemma-ext1) ⟩
( λ (x : a ) → f x )
≡⟨⟩
f
∎ where
lemma-ext1 : ∀{ x : a } → _∙_ b ( f x ) ( ε b ) ≡ f x
lemma-ext1 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid b) ) ) (f x)
universalMapping 側は一直線ですが、一箇所、extensionality が必要になります。Sets では射が λ x → f x の形なので避けることは難しいようです。
Uniqueness の方が少し面倒です。
uniquness : {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →
{ g : Hom B (Generator a) b } → (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ]
uniquness {a} {b} {f} {g} eq =
extensionality ( lemma-ext2 ) where
lemma-ext2 : ( ∀{ x : List a } → (morph ( solution a b f)) x ≡ (morph g) x )
-- (morph ( solution a b f)) [] ≡ (morph g) [] )
lemma-ext2 {[]} = let open ≡-Reasoning in
begin
(morph ( solution a b f)) []
≡⟨ identity ( solution a b f) ⟩
ε b
≡⟨ sym ( identity g ) ⟩
(morph g) []
∎
lemma-ext2 {x :: xs} = let open ≡-Reasoning in
begin
(morph ( solution a b f)) ( x :: xs )
≡⟨ homo ( solution a b f) {x :: []} {xs} ⟩
_∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph ( solution a b f)) xs )
≡⟨ ≡-cong ( λ k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 {xs} ) ⟩
_∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph g) ( xs ))
≡⟨ ≡-cong ( λk → ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
begin
( λx → (morph ( solution a b f)) ( x :: [] ) )
≡⟨ extensionality lemma-ext3 ⟩
( λx → (morph g) ( x :: [] ) )
∎
) ⟩
_∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
≡⟨ sym ( homo g ) ⟩
(morph g) ( x :: xs )
∎ where
lemma-ext3 : ∀{ x : a } → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] )
lemma-ext3 {x} = let open ≡-Reasoning in
begin
(morph ( solution a b f)) (x :: [])
≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
f x
≡⟨ sym ( ≡-cong (λf → f x ) eq ) ⟩
(morph g) ( x :: [] )
∎
証明すべき式自体が、 (FMap U g) o (eta a ) ≡ f → B [ solution a b f ≈ g ] ですが、このままだと、手がかりがなさすぎます。でも、
eta a
は確か、
eta a = λ( x : a ) → x :: []
でした。λx はどこに? と言うことは、、 (FMap U g) o (eta a ) ≡ f は本当は、
λx → (FMap U g) o (eta a x ) ≡ λx → f x
B [ solution a b f ≈ g ] も同様に、λy → (solution a b f) ≈ λy → g y 。しかも、y は List a なはずです。
B [ λ(y : List a) → (solution a b f) y ≈ λ(y : List a) → g y ]
だとすれば、extensinality で引数を明示して、List a の定石である [] と _::_ の場合分けを行えば良いわけです。それが、
extensionality ( lemma-ext2 ) where
lemma-ext2 : ( ∀{ x : List a } → (morph ( solution a b f)) x ≡ (morph g) x )
です。 B は Monoids ですから、射の等式は morph を比較すれば良いわけです。[] の case は、
(morph ( solution a b f)) [] ≡⟨ sym ( identity g ) ⟩ (morph g) []
です。これは、以下のように示せます。
lemma-ext2 {[]} = let open ≡-Reasoning in
begin
(morph ( solution a b f)) []
≡⟨ identity ( solution a b f) ⟩
ε b
≡⟨ sym ( identity g ) ⟩
(morph g) []
∎
[] の case は比較的簡単ですが、_::_ はやさしくありません。f* ( a ++ b ) = f(a) ∙ f(b) を示すだけなので、homo で分解して sym homo で元に戻せば良いだけですが... 示すべき式は、
(morph ( solution a b f)) ( x :: xs ) ≡ (morph g) ( x :: xs )
です。 x :: xs は、x ++ xs ではないので、homo で分解すると、[x] ++ xs つまり、_::_ x [] と、xs に分解されます。分解した xs 側は、
≡⟨ ≡-cong ( λ k → (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 {xs} ) ⟩
で再帰的に処理できます。これで問題は、
_∙_ b ((morph ( solution a b f)) ( x :: []) ) ((morph g) ( xs )) ≡ _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
になりました。右辺は、sym homo で、目的の (morph g) ( x :: xs ) になります。あと、もう少しです。
見通しを良くするために、もう一度、 ≡-cong と extensionality を使って、
(morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] )
だけにします。これが、lemma-ext3 です。
lemma-ext3 : ∀{ x : a } → (morph ( solution a b f)) (x :: []) ≡ (morph g) ( x :: [] )
lemma-ext3 {x} = let open ≡-Reasoning in
begin
(morph ( solution a b f)) (x :: [])
≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
f x
≡⟨ sym ( ≡-cong (λf → f x ) eq ) ⟩
(morph g) ( x :: [] )
∎
まず、下の方から逆にたどってみます。 今まで使ってなかった、
(FMap U g) o (eta a ) ≡ f
の仮定は、\x -> (FMap U g) (eta a x) を C-c C-n で正規化すると、 \x -> morph g (x :: []) です。つまり、
\x -> morph g (x :: []) ≡ \x -> f x
です。これを使うと、 (morph g) ( x :: [] ) を f x に直せます。Extensinality の逆( f ≡ g → λx → f x ≡ λx → g x)は自動的に Agda が推論してくれるわけです。
そこで、最初に戻ります。
(morph ( solution a b f)) (x :: [])
は、 λa → λb → λf → λx → (morph ( solution a b f)) (x :: []) を C-c C-n すると、 λ a b f x → (b ∙ f x) (ε b) です。なので、
≡⟨ ( proj₂ ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
として、ε b を消すと、
\ a -> \b -> \f -> f x
になるはずです。これは Agda が解決して f x してくれます。これで uniquness の証明ができました。