\begin{code}
{-# OPTIONS --safe #-}

module Examples.Bag where

open import Prelude hiding (A)
open import Data.Nat.Properties using (isSetNat)


private
  variable
    A : Type
    x y : A
    xs ys zs : List A

module _ {A : Type} where
  infix  _↺_
\end{code}
%<*perm>
\begin{code}
  data _↺_ : List A → List A → Type where
    swap  : x ∷ y ∷ ys ↺ y ∷ x ∷ ys
    cons  : ∀ x → xs ↺ ys → x ∷ xs ↺ x ∷ ys
\end{code}
%</perm>
\begin{code}
Bag : Type → Type
\end{code}
%<*bag-def>
\begin{code}[inline*]
Bag A = List A / _↺_
\end{code}
%</bag-def>
%<*bag-size>
\begin{code}
size : Bag A → ℕ
size = rec/ isSetNat length ϕ where
  ϕ : (xs ys : List A) → xs ↺ ys → length xs ≡ length ys
  ϕ _ _ swap            = refl
  ϕ _ _ (cons _ xs↺ys)  = cong suc (ϕ _ _ xs↺ys)
\end{code}
%</bag-size>