types - 是否有一种类型理论可以表示相同形状的归纳数据类型的等效性？

Question

假设我有两种归纳定义的数据类型:

Inductive list1 (A : Type) : Type :=
 | nil1 : list1 A
 | cons1 : A -> list1 A -> list1 A.

和

Inductive list2 (A : Type) : Type :=
 | nil2 : list2 A
 | cons2 : A -> list2 A -> list2 A.

对于任何 P (list1 a)我应该能够构建一个 P (list2 a) ，通过应用我用来构建 P (list1 a) 的完全相同的方法除了更换 nil1与 nil2 , list1与 list2和 cons1与 cons2 .类似地，任何需要 list1 a 的函数作为参数可以扩展为 list2 a .

是否有类型系统允许我以这种方式谈论具有相同形状的两种数据类型(具有相同形状的构造函数)，并证明 P (list1 a) -> P (list2 a) ?例如，这是单价、HOTT 或立方/观察类型系统允许的吗？它还可能允许定义函数，如 reverse: list_like a -> list_like a接受两者 list1 s 和 list2 s 作为参数。

Answer 1

在单价的HoTT中，确实可以证明list1 A等于 list2 A所有 A .给出证明 p : list1 A = list2 A , transport (或 subst )给你 P (list1 A) -> P (list2 A)对于任何 P .在立方类型理论中，这种传输也可以按预期计算。据我所知，立方类型理论( CCHM 或 cartesian )是目前唯一可行的设置。 cubicaltt 是最有用(但仍然不是很实用)的实现。