agda-stdlib products and sums of setoids

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.

Sep 03 '19 20:09 HuStmpHrrr

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

Sep 03 '19 22:09 MatthewDaggitt

hmm I don't find those modules though?

Sep 03 '19 23:09 HuStmpHrrr

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

Sep 03 '19 23:09 HuStmpHrrr

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

Sep 05 '19 11:09 MatthewDaggitt

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.

Sep 11 '19 11:09 laMudri

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...)

Jun 13 '23 21:06 JacquesCarette