search

agda / cubical

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

Generalized Universe Levels in 'substInPaths' #1076

Closed kesleta closed 9 months ago

kesleta commented 9 months ago

Made substInPaths slightly more general by allowing A and B to be Types with different levels. Suggested by #1022.