The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.  

Vladimir.