立方类型论中为何需I→A函数类型而非仅依赖路径类型？

• 表达灵活性的需求
  路径类型Path A x y是绑定了端点的依赖类型，它的元素明确是从x到y的路径；而I→A是无端点约束的普通函数类型，元素是把整个区间I映射到A的任意函数。在复杂构造中，你可能需要先定义一个不受端点限制的区间映射（比如f : I→A），再通过额外的等式约束（f 0 = x、f 1 = y）将其转化为特定端点的路径，这种分步处理比直接用路径绑定构造<i> a i更灵活，尤其适合组合多个区间映射、处理高阶路径的场景。

• 元理论与语法的简洁性
  部分立方类型论的表述会把I→A作为更基础的构造，路径类型Path A x y可以被定义为I→A的子类型（即满足端点约束的函数集合）。这种设计能复用现有函数类型的规则，简化元理论的证明和系统实现——毕竟常规类型论本来就支持函数类型和lambda抽象，不需要为路径类型额外添加一套独立的语法和推理规则。而CCHM论文选择将路径类型作为原始构造，路径绑定<i> a i本质上是封装了区间到A的映射逻辑，因此不需要显式引入I→A。

• 与现有类型论框架的兼容性
  后续论文引入I→A，很大程度是为了和传统依赖类型论（如Coq、Agda的核心系统）对齐。普通lambda构造λi. a i是开发者和研究者熟悉的语法，用I→A来表达区间映射，能降低学习门槛，也更容易将立方类型论的特性集成到现有工具链中。相比之下，路径绑定<i> a i是立方类型论特有的语法，无法直接复用现有工具的函数类型处理逻辑。

关于CCHM论文未出现I→A的原因：
CCHM原始论文的核心是直接以路径类型为基础构建同伦语义，他们的系统通过路径绑定、路径连接、反转等原生操作来处理同伦等价，I→A的功能已经被这些原生路径构造完全覆盖，因此不需要额外引入独立的区间函数类型。后续论文的设计思路更偏向于将立方类型论的特性“嵌入”到传统类型论框架中，所以选择了更贴合现有体系的I→A作为基础构造。

内容的提问来源于stack exchange，提问作者盛安安