<div dir="ltr">Looks really interesting; I will definitely look into it.<div><br><div>But currently it is out of scope of my question. All I need is to investigate this inside Agda.</div><div>And In Agda I can prove that you cannot give me such `X` for which <span style="font-family:arial,sans-serif;font-size:13px">`X </span><span style="font-size:13px;font-family:arial,sans-serif">+ not X` is *not* inhabited (see `not-In-Agda` below)</span>:</div><div><br></div><div><div>¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)</div><div>¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))</div><div><br></div><div>not-In-Agda : ¬ (Σ Set λ X → ¬ (X ⊎ ¬ X))</div><div>not-In-Agda (X , p) = ¬¬lem′ X p</div><div><br></div><div>So, it's not the case in [at least 'standard'] Agda.</div><div>(Or probably I am missing the key essence of your message :-D)</div><div><br></div><div>Probably in Agda it is still possible to prove this?</div><div><br></div><div>Thanks,</div><div>Dmytro </div><div><br></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-12 12:46 GMT+03:00 Paolo Capriotti <span dir="ltr"><<a href="mailto:paolo@capriotti.io" target="_blank">paolo@capriotti.io</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Sun, Oct 12, 2014 at 8:24 AM, Dmytro Starosud <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>> wrote:<br>
> Which models do you mean?<br>
> Please share few keywords to google, or links.<br>
<br>
</span>There are models in which there exists a (small) type `X` such that `X<br>
+ not X` is *not* inhabited (e.g. any non-boolean Grothendieck topos).<br>
In such a model, the type `not ((A : Set) -> A + not A)` is inhabited.<br>
It follows that the type corresponding to the statement you want to<br>
prove is not.<br>
<span class="HOEnZb"><font color="#888888"><br>
Paolo<br>
</font></span></blockquote></div><br></div>