diff --git a/TypeTheoryAndFormalProofCh3Sec1.pdf b/TypeTheoryAndFormalProofCh3Sec1.pdf
new file mode 100644
index 0000000..1bfcb59
Binary files /dev/null and b/TypeTheoryAndFormalProofCh3Sec1.pdf differ
diff --git a/TypeTheoryAndFormalProof第3章.typ b/TypeTheoryAndFormalProofCh3Sec1.typ
similarity index 58%
rename from TypeTheoryAndFormalProof第3章.typ
rename to TypeTheoryAndFormalProofCh3Sec1.typ
index 9c6abc3..608f9d3 100644
--- a/TypeTheoryAndFormalProof第3章.typ
+++ b/TypeTheoryAndFormalProofCh3Sec1.typ
@@ -51,4 +51,15 @@ $arrow.twohead.r_beta lambda x : (\b\o\o\l->\n\a\t) . space x$
 
 第二個範例，就是關於iteration迭代。
 
-設有型別$delta$，和函數$F : delta->delta$，定義$D_(delta,F)$是函數，$lambda x : delta . F(F(x))$。所以$D_(delta,F)$是$F$的第二迭代，也標記為$D circle.stroked.small D$。
\ No newline at end of file
+設有型別$sigma$，和函數$F : sigma->sigma$，定義$D_(sigma,F)$是函數，$lambda x : sigma . F(F(x))$。所以$D_(sigma,F)$是$F$的第二迭代，也標記為$D circle.stroked.small D$。我們如何讓$sigma$不是指單一個型別，而是任意型別的代稱呢？我們又可以用什麼方法讓$F$可以是任意函數呢？我們可以用下列表示方式：
+
+$D equiv lambda alpha : ast . lambda f : alpha->alpha . space lambda x : a f(f x)$，$D$叫做多型polymorphic函數，第一個抽象abstration是二階second-order的。因此這樣：
+
+$D space \n\a\t arrow.twohead.r_(beta) lambda f : \n\a\t -> \n\a\t space . lambda x : \n\a\t space f(f x)$其中 $lambda x . f(f x)$即$f circle.stroked.small f$
+
+另外$D space \n\a\t  space \s arrow.twohead.r_(beta) lambda s. space s(s x)$這是函數將自然數$x$轉成$s (s x)$，亦即「```function(x){x+2}```」。至於表示函數合成的$x space circle.stroked.small space y$要如何表示？
+
+我們可以用下列表示方式：
+$circle.stroked.small equiv lambda alpha:ast. lambda beta : ast. lambda gamma : ast .lambda f : alpha -> beta . lambda g : beta -> gamma . lambda x. g (f x)$
+
+因此$circle.stroked.small space  A space B space C space F space G $可以beta-reduction，轉為$G circle.stroked.small F$，即$lambda x : A . G(F(x))$。
diff --git a/TypeTheoryAndFormalProof第3章.pdf b/TypeTheoryAndFormalProof第3章.pdf
deleted file mode 100644
index a380b76..0000000
Binary files a/TypeTheoryAndFormalProof第3章.pdf and /dev/null differ