We already have a pointwise product setoid in the lib; see Relation.Binary.Product.Pointwise. Gergo -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.chalmers.se/pipermail/agda/attachments/20130111/05066041/attachment.html