Bag

Idea

A bag is just a finite multiset.

Presentation

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

$$\frac{}{[]:\mathbf{Bag}(X)}\frac{x:Xxs:\mathbf{Bag}(X)}{(x::xs):\mathbf{Bag}(X)}\frac{x,y:Xxs:\mathbf{Bag}(X)}{x::(y::xs)=y::(x::xs)}$$