[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Vladimir Voevodsky]

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.