agda / cubical

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

Towards schemes of finite presentation without size issues #1080

Open mzeuner opened 9 months ago

mzeuner commented 9 months ago

Redoing the relevant parts of https://github.com/agda/cubical/pull/1068 for finitely presented algebras and this time without raising universe levels.