<div dir="ltr">Btw, I was trying to look into this, but there is something missing with it:<div><br></div><div><div>isProp : Set → Set</div><div>isProp = _</div><div><br></div><div>PROP = ∃ λ A → isProp A</div><div><br></div><div>prop : ¬ ¬ ((A : PROP) → A ⊎ ¬ A)</div><div>prop = _</div></div><div><br></div><div>Agda doesn't want type check type of little prop</div><div>_⊎_ expects types as an arguments and negation expects type as an argument but A is of type PROP and thus is not type, but term.</div><div><br></div><div>Could you clarify what you meant to write? (unfortunately I failed to recover original meaning)</div><div><br></div><div>Thanks in advance,</div><div>Dima</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-12 15:20 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 12:05 PM, Dmytro Starosud <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>> wrote:<br>
> Looks really interesting; I will definitely look into it.<br>
><br>
> But currently it is out of scope of my question. All I need is to<br>
> investigate this inside Agda.<br>
> And In Agda I can prove that you cannot give me such `X` for which `X + not<br>
> X` is *not* inhabited (see `not-In-Agda` below):<br>
><br>
> ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)<br>
> ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))<br>
><br>
> not-In-Agda : ¬ (Σ Set λ X → ¬ (X ⊎ ¬ X))<br>
> not-In-Agda (X , p) = ¬¬lem′ X p<br>
><br>
> So, it's not the case in [at least 'standard'] Agda.<br>
> (Or probably I am missing the key essence of your message :-D)<br>
<br>
</span>Well, I wrote that `X` is such that `X + not X` is not inhabited, but<br>
that doesn't mean that `not (X + not X)` is inhabited, so there's no<br>
contradiction here.<br>
<br>
Nevertheless, I realised that what I wrote is incorrect. The negation<br>
of LEM is not (globally) true in the topos I was thinking about, so<br>
the statement you want to prove actually holds there. Sorry about<br>
that.<br>
<br>
It is still true that the statement is unprovable, but the argument<br>
needs to be a bit subtler. For example, Corollary 3.2.7 in the HoTT<br>
book (<a href="http://homotopytypetheory.org/book/" target="_blank">http://homotopytypetheory.org/book/</a>) shows that any model of<br>
type theory compatible with univalence falsifies the statement.<br>
<br>
That raises a further question: is the statement<br>
<br>
not not ((A : Prop) -> A + not A)<br>
<br>
provable (where Prop = Σ (A : Set) . isProp(A))?<br>
<span class="HOEnZb"><font color="#888888"><br>
Paolo<br>
</font></span></blockquote></div><br></div>