Bag Equivalence via a Proof-Relevant Membership RelationBag Equivalence via a Proof-Relevant Membership Relation AbstractTwo lists are bag equivalent if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. This paper describes how one can define bag equivalence as the presence of bijections between sets of membership proofs. This definition has some desirable properties:
UpdatesThe paper states that the new definition of bag equivalence is equivalent to a more standard one. In the accompanying code it is proved that, if "bijection" is replaced by the equivalent concept of "weak equivalence" in the general versions of these definitions (those that work for all unary containers), then they are isomorphic (assuming extensionality). If the membership relation is not "set-valued" it is perhaps more appropriate to define the subbag relation in terms of what the Homotopy Type Theory book calls "embeddings" rather than injections. Nils Anders DanielssonLast updated Fri Jul 1 11:18:33 UTC 2016. |