Martin Lof Type Theory

Coq

http://www.cse.chalmers.se/research/group/logic/book/book.pdf

これは後で読むことにする。


3連休はCategory Theoryの読書として、

  • "Category Theory",Steve Awodey
  • "CATEGORIES AND COMPUTER SCIENCE", R.F.C.Walters
  • "Conceptual Mathematics",F.William Lawvere

と飛ばし読みしてきたが、ここで気分を変えて、

  • "An Introduction to Abstract Algebra",Derek J.S. Robinson

に手を出す。
素人だから、まずは雰囲気を楽しむことから。

あと、Groupoidの説明としてこんな文書があるようだ。