Dependently-typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations satisfied propositionally by a large class of container-like type constructors $F : \operatorname{Type} \to \operatorname{Type}$, equipped with a $\operatorname{map}_{F} : (A \to B) \to F\ A \to F\ B$, such as lists or trees. Promoting these equations to definitional ones strengthen the theory, enabling slicker proofs and more automation for functorial type constructors. This extension is used to modularly justify a structural form of coercive subtyping, propagating subtyping through type formers in a map-like fashion. We show that the resulting notion of coercive subtyping, thanks to the extra definitional equations, is equivalent to a natural and implicit form of subsumptive subtyping. The key result of decidability of type-checking in a dependent type system with functor laws for lists has been entirely mechanized in Coq.

翻译：依赖类型证明助手的关键在于定义性相等，它将底层类型理论中自动等同的类型与项关联起来。本文扩展了类型理论，加入了定义性函子定律——这类等式对一大类容器式类型构造子（如列表或树）$F : \operatorname{Type} \to \operatorname{Type}$（配备$\operatorname{map}_{F} : (A \to B) \to F\ A \to F\ B$）在命题层面成立。将这些等式提升为定义性等式可强化理论，从而为函子类型构造子提供更简洁的证明和更强的自动化能力。该扩展被用于模块化地论证一种结构化的强制子类型，通过类映射方式在类型构造子间传播子类型。我们证明，得益于额外的定义性等式，由此产生的强制子类型概念等价于一种自然且隐式的包含性子类型。关于带列表函子定律的依赖类型系统中类型检查可判定性的关键结果，已在Coq中完全机械化实现。