«Свободные теоремы» в смысле статьи Уодлера «Теоремы бесплатно!» уравнения о некоторых значениях выводятся только на основе их типа. Так что, например,
f : {A : Set} → List A → List A
автоматически удовлетворяет
f . map g = map g . f
Тогда могу ли я получить термин Agda следующего типа:
(f : {A : Set} → List A → List A) {B C : Set} (g : B → C) (xs : List B)
→ f (map g xs) ≡ map g (f xs)
или если да/если нет, могу ли я сделать что-то более/менее общее?
Мне известно о существовании библиотеки облегченных бесплатных теорем но я не думаю, что он делает то, что я хочу (а если и делает, то я не понимаю его достаточно хорошо, чтобы сделать это).
(Пример использования: у меня есть функтор F : Set → Set, и я хотел бы доказать, что полиморфная функция F A × F B → F (A × B) автоматически является естественным преобразованием.)
