Type theories can be formalized using the intrinsically (hard) or the extrinsically (soft) typed style. In large libraries of type theoretical features, often both styles are present, which can lead to code duplication and integration issues. We define an operator that systematically translates a hard-typed into the corresponding soft-typed formulation. Even though this translation is known in principle, a number of subtleties make it more difficult than naively expected. Importantly, our translation preserves modularity, i.e., it maps structured sets of hard-typed features to correspondingly structured soft-typed ones. We implement our operator in the MMT system and apply it to a library of type-theoretical features.

翻译：类型理论可以使用内在( 硬) 或外部( 软) 打字风格正式化 。 在大型的理论型号库中, 通常两种类型都存在, 这可能导致代码重复和整合问题 。 我们定义一个操作器, 系统地将硬型转换为相应的软型配方 。 尽管这个翻译在原则上是已知的, 但一些微妙之处使得它比天真的预想的要困难得多 。 重要的是, 我们的翻译保存模块化, 也就是说, 它将结构化的硬型特征组合绘制成相应结构的软型号。 我们在 MMT 系统中执行操作器, 并将其应用到类型理论性特征的图书馆 。