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

[Andreas Abel]

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
>