Inductive type :=
  | ty_func : type → type → type

  | ty_unit : type
  | ty_nat : type

  | ty_prod : type → type → type
  | ty_sum : type → type → type.

Definition ty_bool := ty_sum ty_unit ty_unit.