--- a/paper/agda.tex	Tue Jan 31 11:57:12 2017 +0900
+++ b/paper/agda.tex	Tue Jan 31 16:41:36 2017 +0900
@@ -281,7 +281,7 @@
 型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
 Agda は依存型という強力な型システムを持っている。
 依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
-この節では Agda の文法的な紹介を行なう。 % ref pdf のアレ
+この節では Agda の文法的な紹介を行なう~\cite{agda-documentation}。 % ref pdf のアレ
 
 まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
 トップレベルのモジュールはファイル名と同一となる。
@@ -342,6 +342,78 @@
 
 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
 
+次に依存型について見ていく。
+依存型で最も基本的なものは関数型である。
+依存型を利用した関数は引数の型に依存して返す型を決定できる。
+
+Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
+ここで B の中で x を扱っても良い。
+例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。
+
+\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
+
+この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
+実際に Nat へ適用した例が \verb/id-zero/ である。
+
+依存型を用いることで任意の型に適用可能な多相の恒等関数を定義した。
+しかし型を明示的に指定せずとも \verb/zero/ を渡された場合は恒等関数の型は自明に \verb/Nat -> Nat/である。
+その場合、型を推論することで実際に引数として渡さないようにできる。
+これを暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。
+
+例えば恒等関数の型を暗黙的な引数にするとリスト~\ref{src:agda-implicit-id}のようになる。
+この恒等関数を利用する際は値を渡すだけで型が自動的に推論される。
+よって関数を利用する際は \verb/id-true/ のように記述できる。
+なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる。
+
+\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
+
+Agda にはレコード型も存在する。
+定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
+例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
+レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
+複数の値を列挙する際は \verb/;/ で区切る。
+
+\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
+
+構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
+なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
+また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。
+Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。
+
+\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
+
+Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
+とあるデータ型が、ある型と名前を持つ関数を持つことを保証する。
+これは Haskell における型クラスや Java におけるインターフェースに相当する。
+Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
+例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
+具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。
+
+\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}
+
+ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
+型Nat が Eq の上位型であることを記述するとリスト~\ref{src-agda-instance}のようになる。
+
+\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}
+
+これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
+例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
+部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。
+なお、名前部分は必須である。
+仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。
+部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。
+
+\lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced}
+
+この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。
+Nat型の要素を持つリストの内部に4が含まれるか確認している。
+この \verb/listHas4/ は \verb/true/ に評価される。
+なお、 \verb/--/ の後はコメントである。
+
+\lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced}
+
+
+% TODO: 必要なら with の解説
 
 \section{Reasoning}
 

--- a/paper/atton-master.tex	Tue Jan 31 11:57:12 2017 +0900
+++ b/paper/atton-master.tex	Tue Jan 31 16:41:36 2017 +0900
@@ -25,6 +25,7 @@
 \usepackage{bussproofs}
 \usepackage{amssymb}
 \usepackage{amsmath}
+\usepackage{colonequals}
 \usepackage[utf8]{inputenc}
 
 %\input{dummy.tex} %% font

--- a/paper/escape_agda.rb	Tue Jan 31 11:57:12 2017 +0900
+++ b/paper/escape_agda.rb	Tue Jan 31 16:41:36 2017 +0900
@@ -6,6 +6,7 @@
 
 ReplaceTable = {
   '->' => 'rightarrow',
+  '∷' => 'text{::}',
   '∙'  => 'circ',
   '≡' => 'equiv',
   '×' => 'times',

--- a/paper/reference.bib	Tue Jan 31 11:57:12 2017 +0900
+++ b/paper/reference.bib	Tue Jan 31 16:41:36 2017 +0900
@@ -91,6 +91,14 @@
     note = {Accessed: 2016/01/20(Fri)}
 }
 
+@misc{agda-documentation,
+    title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation},
+    howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}},
+    note = {Accessed: 2016/01/31(Tue)}
+}
+
+
+
 @misc{coq,
     title = {Welcome! | The Coq Proof Assistant},
     howpublished = {\url{https://coq.inria.fr/}},

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaElem.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,3 @@
+elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
+elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs)
+elem         x []        = false

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaElemApply.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,3 @@
+listHas4 : Bool
+listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaId.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,5 @@
+identity : (A : Set) -> A -> A
+identity A x = x
+
+id-zero : Nat
+id-zero = identity Nat zero

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaImplicitId.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,5 @@
+id : {A : Set} -> A -> A
+id x = x
+
+id-true : Bool
+id-true = id true

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaInstance.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,9 @@
+_==Nat_ : Nat -> Nat -> Bool
+zero    ==Nat zero    = true
+(suc n) ==Nat zero    = false
+zero    ==Nat (suc m) = false
+(suc n) ==Nat (suc m) = n ==Nat m
+
+instance
+  natHas== : Eq Nat
+  natHas== = record { _==_ = _==Nat_}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaRecord.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,7 @@
+record Point : Set where
+  field
+    x : Nat
+    y : Nat
+
+makePoint : Nat -> Nat -> Point
+makePoint a b = record { x = a ; y = b }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaRecordProj.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,8 @@
+getX : Point -> Nat
+getX p = Point.get p
+
+getY : Point -> Nat
+getY record { x = a ; y = b} = b
+
+xPlus5 : Point -> Point
+xPlus5 p = record p { x = (Point.x p) + 5}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaTypeClass.agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,3 @@
+record Eq (A : Set) : Set where
+  field
+    _==_ : A -> A -> Bool

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/Eq.Agda	Tue Jan 31 16:41:36 2017 +0900
@@ -0,0 +1,30 @@
+module Eq where
+open import Data.Nat
+open import Data.Bool
+open import Data.List
+
+record Eq (A : Set) : Set where
+  field
+    _==_ : A -> A -> Bool
+
+_==Nat_ : ℕ -> ℕ -> Bool
+zero    ==Nat zero    = true
+(suc n) ==Nat zero    = false
+zero    ==Nat (suc m) = false
+(suc n) ==Nat (suc m) = n ==Nat m
+
+
+instance
+  _ : Eq ℕ
+  _ = record { _==_ = _==Nat_}
+
+_||_ : Bool -> Bool -> Bool
+true  || _ = true
+false || x = x
+
+elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
+elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs)
+elem         x []        = false
+
+listHas4 : Bool
+listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true