依存型 type-theory intrinsicな機能 参考文献 Mathematics and Computation | How to implement dependent type theory I