The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Kris,

You are right, seems that it is proper term. Thanks for the link.

Sincerely,
Kirill Taran

On Thu, Feb 13, 2014 at 4:19 AM, Kristopher Micinski <krismicinski AT gmail.com> wrote:

You might find this little talk by Matthieu Sozeau instructive (he is
also on this list).  I could assume someone will point out the current
state of things here, since I don't really understand it very well...

http://mattam.org/research/publications/Universe_Polymorphism_and_Inference_in_Coq-IAS-051212.pdf

Kris

On Wed, Feb 12, 2014 at 7:17 PM, Kristopher Micinski
<krismicinski AT gmail.com> wrote:
> On Wed, Feb 12, 2014 at 6:32 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:
>> Ali Assaf,
>>
>> You are right, I meant *why* and your answer makes things more clear.
>>
>>> For example, you will need multiple versions of the logical connectives
>>> False, /\, \/, ... at every Type level.
>> Am I right that in Agda we don't pay this cost because we have implicit
>> arguments?
>> (So we define connectives polymorphly on implicit level argument, so we use
>> them the same way e use them in Coq.)
>>
>
> The term for this is universe polymorphism, which is being added to
> Coq iirc?  But while you can't quantify over levels explicitly in Coq,
> they're all held implicit until the kernel solves for constraints.
>
> Kris