The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Jan 6, 2014, at 6:45 PM, Cody Roux 
<cody.roux AT andrew.cmu.edu>
 wrote:

> On 01/06/2014 06:36 PM, Vladimir Voevodsky wrote:
>> In my opinion only those constructions which can be expressed through 
>> eliminators are trustworthy. There is really no other way to supply 
>> rigorousness to inductive types with  pseudo-parameters (or whatever they 
>> are now called) such as Id-types.
> This is simply not true, there are whole PhDs dedicated to describing 
> systems which can do better than eliminators. Andreas mentioned 
> sized-types, which are IMO the most mature candidate.
> 
> The fact that the implementation is behind the theoretical capabilities is 
> just that, an implementation problem.

Let's me say it in a more careful way: 

In my opinion only those constructions which can be expressed through 
eliminators are trustworthy since I do not know of any other way to supply 
rigorousness to inductive types with  pseudo-parameters (or whatever they are 
now called) such as Id-types *in the presence of univalence*.

Vladimir.