The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 08/01/2014 20:55, Vladimir Voevodsky wrote:
> On Jan 8, 2014, at 12:40 PM, Cody Roux 
> <cody.roux AT andrew.cmu.edu>
>  wrote:
>> That's fair, but I don't see why eliminators have a more powerful
>> ontological status than sized-types. They require work to be derived as
>> well, and the correctness proofs for them are quite similar to that for
>> sized types. This seems like a matter of preference. Obviously I'm not
>> neutral in this matter though.
>>
>> Best,
>>
>> Cody
>>
> In the case of the univalent model eliminators are better because I have 
> invested a lot of effort into checking that they are compatible with the 
> model (some details of it are at the end of my "Notes on Type Systems").

As Cody said, it is likely that a lot of this work can be reused (or at
least adapted) if you switch to sized-types. The only new ingredient is
ordinal iteration, and the fact that those ordinals are not used in the
process you iterate. This is what I call "stage irrelevance" in my
habilitation thesis. Andreas has something similar in his
implementation. IIUC it's an implicit product, which is much more
flexible than stage irrelevance, but harder to understand set-theoretically.

I must admit that the situation is quite different with higher inductive
types. The eliminator does not split into pattern-matching + fixpoint in
the obvious way. That's the main blocking issue I'm facing in my
implementation of HITs. (I've tried to explain this in Barcelona last
September.) However, I'm not going to surrender so easily.

Bruno.