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