Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
also created axiom UIP, just for completeness. But the entry still needs some reference or else some further details.
okay, added the statement. Hope I put the bracket type in the right place…
I have added brief cross-links between axiom UIP and univalence axiom
Is UIP technically contrary to the univalence axiom, or does this “just” only leave trivial models?
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.
In the Statement section are we saying that UIP is an element of that dependent product?
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!
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.
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.
Looks good, thanks!
1 to 12 of 12