The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Sep 24, 2011, at 1:50 PM, Adam Chlipala wrote:

> Vladimir Voevodsky wrote:
>> On Sep 24, 2011, at 1:34 PM, Adam Chlipala wrote:
>> 
>>   
>>> Vladimir Voevodsky wrote:
>>>     
>>>> It is arguable whether overusing induction and Prop is of any benefit 
>>>> for the type-theoretic formalization of mathematics. In my experience 
>>>> one can formalize everything with very few uses of [ Inductive ] and no 
>>>> use of Prop at all.
>>>> 
>>>>       
>>> There are two questions here: inductive definitions vs. an impredicative 
>>> universe.  I'm a believer in the usefulness of inductive definitions and 
>>> increasingly a skeptic about the need for impredicativity.
>>>     
>> Existence of a projection from any universe U to Prop defined by [ 
>> inhabited ] ( an inductive definition ) is essentially equivalent to 
>> impredicativity of Prop.
>>   
> 
> Perhaps I don't understand some subtlety here.  The alternative to Coq's 
> impredicative Prop that I have in mind is dropping both Prop and Set, so 
> that we only have a simple infinite Type hierarchy of predicative 
> universes.  (Is this what Agda does?  That's been my impression.)

I am all for dropping both Prop and Set. Still some kind of impredicativity 
will be required e.g. through the use of what I call "resizing rules". For 
example if one has a term of the type  X -> empty it should be possible to 
consider X as a member of the smallest universe. 

I gave a presentation about this on TYPES2011 see 
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_Bergen.pdf
 where I discuss the complications which arise when one tries to work with 
strictly impredicative universe hierarchy.

Vladimir.

PS Note that if one drops Prop then one also drops inductive definitions with 
values in Prop and then, for example, the definition of subgroup generated by 
a subset which Daniel writes about won't work. To replace it with another 
definition - the intersection of all the subgroups which contain the given 
subset, one needs a "resizing rule" since otherwise the subgroup generated by 
a subset will be typed to the larger universe than the subset itself.