Matthieu Sozeau

Hopefully I will have time to look at it in november :)

Well, let's hope for december instead.

Hmm, mixing wf and structural definitions confuses the graph creation. That'll require a non-trivial change.

Yes, that needs to be sorted out, maybe `dependent induction` should just be exported by Equations always.

Just as a remark, I'm experimenting with more agressive minimization to try to lower these numbers, I'll keep you updated. In my experience one thing that can be tried otherwise...

I've went back on this. The problem is caused by using Let's in sections. Each Let introduces universes that are rigid so when they unifiy with each other you get...

@spitters nope, I've had no time to look into it. We should discuss this with @SkySkimmer and @ppedrot, maybe they have different ideas on how to tame this problem.

We should investigate why the uses provoke an inconsistency in V.v. I suppose this could be due to the absence of the implicit resizing with this new definition.

Yep, definitely would be great to have a HoTT/full-DTT compatible congruence, whereas Coq's current congruence closure algorithm does not handle dependency at all. We're thinking with N. Tabareau and E....

Yes, Setoid is just a historical name. What you want is generalized rewriting, i.e., rewriting with arbitrary relations in contexts that preserve them. With univalence, everything is equivalence-preserving, so you...