Скажем, у меня есть два индуктивно определенных типа данных:
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 в качестве параметров.
