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

Schroedinger
  • 1,273
  • 14
  • 32

2 Answers2

7

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

glguy
  • 1,090
  • 7
  • 8
3

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

Schroedinger
  • 1,273
  • 14
  • 32
  • Please post a bit more about the solution so it can help others who have a similar problem (at least your definition of ℕ and _≡_, or the lib version and module name if they are from a library). Upvote will follow :) – fishlips Apr 05 '10 at 09:14