search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

chore: Universal properties of colimits quantify over all universe levels #1126

Closed fredrik-bakke closed 2 months ago

fredrik-bakke commented 2 months ago

Refactors all universal properties and induction principles of colimits to quantify over all universe levels. This still leaves some lemmas about pushout cocones in an awkward position, but I leave that for future work.