You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
Trebor-Huang
changed the title
Slightly more generalizable universes
Slightly more generalized universes
Jul 8, 2023
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.The text was updated successfully, but these errors were encountered: