Lavorando su Assiomi di Peano in Agda e ha colpito un po ' un punto di attaccare

Question

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

è l'assioma sto cercando di risolvere e di supporto, ho provato con un cong (dalla libreria di base), ma sto avendo problemi con il cong costruttore

PA6 = cong

mi viene da nessuna parte, so per cong sono tenuti a fornire una reflex per la parità e un tipo, ma io non sono sicuro di che tipo dovrei alimentazione.Idee?

Questo è un piccolo assegnazione all'Università, quindi preferirei qualcuno di dimostrare ciò che ho perso, piuttosto che scrivere il acutual risposta, ma preferirei un qualsiasi grado di sostenere.

Answer 1

Per la natura del sistema che avevo creato, ho dovuto capire ho avuto due equivalenze e quindi bisogno di utilizzare l'equivalenza del metodo di rifl

Così per soddisfare il mio tipo di firma agda accettati: PA6 refl = refl

speranza che aiuta

Answer 2

Il tuo PA6 dice che ≡ è simmetrica.

Questo può essere trovato nella libreria standard dal modulo Relation.Binary.PropositionalEquality.

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

(Questa domanda è piuttosto vecchio, ma sto distacco a beneficio dei futuri lettori che inciampare su di esso.)