Параметрические доказательства в Агде

Question

Чтение этого ответа побудило меня попытаться построить, а затем доказать каноническую форму полиморфных контейнерных функций. Конструкция была простой, но доказательство ставит меня в тупик. Ниже приведена упрощенная версия того, как я пытался написать доказательство.

Упрощенная версия доказывает, что достаточно полиморфные функции из-за параметризации не могут изменять свое поведение только в зависимости от выбора параметра. Допустим, у нас есть функции двух аргументов, одного фиксированного типа и одного параметрического:

PolyFun : Set → Set _
PolyFun A = ∀ {X : Set} → A → X → A

собственность, которую я хотел бы доказать:

open import Relation.Binary.PropositionalEquality

parametricity : ∀ {A X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y
parametricity f a x y = {!!}

Можно ли утверждать подобные заявления изнутри Агды?

Answer 1

Нет, в Agda нет принципа параметричности (пока! [1]).

Однако вы можете использовать эти комбинаторы, чтобы построить тип соответствующей свободной теоремы и постулировать ее:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

[1] http://www.cse.chalmers.se/~mouling/share/PresheafModelParametericTT.pdf