Ali Caglayan

Is that something to do for 8.14?

Nice! I just checked, it works with 8.13 so we just need to do it at some point.

I think `X_2functor` is fine. I would start with changing the O_functor's in ReflectiveSubuniverse to a more streamlined convention first as this seems to cover the shape of just about...

So we sort of have this now with alyectron. Although, the user cannot go and edit proof scripts in the browser. I am however a bit sceptical that being able...

Hi @ejgallego, thank you for the detailed reply! >[which can be annoying for some long running stuff, tho it is easy to cache them in a json] Yes, this is...

I don't quite understand what simpl does compared to cbn. I have read time and time again that cbn is "better behaved" but sometimes I have found that simpl does...

Sometimes I feel like simpl is clever enough not to reduce things down too much and get messy, wheras cbn just reduces everything until it hits a simpl nomatch. This...

The DHProp's that I have in mind is the current implementation of `leq` for nat for example. These do compute, and do so differently for simpl or cbn. Maybe this...

I had originally tried this but I couldn't get it to work. Now that Mike has the coercions working it might be worth trying again.

This can be done, but it means all lemmas involving homotopy groups get split into three cases. We cannot treat the group and abelian group cases together.