Janitorial work on equivalences and embeddings

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Closed fredrik-bakke closed 6 months ago

fredrik-bakke commented 6 months ago

Extracts changes made in #1078 to parts of the library outside of modal-type-theory.

fredrik-bakke commented 6 months ago

Would you mind if I added some changes from #1032 in this pull request too, or do you want me to open a different pull request for those?

fredrik-bakke commented 6 months ago

I'd say they mesh well with the theme of this PR.

EgbertRijke commented 6 months ago

I'd say they mesh well with the theme of this PR.

I'd rather just merge this one, since I already reviewed it in the other PR.