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