[Agda] Classical Mathematics for a Constructive World

[Dan Licata]

Hi Martin,

Thanks!  That makes more sense.  

I'm still a little confused about the difference between

  Exists X : Type. ¬(X + ¬ X)

which we cannot prove (it would be contradictory with the usual fact
that Pi X:Type. ¬¬(X + ¬ X) holds) and

  ¬Em = ¬(Pi X : Type. X + ¬X)

which we can prove with univlanece.  

I guess this is just saying that classical logic is inconsistent with
univalence, but it's a little surprising to me that a mere de Morgan 
will do us in.  

Do you have any intuition for this?  I want to say that it has something
to do with continuity:   ¬Em is asserting the absence of a "continuous"
proof of excluded middle.  

-Dan

On Nov27, Martin Escardo wrote:
>
> On 27/11/12 00:05, Dan Licata wrote:
>> I'd like to understand exactly what statement is true in HoTT but not
>> plain MLTT.
>
>
> Let EM be the (large) type (Pi X : Type. X + ¬X).
>
>    (1) MLTT cannot inhabit EM (of course).
>
>    (2) MLTT cannot inhabit ¬EM (because classical ZF gives a model in
>    which EM is inhabited).
>
> So EM is independent of MLTT.
>
> Now consider MLTT with the univalence axiom.
>
> By Hedberg's theorem, any type with decidable equality in an hset. So, if 
> EM holds, then every type is an hset.
>
> But if univalence holds, then there are large types which are not
> hsets, as is well known.
>
> Combining these two procedures, you get an inhabitant of ¬EM.
>
> Martin
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda