Implement IsPullback suggestions

agda / agda-categories

A new Categories library for Agda

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

MIT License

367 stars 68 forks source link

Implement IsPullback suggestions #431

Closed jacquescomeaux closed 1 month ago

jacquescomeaux commented 2 months ago

This pull request is intended to address issue #334.

Tasks:

[x] Move unique field to bottom
[x] Replace unique with unique-diagram
[x] Reconsider naming

jacquescomeaux commented 2 months ago

What about naming? Is unique-diagram the right name for the property now included as a record field?

JacquesCarette commented 1 month ago

Thanks for the updates (and sorry on my slowness!). On name: unique-diagram seems super generic (as was unique...) but if we're going to change it, then maybe unique-pb-square would be more indicative?

jacquescomeaux commented 1 month ago

I don't really think the name needs to change. I just wanted to make sure there wasn't an obviously-better alternative before I consider the PR done.

JacquesCarette commented 1 month ago

Sure, we can go with that and see if people complain.