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: bracket type

Bottom of Page

1 to 13 of 13

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2011
    • (edited Sep 26th 2012)

    started bracket type, just for completeness, but don’t really have time for it

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2011

    had the chance to add a bit more to bracket type: now there is an Idea-section a Semantics-section.

    I have also added links to bracket type to relevant entries, in particular to types and logic - table.

    Experts please check. I am pretty sure I know what I am talking about here, but I may not be using language in the standard way.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2011

    I am somewhat surprised that the idea of “bracket types” is not already in the original articles on propositions as types. I had thought that taking bracket types is implicitly understood all along.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 3rd 2011
    Thanks! I edited bracket type a bit. Bracket types were actually already referred to at propositions as types, only not by that name -- in the final paragraph of the Idea section under the phrase "propositions as some types". I added extra clarification there as well.
    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012
    • (edited Sep 26th 2012)

    I have added to bracket type a brief section Definition in homotopy type theory with the definition of supp(A)supp(A).

    Also added four references on this. I see in Mike’s lectures the construction is attributed to Lumsdaine. However in the recent post by Brunerie, it seems to be attributed to Voevodsky. I don’t know. The entry currently does not cite Lumsdaine yet, but probably it should.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2012
    • (edited Sep 26th 2012)

    Voevodsky defined it, as Guillaume said, “using impredicative quantification and resizing rules” (and also univalence). I believe his definition simply mimics the classical proof that a (1-)topos is a regular category — univalence plus a resizing rule is just the way that you get a subobject classifier in HoTT.

    The definition as an HIT is what is due to Peter Lumsdaine.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 26th 2017

    I added the recursion principle for supp(A)supp(A). I also added to the notations for the bracket type. We’re up to 6 now.

  8. fixed HTML entities to UTF-8 characters in Agda snippet

    anqurvanillapy

    diff, v17, current

  9. added section relating propositional truncations to localizations.

    Anonymous

    diff, v23, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeFeb 20th 2023

    added pointer to

    and doi-link to:

    diff, v24, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2023

    added pointer to:

    Have only scanned the first few pages, but: Is this not secretly rediscovering the notion of anafunctor?

    diff, v25, current

    • CommentRowNumber12.
    • CommentAuthorGuest
    • CommentTimeMar 10th 2023

    added definition of bracket type using a type of all propositions.

    diff, v27, current

  13. Added definition of propositional truncation as a sequential colimit and added the reference where the definition came from

    Anonymouse

    diff, v31, current

1 to 13 of 13

  1.