Link 集に math in type theory を追加

src/README.md

@@ -6,10 +6,10 @@
 
 ## リンク集
 
-参考にさせていただいたページをここに列挙します．
+* [Mathematics in type Theory 日本語訳](https://lean-ja.github.io/math-in-type-theory-ja/) このリストでは「命題は型，証明はその項」という型理論を基礎として数学を実装する際の事実は既知としています．こういった話に全く馴染みがない方は，まずこちらの記事を読まれると良いと思います．
 
 * [mathlib4-all-tactics](https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md) 全タクティクの網羅的なリスト．
 
-* [数学系のためのLean勉強会](https://github.com/yuma-mizuno/lean-math-workshop) いくつかコード例を拝借させていただきました．
+* [数学系のためのLean勉強会](https://github.com/yuma-mizuno/lean-math-workshop) Lean で数学をどのように実装するのか，実際に実装する過程を追うことで学べる教材です．いくつかコード例を拝借させていただきました．
 
-* [Formalizing Mathematics](https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/Part_C.html) Lean3 による例ですが，よく使うタクティクを平易な解説とともに紹介しているリストです．
+* [Formalizing Mathematics](https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/Part_C.html) Lean3 による例ですが，よく使うタクティクを平易な解説とともに紹介しているリストです．コード例や解説を参考にさせていただきました．