Not signed in (Sign In)

Start a new discussion

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).
    • 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

  1. Looks good, thanks!

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)