AbVec

Idea

An Abelian vector is a bag with fixed cardinality. Alternatively it can be thought of as a vector in which the order of elements is irrelevant.

Presentation

A bag can be presented as an indexed quotient inductive type freely from the following constructors:

$$\frac{}{[]:\mathbf{AbVec}(X,0)}\frac{x:Xxs:\mathbf{Bag}(X,n)}{(x::xs):\mathbf{Bag}(X,n^{+})}\frac{x,y:Xxs:\mathbf{Bag}(X,n)}{x::(y::xs)=y::(x::xs)}$$