关于形式化类型论中归纳定义与推理规则的关系及归纳类型本质的疑问

我一直对形式化类型论里的这一点最摸不透——就拿*同伦类型论（HoTT）*来说吧，书里随处可见各种（高阶或非高阶的）归纳定义，比如列表、商集、实数这些，但到了末尾的形式化部分，真正给出推理规则的却寥寥无几：积类型、余积类型、空类型、单位类型、自然数类型还有恒等类型。在自然数类型的定义下面，他们只提了一句“其他归纳定义都遵循同样的通用模式”，这让我忍不住觉得：每次在类型论里给出一个归纳定义，就意味着要新增一套对应的推理规则。

在我看来，这跟集合论比起来既不实用又有点“别扭”——集合论里只有固定数量的逻辑推理规则和公理，直接组合这些规则和公理就能定义出复杂的构造。

是不是我完全误解了归纳类型的本质？我能想到，在类型论的某个具体模型里，或许可以证明某些类别的归纳类型是存在的，但我还没在直接的形式化体系里见过类似的内容，也脑补不出它会是什么样子。

备注：内容来源于stack exchange，提问作者kongus_bongus