<div dir="ltr">Thank you all!<div>Looks like you gave me enough to read to solve my problem :)</div><div><br></div><div>Cheers,</div><div>Dima</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-12 17:10 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 1:20 PM, Paolo Capriotti <<a href="mailto:paolo@capriotti.io">paolo@capriotti.io</a>> wrote:<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>
<br>
</span>The answer should be no again. I think it suffices to look at the<br>
copresheaf category Set^ω. There, if I'm not mistaken, the type<br>
corresponding to "propositional" LEM is not just uninhabited, but<br>
globally 0. Therefore its double negation is 0 as well.<br>
<span class="HOEnZb"><font color="#888888"><br>
Paolo<br>
</font></span></blockquote></div><br></div>