[Agda] excluded-middle

[Katsutoshi Itoh]

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.

-- 
----
いとう かつとし
cutsea110 at gmail.com