Working on Peano Axioms in Agda and hit a bit of a sticking point

Question

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

is the axiom I am trying to solve and support, I've tried using a cong (from the core library) but am having troubles with the cong constructor

PA6 = cong

gets me nowhere, I know for cong I am required to supply a refl for equality and a type, but I'm, not sure what type I'm supposed to supply. Ideas?

This is for a small assignment at University, so I'd rather someone demonstrate what I've missed rather than write the acutual answer, but I'd appreciate any degree of support.

Answer 1

By the nature of the system that I had created, I had to realise I had two equivalences and thus needed to use the equivalence method refl

Thus to satisfy my type signature agda accepted: PA6 refl = refl

hope that helps

Answer 2

Your PA6 says that ≡ is symmetric.

This can be found in the standard library from the Relation.Binary.PropositionalEquality module.

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

(This question is pretty old, but I'm posting for the benefit of future readers that stumble upon it.)