定義，命題，証明

アイデアとは対照的に，数学の他の部分（定義，定理/予想, 証明）は基礎的なシステムで形式化することができ，したがって精確な方法でコンピュータ上に作成・保存することができます．これは pdf ファイルのことではありません！pdf ファイルこそ，私が脱却したいものなのです！つまり，様々ある数学の基礎付け（集合論，型理論，圏論）のうち1つを理解するコンピュータプログラミング言語が設計されており，その言語で数学者が問題の定義，命題，証明を書くことができるということです．

私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や $\pi$ の定義は集合です．そして証明とは，論理のステップをつなげたものです．集合論において，定義と証明は全く異なるもののように私には思えます．群とは，定義と証明の混合物です．―― 群とは，順序付き4つ組 $(G,m,i,e)$ であって，特定の公理を満たすもののことです．つまり，論理が付属した集合です．

しかし，型理論では驚くほど違います．今挙げた３つのもの ―― 定義，命題，証明 ―― はすべて同じ種類のものです！これらはすべて項です．群，証明，実数 ―― これらもすべて項です．定義と証明の統一，つまり集合と論理の統一が，型理論を実用的な基礎システムたらしめ，コンピュータに学部レベルのすべての数学を教えることを可能にしています．