Changes for Rocq PR#21164 #2318
Conversation
| (** Because [IsTrunc] is cumulative, we can use only one universe variable here. *) | ||
| #[export] Instance istrunc_truncation@{i} (n : trunc_index) (A : Type@{i}) | ||
| : IsTrunc@{i} n (Trunc@{i} n A). |
There was a problem hiding this comment.
We decided to make IsTrunc (really, IsTrunc_internal) cumulative, but this extra flexibility makes it harder for Rocq to choose universe variables optimally. E.g. with the original version of istrunc_truncation, there is not a unique choice of j, since anything smaller than the desired j will work. With this change, there is no longer the flexibility to choose j, making it easier for Rocq, but then Rocq can fail to find a solution in other situations. It's a bit of a dilemma, and we might end up making different design decisions once we have algebraic universes.
|
Looks good to me. If the change is backward compatible, maybe you can merge now so that we can easily run a bench for Rocq PR#21164 ? |
|
I had a look this morning, no comments from me. LGTM |
|
@jdchristensen I have updated the Rocq PR rocq-prover/rocq#21164 to handle cumulative inductive type properly, so you can revert last commit HoTTBookExercises: make build with Rocq PR#21164 |
|
@tabareau Thanks, I'll do that. Just out of curiosity, do you know if the other commits in this PR are still needed? I think they are fine to keep, but I wonder if cumulativity was also the issue in those places. |
|
It's not clear to me that the last commit in #21164 is a good idea, for now I'd just wait for this PR to converge before partially reverting stuff or fixing it further. |
4 participants
The changes here make Coq-HoTT build with Rocq PR rocq-prover/rocq#21164
Each commit is independent, and in all but the last case, these are simplifications that are good to have anyways. (The last case is a minor change, so not a big deal.)
@ppedrot @tabareau