Working on Peano's Axioms in Agda and Hitting a Slice of Point

Question

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

- this is an axiom that I'm trying to solve and support, I tried using cong (from the main library), but I had problems with the cong constructor

PA6 = cong

doesn't get me anywhere, I know that for cong I need to provide refl for equality and type, but I'm not sure which type I should provide. Ideas?

This is for a small assignment at the University, so I would prefer someone to demonstrate what I missed, instead of writing an answer, but I would appreciate any degree of support.

Answer 1

, , , refl

, agda : PA6 refl = refl

,

Answer 2

PA6 , ≡ .

Relation.Binary.PropositionalEquality.

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

( , , .)