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.

• 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 : 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 $u a$ as the function required by the Univalence Axiom, but then lower case is the norm.

• CommentRowNumber10.
• CommentAuthorRichard Williamson
• CommentTime7 days ago
• (edited 7 days ago)

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

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTime7 days ago

Tweaked statement of rule

1. Looks good, thanks!