search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

products and sums of setoids #879

Open HuStmpHrrr opened 5 years ago

HuStmpHrrr commented 5 years ago

it is interesting to see that there is no induced products and sums of setoids in this library yet. do I just overlook it or is it indeed the case.

MatthewDaggitt commented 5 years ago

If I understand what you're after correctly then they should be in 'Data.(Sum/Product).Relation.Binary.Equality.Setoid'?

HuStmpHrrr commented 5 years ago

hmm I don't find those modules though?

HuStmpHrrr commented 5 years ago

oh you meant Pointwise. I see, that's a bit tricky to notice.

MatthewDaggitt commented 5 years ago

Hmm, it definitely would be a little easier to find if the modules I suggested actually existed...

laMudri commented 5 years ago

non-dependent products, sums

But yeah, this is a classic problem of having two hierarchies (type formers and order structures), but only reflecting one of them in the module hierarchy.

JacquesCarette commented 1 year ago

So this issue really is about findability rather than missing functionality? I have seen sum and product of setoids in the 2.0 library (but, of course, I can't find them right now...)

jamesmckinna commented 6 months ago

non-dependent products, sums

But yeah, this is a classic problem of having two hierarchies (type formers and order structures), but only reflecting one of them in the module hierarchy.

So can we close this in favour of a separate issue about hierarchies?

So this issue really is about findability rather than missing functionality?

And would the 'hierarchy' issue help/solve the findability/navigability issue?

TL;DR: suggest we close this one, but open new, but more appropriately focused, issues instead?