自分で調べて自分でかけ。coq/ hott 使えば、何も中身の仕組みしらんくてもアホでもできる。

悪いが、機械より上のことは、
そこまで興味ない。