习题 2-4 [type-theory-book/exercise-2-4]