The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,

From what I understand it seems that universe polymorphism implies (by
definition) this "feature" that Type is not a Type but a "query for a
type universe". So getting rid of this feature seems to imply getting
rid of universe polymorphism. Is it worth the effort to implement a
switch to disable universe polymorphism (that are a great feature most
of the time) and this feature as a side effect? Is it what HoTT does?

Best regards,
P.

2012/4/19 Andrej Bauer 
<andrej.bauer AT andrej.com>:
> On Wed, Apr 18, 2012 at 11:03 PM, AUGER Cédric 
>Â <sedrikov AT gmail.com>
>  wrote:
>> Definition r : Type := forall x y : A, Q x y.
>>             ^^^^^^
>> isn't type casting simpler than defining Q' ?
>> I always found that giving explicitely the type of a symbol at top
>> level was nicer that making the reader to mentaly perform the type
>> inference.
>
> First, casting to "Type" is not a type annotation because Type is not
> a type... Coq gets to choose which one it is, and it can choose Prop.
> Second, what about intermediate expressions, how do I type those?
>
> Frederic makes a similar observation:
>
>> I agree with Andrej that this is not a desirable property to do type 
>> inference when a type is explicitly given.
>
> Again, and I was confused about this yesterday, Type is not a real
> type, so annotating with Type is not a real type annotation. Coq still
> has to infer something, namely the level, and as Hugo explained to me,
> the levels go
> Prop < Set < ... < Type(k) < ... Coq picks the lowest available.
>
> With kind regards,
>
> Andrej
>