# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1487220547 -32400
# Node ID 7903c02fe6868710de60687c65122e67602e6360
# Parent  18f872806bc09dd7d959885c74bbc1342def24b4
Update

diff -r 18f872806bc0 -r 7903c02fe686 paper/agda.tex
--- a/paper/agda.tex	Thu Feb 16 13:39:49 2017 +0900
+++ b/paper/agda.tex	Thu Feb 16 13:49:07 2017 +0900
@@ -457,7 +457,12 @@
 $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
 よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
 これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。
-仮定 A $ \times $ B と仮定 A から A $ \rightarrow $ C を導いている。
+仮定 $ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $  と仮定 A から A $ \rightarrow $ C を導いている。
+
+仮定に相当する変数 p の型は$ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $ であり、p からそれぞれの命題を取り出す操作が \verb/fst/ と \verb/snd/ に相当する。
+\verb/fst p/ の型は $ (\text{A} \rightarrow \text{B}) $ であり、\verb/snd p/ の型は $ (\text{B} \rightarrow \text{C}) $ である。
+もう一つの仮定xの型は A なので、\verb/fst p/ を関数適用することで B が導ける。
+得られた B を \verb/snd p/ に適用することで最終的に C が導ける。
 
 \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced}
 
diff -r 18f872806bc0 -r 7903c02fe686 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed