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

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)的完全相同的方法，除了用nil2替换nil1，用list1替换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 是最有用（但仍然不是很实用）的实现。