如何定义“类型包含”？

不甚理解你描述的“包含关系”，但Coq标准库有定义整数Z：

Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

更多函数支持收录于ZArith库。