search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

Slightly more generalized universes #1022

Closed Trebor-Huang closed 1 month ago

Trebor-Huang commented 1 year ago

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.

mortberg commented 1 year ago

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

Trebor-Huang commented 1 month ago

I take that it is already fixed by the PR?