Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: double negation modality / (-1)-truncation modality

Bottom of Page

1 to 7 of 7

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2013
    • (edited Nov 3rd 2013)

    I have created a stub for n-truncation modality and cross-linked with double negation modality.

    I gather that double negation = (-1)-truncation in a “predicative context”, but maybe I don’t fully understand yet what predicativity has to do with it.

    • CommentRowNumber2.
    • CommentAuthorspitters
    • CommentTimeNov 3rd 2013
    Do you mean "classical context" ? Why would all propositions equal their double negation constructively?
    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2013

    Yes, sorry, I am thinking classical context here.

    Just remind me, in generality, the double negation modality and the (-1)-truncation modality are related by which kind of map?

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeNov 4th 2013

    If you just mean the direction, the map goes from ‖A‖ −1{\|A\|}_{-1} to ¬(¬A)\neg(\neg{A}).

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 4th 2013

    Does it have any special properties? (e.g. nn-connected for some nn)

    • CommentRowNumber6.
    • CommentAuthorZhen Lin
    • CommentTimeNov 4th 2013

    I think it fails to even be (-1)-connected (because it’s rarely an effective epimorphism).

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2013

    Where “rarely” = “iff LEM holds”.

1 to 7 of 7

  1.