--- a/agda-prog.ind	Mon Dec 02 18:30:16 2013 +0900
+++ b/agda-prog.ind	Tue Dec 03 17:17:57 2013 +0900
@@ -308,7 +308,7 @@
 a == a というデータ構造を返す。これは、a == a の証明に対応するλ式でもあって、Curry Haward 対応に
 相当する。
 
-これは、実際には、Relation.Binary.PropositionalEquality で定義されているので、自分で定義する必要はない。
+これは、実際には、Relation.Binary.PropositionalEquality で _≡_  として定義されているので、自分で定義する必要はない。
 
 data 型の他に record 型あり、この append の例題では使わないが、排他的和を表すデータ構造を提供し、圏や関手を定義することができる。
 
@@ -495,77 +495,360 @@
 
 Agda の module には引数があり、暗黙の引数も使うことができる。
 
----数式変形用に ? を使う
+% 数式変形用に ? を使う (この例ではうまく動かない)
+
+--record の使い方
+
+data は constructor を提供するが、record は数学的構造の存在を示す。以下は\cite{} による圏の定義である。
 
-証明の例 (Append の結合)
+    record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁)
+                      (Hom : Obj → Obj → Set c₂)
+                      (_≈_ : {A B : Obj} → Rel (Hom A B) ℓ)
+                      (_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C)
+                      (Id  : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+      field
+        isEquivalence : {A B : Obj} → IsEquivalence {c₂} {ℓ} {Hom A B} _≈_
+        identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f
+        identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f
+        o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} → f ≈ g → h ≈ i → (h o f) ≈ (i o g)
+        associative : {A B C D : Obj} {f : Hom C D}  {g : Hom B C} {h : Hom A B}
+                                      → (f o (g o h)) ≈ ((f o g) o h)
 
-record の使い方
+ここでは、圏の要素がコンストラクタ IsCategory に列挙されている。そして、圏が満たす性質(公理)が field に列挙
+されている。
+
+field は data 型と異なり、要素へアクセスするアクセサを提供している。
+なので、record field は、パターンには使えない。圏を作るときには、アクセサをすべて定義する必要がある。
+つまり、圏であることを示すには公理をすべて満たすことを示す必要がある。例えば、
 
-数学的構造の存在を示す
+    isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id
+    isKleisliCategory  = record  { isEquivalence =  isEquivalence
+                    ; identityL =   KidL
+                    ; identityR =   KidR
+                    ; o-resp-≈ =    Ko-resp
+                    ; associative = Kassoc
+                    }
+
+のように record の中で filed を全部定義する。(KidL などは、別に定義されているとする)
+
+record を入力に使うと、filed は、すべて仮定される。
+つまり、filed に記述した性質を持つ数学的存在を仮定することになる。なので、record は、数学的存在を記述するのに向いている。
 
-record での変数の位置の選択
+ここで、Hom は圏の arrow であり、対象を二つ引数とし何かの集合を返す関数として定義されている。_≈_ は、arrow の等号だが、data 型としては
+定義されていなくて、Rel (Hom A B) ℓ)　となっている。これは、Relation.Binary.Core に定義されていて、
+
+    Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+    Rel A ℓ =  A → A → Set ℓ
 
-これから証明する部分の扱い
+となっている。つまり arrow と同じように集合で定義されている。ここでは Aという型を持つ引数を二つ持ち、何かの 集合を返す関数である。
+このせいで、arrow には _≡_ を使うことができない。
+合同性 ( 同じものに同じ関数を作用させても同じ ) は、 _≡_  を仮定しているので、この圏の定義では、合同性を
+自由に使うことはできない。もし、arrow が Set であれば、あるいは、_≈_  → _≡_   を仮定すれば、 _≡_  を使うことができる。
+
+--record での変数の位置の選択
+
+record 型を入力で使う場合は、
+record の引数は、record で定義される数学的構造を定義した時に決まっている必要がある。
+field に書かるのは関数か関数で表された式になるが、これは、record が勝手に提示するものになり、
+外から指定することはできない。
 
-eval の使い方
+逆に record を値として定義する時には、record の引数は指定できず、field の値のみを指定できる。
+record の引数は field の中の式の型から決まる。
+
+関手を record で定義する時に、二つの射(対象の写像FObjと射の写像FMap)は field として定義する。
+record IsFunctor では関手の入力と出力に対応する二つの圏は record の引数になっている。
+一方で、record Functor では関手の入力と出力に対応する二つの圏は record のfieldになっている。
+このように二段階で数学的構造を定義すると、値としての fieldと、公理としての field を分離することができる。
 
-Agda では証明できないもの
+値は、入力となるrecord の引数に記述すると「すべての、その型の値に対してrecordが存在する」という意味になり、
+入力となるrecord の field に記述すると、 「record は、その型の値を生成する」になる。なので、どちらに記述するかの
+差は大きい。
+
+    record IsFunctor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁′ c₂′ ℓ′)
+                     (FObj : Obj C → Obj D)
+                     (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B))
+                     : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+      field
+        ≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ]
+        identity : {A : Obj C} →  D [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {D} (FObj A)) ]
+        distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
+          → D [ FMap (C [ g o f ]) ≈ (D [ FMap g o FMap f ] )]
 
-外延性
+    record Functor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′)
+      : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+      field
+        FObj : Obj domain → Obj codomain
+        FMap : {A B : Obj domain} → Hom domain A B → Hom codomain (FObj A) (FObj B)
+        isFunctor : IsFunctor domain codomain FObj FMap
+
+-- Agda では証明できないもの
 
-合同性
+一連の証明で、まだ証明できない部分は、postulate を使って仮定してしまうという方法がある。また、
+証明できてない部分を入力に明示的に記述しても良い。? で放置すると、そこの部分がいつも表示される
+欠点がある。
+
+逆に、Agda が証明が終わったと表示(何もエラーを表示しない)としても、これらの証明されてない
+部分が残っていることがある。
+
+Agad は直観主義論理であり、証明できない式がいくつかあるが、それらは仮定しても構わない。
+そのような命題の一つは、 以下の関数外延性である。
 
-a=b は証明できない。
+ Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} 
+     → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )             
+
+つまり、全ての値について等しいからと言って、その関数自体が(_≡_ の意味で)等しいということを
+証明することはできない。これは、仮定する必要がある。関数が仮定ではなく実際に構成されている
+ものならば、この仮定は必要ない。
+
+この式は、Agda のライブラリに記述されていて、必要ならばそれを postulate すれば良い。
 
-赤を解決する(型の矛盾)
+Rel で定義された等式から、_≡_ を導くこともできない。もし、圏の射が集合ならば
+射の等式は _≡_ で定義されるべきなので、以下を仮定しても良い、あるいはする必要がある。
+
+    postulate ≈-≡ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  
+      {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+
+米田レンマは射が集合であることを要求するので、明示的に集合全体の圏に対して証明するか、
+任意の圏に対して、これと関数外延性を仮定して証明する必要がある。
+
+また、集合以外の関係に対する合同性も単独では証明できない。例えば、関手の合同性は、自明には成り立たない
+ので、以下のように IsFunctor の公理とする必要がある。
 
-黄を解決する(十分限定されていない変数)
+        ≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ]
+
+また、
+   a b  : Set 
+の場合に、a ≡ b は証明できない。 _≡_ は、初めから同じもの( x  ≡  x )に対して生成できるので、最初から
+異なる可能性のあるものには成立しない。合同性の逆、写像した先で等しければ、元も等しいは、例えば以下の米田関手の
+Full embededing は、
+
+    FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
 
-暗黙の変数を明示する
+この形で証明することはできない。逆写像を実際に構築することによってしか証明できない。
+
+--Agda でのデバッグ
+
+Agda は実行することが目的の言語ではないので、デバッグはコンパイル時エラーに対してのみ行う。主なエラーは三種類である。
+
+最初は構文エラーである。Agda は、ほとんどの場合、語の区切りに空白を要求する。特に -> や =  : の両側に空白を要求する。
+例外は () と {} のみである。空白がないと一つの語だと解釈される。x=y は x=y という一つの変数である。これは、式を
+変数に格納する時には読みやすい。また、さまざまなUnicodeの記号を自由に使えるという利点がある。しかし、実際には、
+構文エラーの大半は空白の入れ忘れである。
 
-再利用性
+もう一つのエラーは型の不整合である。これは、Emacs 上で赤で表示される。不整合の部分を ?に置き換えれば、そこにあるべき
+ものの型が示されるので、それを入れれば良い。これは比較的簡単に解決されるエラーである。
+
+最後は、変数が十分に代入されてない場合のエラーである。record の field が定義されてないのに、そこへの参照が必要な場合
+などに、その部分が黄色で表示される。これは、record の深い部分で起こることもあり、解決が難しい。
+
+この場合に、まずすることは「 暗黙の変数を明示」である。これにより解決することがある。関数の呼び出し時に、
+{a}  などとして指定する。
 
-module parameter と、lemma の入力
+同じものを繰り返し記述することは、普通のプログラムでも変更を複数の場所で行うことになるので望ましくない。
+Agda でも同じことが言える。そのために Agda には module がある。
+
+module には parameter があり、それを module 中で暗黙の入力として使うことができる。一方で、証明するべきに式に
+明示的あるいは暗黙の引数として記述しても良い。どちらにするかは、 Agda の Monomorphism から来る問題がある。
 
-Mono morphism から来る問題
+Agda は一つのファイルの中で、異なる型の持つ関数は異なる名前である必要がある。型が異なる同じ名前の関数を
+作ることはできない。これは、module を異なる型で複数回呼び出すことができないということを意味する。
+module parameter ではなく、個々の式の入力すれば、module を複数回呼び出す必要はなくなる。
+
+暗黙の変数は便利であるが、増やすと Agda のメモリを消費し、証明のチェックが遅くなる。その場合は、明示的な変数に
+変えるとなおる場合がある。
 
 --圏論の例
 
-圏の定義
+ここまでで、 圏の定義と 関手の定義を使ってきた。 自然変換の定義は、以下のようになる。
+
+
+--        F(f)                                                                                                                                
+--   F(a) ---→ F(b)                                                                                                                           
+--    |          |                                                                                                                            
+--    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)                                                                                                 
+--    |          |                                                                                                                            
+--    v          v                                                                                                                            
+--   G(a) ---→ G(b)                                                                                                                           
+--        G(f)                                                                                                                                
+
+    record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
+                     ( F G : Functor D C )
+                     (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
+                     : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+      field
+        commute : {a b : Obj D} {f : Hom D a b}
+          → C [ C [ (  FMap G f ) o  ( TMap a ) ]  ≈ C [ (TMap b ) o  (FMap F f)  ] ]
+
+    record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′)
+         (F G : Functor domain codomain )
+           : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+      field
+        TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
+        isNTrans : IsNTrans domain codomain F G TMap
 
-関手の定義
+今までと同じように二つにわけて定義している。
+
+これを使って、 Monad の結合性の証明を以下のように行うことができる。まず Monad を定義する。
+
+        record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+                         ( T : Functor A A )
+                         ( η : NTrans A A identityFunctor T )
+                         ( μ : NTrans A A (T ○ T) T)
+                         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+           field
+              assoc  : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
+              unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+              unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+
+        record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
+               : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+          field
+            isMonad : IsMonad A T η μ
+             -- g ○ f = μ(c) T(g) f                                                                                                           
+          join : { a b : Obj A } → { c : Obj A } →
+                              ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
+          join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
+
+証明するべき式は、
+
+               join M h (join M g f)  ≈ join M ( join M h g) f 
+
+である。この証明は以下のようになる。
 
-自然変換の定義
+    -- h ○ (g ○ f) = (h ○ g) ○ f                                                                                                                  
+    Lemma9 : { a b c d : Obj A }
+                     ( h : Hom A c ( FObj T d) )
+                     ( g : Hom A b ( FObj T c) )
+                     ( f : Hom A a ( FObj T b) )
+                          → A  [ join M h (join M g f)  ≈ join M ( join M h g) f ]
+    Lemma9 {a} {b} {c} {d} h g f =
+      begin
+         join M h (join M g f)
+       ≈⟨⟩
+         join M h (                  ( TMap μ c o ( FMap T g o f ) ) )
+       ≈⟨⟩
+         ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
+       ≈⟨ cdr ( cdr ( assoc )) ⟩
+         ( TMap μ d  o ( FMap T h o ( ( TMap μ c o  FMap T g )  o f ) ) )
+       ≈⟨ assoc  ⟩    ---   ( f  o  ( g  o  h ) ) = ( ( f  o  g )  o  h )                                                                         
+         (     ( TMap μ d o  FMap T h ) o  ( (TMap μ c   o  FMap T g )    o f ) )
+       ≈⟨ assoc  ⟩
+         ( ( ( TMap μ d o      FMap T h ) o  (TMap μ c   o  FMap T g ) )  o f )
+       ≈↑⟨ car assoc ⟩
+         ( ( TMap μ d o  ( FMap T h     o   ( TMap μ c   o  FMap T g ) ) ) o f )
+       ≈⟨ car ( cdr (assoc) ) ⟩
+         ( ( TMap μ d o  ( ( FMap T h o       TMap μ c ) o  FMap T g )   ) o f )
+       ≈⟨ car assoc ⟩
+         ( ( ( TMap μ d o  ( FMap T h   o   TMap μ c ) ) o  FMap T g ) o f )
+       ≈⟨ car (car ( cdr ( begin
+               ( FMap T h o TMap μ c )
+           ≈⟨ nat μ ⟩
+               ( TMap μ (FObj T d) o FMap T (FMap T h) )
+            ∎
+       )))  ⟩
+          ( ( ( TMap μ d  o  ( TMap μ ( FObj T d)  o FMap T (  FMap T h ) ) )  o FMap T g )  o f )
+       ≈↑⟨ car assoc ⟩
+         ( ( TMap μ d  o  ( ( TMap μ ( FObj T d)   o FMap T (  FMap T h ) )   o FMap T g ) )   o f )
+       ≈↑⟨ car ( cdr assoc ) ⟩
+         ( ( TMap μ d  o  ( TMap μ ( FObj T d)   o ( FMap T (  FMap T h ) o FMap T g ) ) )   o f )
+       ≈↑⟨ car ( cdr (cdr (distr T ))) ⟩
+         ( ( TMap μ d  o  ( TMap μ ( FObj T d)     o FMap T ( ( FMap T h  o g ) ) ) )   o f )
+       ≈⟨ car assoc ⟩
+         ( ( ( TMap μ d  o  TMap μ ( FObj T d)  )  o FMap T ( ( FMap T h  o g ) ) )    o f )
+       ≈⟨ car ( car (
+          begin
+             ( TMap μ d o TMap μ (FObj T d) )
+          ≈⟨ IsMonad.assoc ( isMonad M) ⟩
+             ( TMap μ d o FMap T (TMap μ d) )
+          ∎
+       )) ⟩
+         ( ( ( TMap μ d  o    FMap T ( TMap μ d) ) o FMap T ( ( FMap T h  o g ) ) )    o f )
+       ≈↑⟨ car assoc ⟩
+         ( ( TMap μ d  o  ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) ) )  o f )
+       ≈↑⟨ assoc ⟩
+         ( TMap μ d  o  ( ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) )  o f ) )
+       ≈↑⟨ cdr ( car (  distr T ))   ⟩
+         ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
+       ≈⟨⟩
+         join M ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
+       ≈⟨⟩
+         join M ( join M h g) f
+      ∎ where open ≈-Reasoning (A)
 
-Monad の結合性の証明
+ここで、assoc は射の合成の結合法則を使って、式を変形していることを示している。
+nat μ は、自然変換μの commute 規則を呼び出している。≈↑⟨⟩　は、逆向きの推論、≈⟨⟩ は正規型同士が
+同じ場合の見かけだけの変換である。 distr T は関手Tの分配法則である。car と cdr は、
+括弧のレベルの深い部分に推論規則を適用することを示す。
+begin/∎  の式変形は入れ子にすることができて、式の特定の部分に対して、着目して変形することできる。
 
+IsMonad.assoc ( isMonad M)  は、Monad の結合則が使われている部分である。
+
+この証明は、もちろん手での証明、清書された証明と同一である。、この
+証明を見ると、Monad の規則にうち、結合則のみを使っていることがわかる。
+自然変換の可換則を一箇所、T の分配則を二箇所で使っていることがわかる。
 
 --Agda の有効性
 
-Haskell の構文との親和性
+Agda は Haskell の構文との親和性があり、Haskell を知っていれば、他の証明支援系よりも学びやすいと思われる。
 
-証明の完成度がわかる
+本や自分の証明と異なり、証明の完成度がわかる。逆に、ほとんどすべてを証明しないと証明が完結しない。
+
+推論規則や式を見ることができるので、証明の対称性を視認できる。特に式変形を使うことより、証明の対称性を
+可視化できる。
 
-証明の対称性を視認できる
+? による単一化 により証明を見つけることができる。しかし、Agda は自動化する方法がほとんど存在しないので、
+すべて人手で証明する必要がある。
 
-Unification により証明を見つけることができる
+Monomoprhism があり、勝手な記号を導入することが広く行われている。さらに、record 定義や module 定義に
+任意性があり、 証明は極めて個人的なものになる。module をそのまま使う以外に証明を共有することは難しい。
+式変形ではなく、λ式により直接証明を記述する場合は、Coq と同様に視認性の低い証明になってしまう。
 
-すべて人手
+Agda は特に圏論の証明に向いており、 Monad や Kan extension を「証明として」理解するためには有効であると
+思われる。しかし、証明を理解することは数学的に理解することとは異なる。実際、モデルを理解することとの
+差がある。圏論の場合は、モデルはグラフであり、モデル的に理解することと証明から理解することのギャップは
+小さい。
 
-式変形を明示できる
+例えば、自然変換の可換性は、純粋に記号的な可換性であり、そのパターンを理解することが自然変換を理解することになる。
 
-証明は極めて個人的
+自分で Agda で証明を構築することは、一種のパズル、あるいは詰将棋のようなものであり、それ自体が知的遊戯として
+すぐれている。これは、省略されている数学書を補う仕組みになっている。実際、Agda のようなツール抜きでも、
+数式を手書きするなどの方法で、それを補うことをしなければ、数学を理解することはできない。Agda は、その際に
+起きるエラーを指摘してくれるので、未熟な理解を防ぐことができる。
 
-勝手な記号
+証明の対称性と、パターンは、それ自体が数学的証明の技術であり、Agda を使うことにより、その技術を身につけられる
+ことが大きい。自然変換の可換性を可換図で記述することは広く使われているが、Agda で記述すると、それは、
+関手と自然変換の式のパターンとなる。
 
-勝手なrecord
+Monad を理解するのに、join の結合性を理解することが必須かというと、そのようなことはない。むしろ、それが
+重要であることを主張している解説は少ない。しかし、
 
-勝手な module parameter
+   T が関手(データ構造)
+   return が自然変換η (プログラム)
+   join が自然変換μ (プログラム)
 
-理論の理解に使う Monad とか Kan extension とか
+という対応を理解しなければ、Monad を使う理由を理解できない。実際、Monad は対象レベルとメタレベルの
+双対性(随伴関手)が反映されたものになっている。
+
 
 --今後の展開
 
-プログラミングと証明を同時に行う
+Agda は、Emacs に密接に結びついた会話的な証明支援系だが、実際のプログラミングに比べると、一行当たりにかかる
+時間が十倍以上ある。1日にかける行数は100行が限界に近い。難しい部分では一行に数日かかることもある。
+
+圏論を理解するのに Agda が有効であることはわかったが、これを実用的な(例えば)Haskellのプログラムに
+応用するには、人間的、あるいは計算環境的なギャップがある。
+
+例えば、Monad は、その組み合わせを Monad にすることが難しいことが知られている。Monad の組み合わせ自体は、
+Haskell で作れるが、組み合わせた join が、元の join と、どう関係あるかを示すのは難しい。それを示すには
+Agda などのシステムが役に立つかもれない。
+
+今後は、さらに Agda での圏論の理解を深めると共に、実用的なプログラムの信頼性を高めるのに Agda (あるいは、
+これに類似したシステム)が使えるかどうかを調べていく予定である。
 
 
+
+
+
+
+
+