[Agda] Why is propositional equality "Set a" instead of just Set?

[Martin Escardo]

Thanks. I think this answers the question of universe level assignment 
for inductive definitions, and in particular propositional equality, as 
far as univalence is concerned. But are there criteria for 
"correcteness" of universe level assignment for equality, and more 
generally inductive definitions, other than univalence? What does a 
"purely constructive" look at the problem suggest? Martin

On 19/08/13 20:54, Nils Anders Danielsson wrote:
> On 2013-08-19 19:17, Martin Escardo wrote:
>> For example, a question that comes to mind immediately is what
>> universe level assignments are (in)compatible with univalence. Even if
>> one doesn't want to postulate univalence, I think it is interesting to
>> be compatible with univalence. (In the same way one wants to be
>> compatible with excluded middle, with continuity, with function
>> extensionality, etc.)
>
> Vladimir Voevodsky wrote the following in an old version of his
> Foundations library:
>
>    "IMPORTANT: for those who may want to add to these files. There are
> some rules which have to be followed in creating new definitions and
> theorems which at the moment are not tracked by the proof checker.
>
>    1. The current system of Coq is not completely compatible with the
> univalent semantics. The problem (the only one as far as I know) lies in
> the way the universe levels (u-levels) are assigned to the objects
> defined by the inductive definitions of the form
>
>    Inductive Ind (...)...(...): A -> Type := ...
>
>
>    The current u-level assignemet takes into account the u-levels of the
> constructors but not the u-level of A. To ensure compatibility with the
> univalent model the u-level of Ind should be no less than the u-level of
> A. The u-levels of the parameters (the types appearing in (...)...(...)
> ) do not matter.
>
>    A particular case of this problem is the "singleton elimination" rule
> which provides a good example of this incompatibility. The inductive
> definition of the identity types which uses one of the points as a
> parametr has A=:T (the underlying type) but since no mention of T
> appears in the constructor the system considers that there are no
> u-level restrictions on the resulting object and in particular that it
> can be placed in Prop while still having the full Ind_rect elimninator
> (see elimination, singleton elimination in the Index to the Refernce
> Manual).
>
>    Since in the present approach the universe management is made
> explicit one has:
>
>    RULE 1 Do not use inductive definitions of the form
>
>    Inductive Ind (...)...(...): A -> UU := ...
>
>    unless all the "arguments" of A can be typed to UU."
>
>
> https://github.com/vladimirias/Foundations/blob/5d74869805c341c89ee63d65430596bcbabfd32b/Main_Library/Generalities/uuu.v
>
>
> Hugo Herbelin has written a patch that changes the level assignment
> algorithm:
>
>
> https://github.com/vladimirias/Foundations/blob/master/Coq_patches/README
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe