The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

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