diff --git a/TypeTheoryAndFormalProof第3章.pdf b/TypeTheoryAndFormalProof第3章.pdf
index e5a2ecd..a380b76 100644
Binary files a/TypeTheoryAndFormalProof第3章.pdf and b/TypeTheoryAndFormalProof第3章.pdf differ
diff --git a/TypeTheoryAndFormalProof第3章.typ b/TypeTheoryAndFormalProof第3章.typ
index 3fcfde4..9c6abc3 100644
--- a/TypeTheoryAndFormalProof第3章.typ
+++ b/TypeTheoryAndFormalProof第3章.typ
@@ -47,4 +47,8 @@ $(lambda alpha : ast . lambda x : alpha . x ) (\b\o\o\l->\n\a\t) $
 
 $arrow.twohead.r_beta lambda x : (\b\o\o\l->\n\a\t) . space x$
 
-然而我們需要$beta$-reduction
\ No newline at end of file
+然而我們需要$beta$-reduction，之後介紹。
+
+第二個範例，就是關於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