Working on Peano Axioms in Agda and hit a bit of a sticking point
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'开发者_JS百科d appreciate any degree of support.
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.)
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
精彩评论