search

agda / cubical

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

Another minor universe level generalisation #1138

Closed awswan closed 3 weeks ago

awswan commented 3 weeks ago

Another minor generalisation in universe levels, this one in Unit.Properties. I seem to send a lot of these, but they are all things that actually came up while I was using the library.

awswan commented 3 weeks ago

Less sure about this after noticing it breaks stuff, but it is following the principle of maximum universe generality.

awswan commented 3 weeks ago

Sorry for sending two commits to fix the same thing after sending the pull request. I'm satisfied now and I'll stop touching it.

mortberg commented 3 weeks ago

Looks good to me! Thanks for catching these small things