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

오류가있는 곳을 알아 냈습니다. 위의 컷 - 다운 버전이 표시되지 않습니다.분명히 나는 클래스 자체의 이름이 첫 번째 초기화 후에 새로운 변수를 겹쳐 씁니다.

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.)