Работая над аксиомами Пеано в Агде, мы столкнулись с проблемой

Question

PA6 : ∀{m n} -> m ≡ n -> n ≡ m

- это аксиома, которую я пытаюсь решить и поддержать, я пытался использовать cong (из базовой библиотеки), но у меня проблемы с конструктором cong

PA6 = cong

никуда меня не приведет, я знаю, что для cong я должен предоставить refl для равенства и типа, но я не уверен, какой тип я должен предоставить. Идеи?

Это для небольшого задания в университете, поэтому я бы предпочел, чтобы кто-то продемонстрировал то, что я пропустил, а не написал точный ответ, но я был бы признателен за любую степень поддержки.

Answer 1

Ваш PA6 говорит, что ≡ является симметричным.

Это можно найти в стандартной библиотеке модуля Relation.Binary.PropositionalEquality.

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

(Этот вопрос довольно старый, но я пишу для будущих читателей, которые наткнулись на него.)

Answer 2

По характеру системы, которую я создал, я должен был понять, что у меня есть две эквивалентности и, следовательно, необходимо использовать метод эквивалентности refl

Таким образом, для удовлетворения моего типа подпись Агда принята: PA6 refl = refl

надеюсь, что помогает