The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.)