Qiit.bag

-- Finite multisets over ANY carrier code (docs/NovaFoundation.txt,
-- worked example, over its ambient Γ = [a : 𝕌]): points quotiented by
-- the swap equation. Every generated def abstracts over the carrier,
-- and so does everything defined below — instances are applications.

data [a : 𝕌]
  Bag : U
  nil : El Bag
  ins : a → El Bag → El Bag
  swp : (x : a) (y : a) (m : El Bag) → ins x (ins y m) ≡ ins y (ins x m) ∈ El Bag

-- the imposed equation, GENERICALLY, via the store (the generated swp
-- lemma discharges the ⋆ at every carrier at once)
swapG : {a : 𝕌} {x y : a} {m : Bag a} → ins a x (ins a y m) ≡ ins a y (ins a x m) ∈ Bag a
  using (Qiit.bag.Bag.unfold, Qiit.bag.ins.eq, swp)
swapG = λa x y m. ⋆

-- size, defined once for every carrier — the method is
-- order-insensitive, so the coherence argument is ⋆
size : (a : 𝕌) → Bag a → ℕ using (Qiit.bag.Bag.unfold)
size = λa m. BagElim a (λb. ℕ) Z (λx r ih. S ih) (λx y r ih. ⋆) m

-- instances: applications of the generic definitions
swapN : ins ℕ Z (ins ℕ (S Z) (nil ℕ)) ≡ ins ℕ (S Z) (ins ℕ Z (nil ℕ)) ∈ Bag ℕ
  using (Qiit.bag.Bag.eq)
swapN = swapG

sizeTwoN : size ℕ (ins ℕ Z (ins ℕ (S Z) (nil ℕ))) ≡ 2
  using (Qiit.bag.Bag.eq, Qiit.bag.BagElim.eq, Qiit.bag.ins.eq, Qiit.bag.nil.eq, Qiit.bag.size.eq)
sizeTwoN = ⋆

sizeOneU : size 𝟙 (ins 𝟙 () (nil 𝟙)) ≡ S Z
  using (Qiit.bag.Bag.eq, Qiit.bag.BagElim.eq, Qiit.bag.ins.eq, Qiit.bag.nil.eq, Qiit.bag.size.eq)
sizeOneU = ⋆