agda
Permutation vs Bag equality
With @HuStmpHrrr's excellent addition, we now have two ways of looking at the same relation for lists. Unfortunately due to the current naming conventions the link between the two isn't obvious. One is in Data.List.Relation.Bag(AndSet)Equality and the other in Data.List.Relation.Permutation.Inductive.
Ideally before v1.0 it would be good if we could unify the two i.e refer them both as bag equalities, or both as permutations. Does anyone have any preferences as to which? Or a third suggestion!
This is very tricky, because although they implement "the same thing" they are conceptually very different. The point is that permutations are conceptually 'objects' which are fine on their own, yes "proof relevant bag equality" (to use @nad 's nice terminology from the paper where I learned this) also happen to be (essentially) permutations as well.
This occurs in group theory more generally: group exists as stand-alone objects, but also as generating group-actions on sets.
Classical mathematicians are happy to conflate these somewhat, as for them the morphism between a finite set of size n and Fin n is 'irrelevant' (or left implicit or ...). But constructively, this is not irrelevant!
So there is a point to having permutations (as objects), permutations that act on lists, permutations that act on tables, and even variants that act on lists-over-Setoid and table-over-Setoid.
A vote for "deep thinking required first". The current situation is not great. There can be more uniformity that lets one move between points of view more easily. But a proper design is not obvious. I would not hold up 1.0 for such a design, but warn people that this particular API for 'permutations' might change.
I prefer bag/set equivalence to bag/set equality. (I used to refer to the relations as equalities, but Fritz Henglein convinced me that the term equivalence is better.)
Following @JacquesCarette's advice and removing the v1.0 tag. Further discussion needed.
I'd nudge the community to consider closing this issue...
... @JacquesCarette made the good case against unifying the two notions, and I see no strong arguments for?
Feel free to reopen at a future date, but with an eye to current issues/PRs considering reorganising Permutation on List (and potentially multiplying the number of representations) I think this is ... out-of-date now!
