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

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作为参数的函数都可以扩展为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或笛卡儿)是目前唯一有效的设置.cubicaltt是最实用的(但仍然不是很实用)实现.