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: uniqueness of identity proofs

Bottom of Page

1 to 20 of 20

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2012
    • (edited May 3rd 2014)

    also created axiom UIP, just for completeness. But the entry still needs some reference or else some further details.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2012

    okay, added the statement. Hope I put the bracket type in the right place…

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2015

    I have added brief cross-links between axiom UIP and univalence axiom

    • CommentRowNumber4.
    • CommentAuthorNikolajK
    • CommentTimeMar 22nd 2017

    Is UIP technically contrary to the univalence axiom, or does this “just” only leave trivial models?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 22nd 2017

    Internally, it is technically contrary, in the sense that if you have both of them you can construct an inhabitant of ∅\emptyset. (This is the only possible internal meaning of “contrary”.) Externally, you are right that what this means is that only the trivial model satifies both.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 9th 2018

    In the Statement section are we saying that UIP is an element of that dependent product?

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 9th 2018
    • (edited Aug 9th 2018)

    I believe that what is intended is to assert (take as an axiom) that there is a term of that dependent product. I.e. if written as a rule, one would have nothing above the line and this judgement below it. I can try to write it like that later (no time just now). I myself would probably write it with A:TypeA : Type above the line, removing one term from the dependent product, but one might object that it looks less like an axiom then. I defer to whatever way to write it Mike would prefer!

    • CommentRowNumber8.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 9th 2018
    • (edited Aug 9th 2018)

    By the way, I find the statement that this axiom makes the type theory extensional slightly confusing; I think that what is meant is what is described as ’propositional extensionality’ at extensional type theory, whereas my default meaning for extensional type theory would be the stricter one.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 9th 2018

    So yes it could be like the use of uau a as the function required by the Univalence Axiom, but then lower case is the norm.

    • CommentRowNumber10.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 9th 2018
    • (edited Aug 9th 2018)

    Attempted to clarify the statement of the axiom as per the discussion above. Feel free to improve.

    diff, v5, current

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2018

    Tweaked statement of rule

    diff, v6, current

  12. Looks good, thanks!

  13. adding references for UIP in XTT.

    Anonymous

    diff, v9, current

  14. added section about definitional UIP.

    Anonymous

    diff, v9, current

  15. propositionally extensional type theory -> set-level type theory

    Anonymous

    diff, v9, current

  16. renaming page to “uniqueness of identity proofs” since not every formulation of UIP is an axiom.

    Anonymous

    diff, v9, current

  17. adding foundational axioms contents to sidebar

    Anonymous

    diff, v12, current

    • CommentRowNumber18.
    • CommentAuthorChristian Sattler
    • CommentTimeDec 10th 2023
    • (edited Dec 10th 2023)

    Axiom K technically stands for a combinator like J, only for loops instead of paths. People often conflate it with uniqueness of identity proofs (UIP) because they are interderivable when ignoring concerns about definitional equality.

    The wiki page should state the correct version. This used to be the case up until revision 15. Maybe this was part of the flood of HoTT-related edits a year ago.

    Now, some parts, like the subsection on computational behaviour doesn’t make any sense anymore.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2023
    • (edited Dec 10th 2023)

    Looking through the page history over at axiom K (type theory), the only other substantial edit by Anonymous is, besides revision 15, their revision 24, the rest of the many edits are single-word adjustments by Anonymous.

    Hence if we rolled back to revision 11, the last version before the notorious Anonymous came in, it would be the material of revisions 15 and 24 that would be reverted.

    I suppose it would be justified.

    (I guess the Anonymous editor here is the “Anonymouse” who is still around, judging from their signature move to write “could” where it needs “can” or “may”.)

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeDec 11th 2023

    I have now rolled back the edits by “Anonymous” at axiom K (type theory) (as announced there).

1 to 20 of 20

  1.