[Agda] excluded-middle

[Martin Escardo]

I am not familiar with the standard library. But What you quote below 
under the name excluded middle from the library is not excluded middle, 
which is not provable in intuitionistic logic (or in Agda unless 
something is wrong), but the intuitionistically valid principle that 
not-not(every type has an inhabitant or not). Martin

On 20/06/16 21:23, Katsutoshi Itoh wrote:
> Hi all.
>
> I'd like to use excluded-middle like below:
>
> ```
>   A∪Aᶜ≈U : ∀ {ℓ} {X : Set ℓ} {A : Pred X lzero} → A ∪ A ᶜ ≈ U
>    A∪Aᶜ≈U {A = A} = record { eql = A∪Aᶜ⊆U A , A∪Aᶜ⊇U A }
>      where
>        A∪Aᶜ⊆U : ∀ {ℓ} {X : Set ℓ} (A : Pred X lzero) → A ∪ A ᶜ ⊆ U
>        A∪Aᶜ⊆U A x∈A∪Aᶜ = tt
>
>        A∪Aᶜ⊇U : ∀ {ℓ} {X : Set ℓ} (A : Pred X lzero) → A ∪ A ᶜ ⊇ U
>        A∪Aᶜ⊇U A {x} tt = excluded-middle
>          where
>            postulate
>              excluded-middle : ∀ {a} {P : Set a} → P ⊎ ¬ P
> ```
>
> On the other hand, in standard library,
> I found excluded-middle at Relation.Nullary.Negation module.
> but, I didn't understand how to use it.
>
> ```
> excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
> excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
> ```
>
> Please teach me how to apply it in my case.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe