qiitBag

-- 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 : El a → El Bag → El Bag
             ; swp : (x : El a) (y : El 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)
def swapG : (a : 𝕌) (x : El a) (y : El a) (m : El (Bag a)) →
            ins _ x (ins _ y m) ≡ ins _ y (ins _ x m) ∈ _ ≔
  λa. λx. λy. λm. ⋆

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

-- instances: applications of the generic definitions
def swapN : ins _ Z (ins _ (S Z) (nil _)) ≡ ins _ (S Z) (ins _ Z (nil _)) ∈ _ ≔
  swapG _ Z (S Z) (nil _)

def sizeTwoN : size _ (ins _ Z (ins _ (S Z) (nil _))) ≡ S (S Z) ∈ _ ≔ ⋆
def sizeOneU : size _ (ins _ () (nil _)) ≡ S Z ∈ _ ≔ ⋆