粪海狂蛆 [index] 1. Principles of Dependent Type Theory 的笔记 [type-theory-book] 习题 2-3 [type-theory-book/exercise-2-3] 习题 2-4 [type-theory-book/exercise-2-4]