search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Trivial cleanup of imports that were commented out. #307

Closed sstucki closed 3 years ago

sstucki commented 3 years ago

The only reason I'm submitting this as a PR (rather than pushing it to master) is this change in src/Categories/Category/Cocartesian/Bundle.agda. It looks like there's some unfinished work there that was left in a comment. Did you leave it there intentionally @JacquesCarette?

JacquesCarette commented 3 years ago

Indeed, I didn't finish that, but the extra items were not needed anywhere, so I figured I'd come back to it when there was a real need. It's fine to delete.