<div dir="ltr">Hi all,<div><br></div><div>In trying the "Classical" exercise near the end of the <i>Negation</i> chapter in PLFA, I'm trying to show that excluded middle implies double negation elimination with:</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">A⊎¬A⇒¬¬A→A : ∀ {A : Set}</font></div><div><font face="monospace">  → A ⊎ ¬ A</font></div><div><font face="monospace">    ---------</font></div><div><font face="monospace">  → ¬ ¬ A → A</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₁ a)   =  λ _ → a</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₂ ¬A)  =  λ()</font></div></blockquote><div><br></div><div>But Agda is complaining:</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">¬ (¬ A) should be empty, but that's not obvious to me</font></div><div><font face="monospace">when checking that the expression λ () has type ¬ (¬ A) → A</font></div></blockquote><div><br></div><div>I wrote a function proving that not-A implies not-//A:</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">¬¬¬-elim-inv : ∀ {A : Set}</font></div><div><font face="monospace">  → ¬ A</font></div><div><font face="monospace">    -------</font></div><div><font face="monospace">  → ¬ ¬ ¬ A</font></div><div><font face="monospace">¬¬¬-elim-inv ¬x  =  λ f → f ¬x</font></div></blockquote><div><br></div><div>And Agda is happy with that proof, but not using it when evaluating the code above. And I can't quite figure out how to incorporate the proof supplied by the second block of code into the evaluation of the first.</div><div><br></div><div>Can anyone get me unstuck?</div><div><br></div><div>Thanks!</div><div>-db</div><div><br></div></div>