Slightly more generalized universes

Open Trebor-Huang opened this issue 2 years ago • 1 comments

https://github.com/agda/cubical/blob/132a2a3197b490c571356f0399a2a6fbfab40f2a/Cubical/Foundations/Transport.agda#L170C1-L170C1

This could be slightly improved with ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}. It's too trivial so I won't submit a PR here. Also we might need to test whether it breaks level inference downstream.

Jul 08 '23 03:07 Trebor-Huang

Feel free to make a PR if nothing breaks. I like short PRs that make things better :-)

Jul 09 '23 10:07 mortberg

I take that it is already fixed by the PR?

Aug 10 '24 15:08 Trebor-Huang