[Agda] PLFA - Negation - Exercise Classical

[David Banas]

Hi all,

In trying the "Classical" exercise near the end of the *Negation* chapter
in PLFA, I'm trying to show that excluded middle implies double negation
elimination with:

A⊎¬A⇒¬¬A→A : ∀ {A : Set}
  → A ⊎ ¬ A
    ---------
  → ¬ ¬ A → A
A⊎¬A⇒¬¬A→A (inj₁ a)   =  λ _ → a
A⊎¬A⇒¬¬A→A (inj₂ ¬A)  =  λ()


But Agda is complaining:

¬ (¬ A) should be empty, but that's not obvious to me
when checking that the expression λ () has type ¬ (¬ A) → A


I wrote a function proving that not-A implies not-//A:

¬¬¬-elim-inv : ∀ {A : Set}
  → ¬ A
    -------
  → ¬ ¬ ¬ A
¬¬¬-elim-inv ¬x  =  λ f → f ¬x


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.

Can anyone get me unstuck?

Thanks!
-db
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200824/eea7b6ef/attachment.html>