Our great sponsors
-
He's saying that you should treat that implementation of lists-as-sets as being commutative, but with the caveat that you need to regard lists that are permutations of each other (i.e. lists that have the same elements, possibly in a different order) as equivalent. In this setting, you identify "equivalent" elements -- if R is an equivalence relation, and R a b, and [a] and [b] are their equivalence classes, you say [a] = [b]. Lean has a type for quotients where you get equality in sense (although strictly speaking, lean's quotients aren't implemented as equivalence classes).
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.