是否存在类型理论，其中相同形状的归纳数据类型的等价性是可表示的？

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这样接受list1s和list2s作为参数的函数。

Answer 1

在具有单一性的HoTT中，确实证明list1 A等于所有list2 A的A。鉴于p : list1 A = list2 A证明，运输（或subst）为任何P (list1 A) -> P (list2 A)提供P。在立方体类型的理论中，这种运输也可以按预期计算。据我所知，立方型理论（CCHM或cartesian）是目前唯一有效的设置。 cubicaltt是最实用的（但仍然不是很实用）。