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: mere proposition

Bottom of Page

1 to 20 of 20

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 7th 2014

    an entry for mere proposition had been missing. Created a minimum, just so as to satisfy links.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeMar 9th 2014

    What's the difference between this and an h-proposition?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2014

    None.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMar 10th 2014
    • (edited Mar 10th 2014)

    I had said that explicitly at h-proposition but apparently not at mere proposition. Have added now the following:

    This is the same concept as that of h-proposition as well as that of (-1)-truncated homotopy type and (-1)-groupoid (if these are understood in the general context of geometric homotopy types).

    The terminology “mere proposition” is meant to better work in informal language in view of the propositions as types interpretation, where every type XX “is” a proposition in a way, or rather represents a proposition, namely the mere proposition which is its (-1)-truncation isInhab (X).

    I seem to remember that the h-level terminology got sort of deprecated. In any case, we have similarly duplicating entries for (-2)-truncation (true, unit type, contractible type). I’d think it’s okay, but of course if anyone feels like rather merging these entries, I won’t object.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2014

    The duplicating entries for (-2)-truncation actually mean different things, e.g. the unit type is a particular type with a particular definition, whereas being contractible is a property of an arbitrary type. But h-proposition and mere proposition are synonyms, so I think the pages should be merged.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2014

    That's my thought as well, but I wasn't sure whether it was true that they are synonyms, so I'm glad that you answered that.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2014

    The difference between -2-groupoid and contractible type is quite similarly not in the technical meaning but more in which reader my end up looking for which term.

    But if you have strong editorial feelings about this then you probably have the energy to reorganize it.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2014

    No, a (-2)-groupoid is a concept in category theory, whereas a contractible type is a concept in type theory.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2014

    I’ve merged them.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2014

    Hey Mike, I am not sure if we should stage arguments in this form over what are less than trivialities. Please have it your way, you are welcome. I suppose you have a strong feeling of ownership of this topic and its incarnation in words.

    As you know, there were once people who titled their article “Types are omega-groupoids”, there are equivalences justifying this language, there are good reasons to emphasize the equivalence over the superficial differences. There are different styles of talking, but as long as there is no substantial issue, maybe we can relax a bit?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2014

    I’m not angry or annoyed, sorry if I gave that impression. I just have less time than usual to spend carefully phrasing my comments to avoid unintentionally giving offense. Sorry. (-:

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2014

    The point I’m making, if it matters any more, is that “mere proposition” and “h-proposition” mean literally the same thing by definition, which is not the case for any of the other pairs of concepts you’ve mentioned.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeMar 12th 2014

    To me, it also matters that ‘mere proposition’ and ‘h-proposition’ are used by the same people in the same context, which isn't so for ‘(−2)(-2)-groupoid’ and ‘contractible type’.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 3rd 2018

    I can convince myself that ∏ x:A∏ y:A(x=y)\prod_{x\colon A} \prod_{y\colon A} (x=y) and ∏ x:A∏ y:AisContr(x=y)\prod_{x\colon A} \prod_{y\colon A} isContr(x=y) are equivalent, but is there a nice slick way to show this?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMar 4th 2018

    I don’t know a particularly slick way.

  16. adding natural deduction syntax rules for isProp; not sure how to define these without product types

    Anonymous

    diff, v11, current

  17. adding rules for isProp which does not involve product types

    Anonymous

    diff, v12, current

  19. adding standard rules for isProp

    Anonymous

    diff, v18, current

  20. adding section on the principles of omniscience for mere propositions

    Anonymouse

    diff, v26, current

1 to 20 of 20

  1.