--- a/tex/agda.tex	Wed Sep 09 22:07:32 2020 +0900
+++ b/tex/agda.tex	Fri Sep 11 02:30:15 2020 +0900
@@ -1,2 +1,17 @@
-\section{agda}
-    agdaとは、Agda は依存型をもつ純粋関数型の言語である。 定理証明支援器でもある。
+\section{Agda}
+Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
+ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
+Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
+は記述したプログラムを証明することができる。
+
+%\subsection{Record 型}
+
+%\subsection{Data 型}
+
+%\subsection{Agdaの基本操作}
+
+%\subsection{定理証明支援器としての Agda}
+
+%\subsectoin{}
+
+