The Coq mailing list

[Andreas Abel <abela AT chalmers.se>]

Bruno, I like to read your habilitation thesis (I hope it is not in
French).  Where can I find it?

Cheers, Andreas

On 08.01.14 10:45 PM, Bruno Barras wrote:
> 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.
> 
> _______________________________________________
> Agda mailing list
> Agda AT lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>