## Bag Equivalence via a Proof-Relevant Membership RelationBag Equivalence via a Proof-Relevant Membership Relation ## AbstractTwo lists are - Many bag equivalences can be proved using a flexible form of equational reasoning.
- The definition generalises easily to arbitrary unary containers, including types with infinite values, such as streams.
- By using a slight variation of the definition one gets set equivalence instead, i.e. equality up to order and multiplicity. Other variations give the subset and subbag preorders.
- The definition works well in mechanised proofs.
## UpdatesThe paper states that the new definition of bag equivalence is 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 DanielssonDisclaimer Last updated Fri Jul 1 11:18:33 UTC 2016. |