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