```\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Data.Array
\import Data.Or
\import Function.Meta
\import Logic
\import Paths
\import Relation.Equivalence
\import Set

\type PermSet (A : \Set) => Quotient {Array A} EPerm
\where {
\func inPS~ {A : \Set} (l : Array A) : Quotient EPerm => in~ l

\func inPS {A : \Set} (l : Array A) : PermSet A => in~ l

\lemma unext {A : \Set} {l l' : Array A} (p : inPS~ l = {PermSet A} inPS~ l') : TruncP (EPerm l l')
=> Quotient.equalityClosure EPerm.EPerm-equivalence (\lam e => inP e) (path (\lam i => p i))

\lemma ~-psequiv {A : \Set} {l l' : Array A} (e : EPerm l l') : inPS l = inPS l'
=> permSet-ext (~-pequiv e)
}

\open PermSet

\lemma permSet-ext {A : \Set} {x y : PermSet A} (p : x = {Quotient EPerm} y) : x = y
=> path (\lam i => p i)

\instance PermSetDec (A : DecSet) : DecSet (PermSet A)
| decideEq => \case \elim __, \elim __ \with {
| in~ l, in~ l' => \case EPerm.EPermDec {A} {l} {l'} \with {
| inl e => yes (~-psequiv e)
| inr q => no \lam p => \case unext p \with {
| inP p' => q p'
}
}
}

\instance PermSetMonoid (A : \Set) : CMonoid (PermSet A)
| ide => in~ nil
| * (x y : PermSet A) : PermSet A \with {
| in~ l, in~ l' => in~ (l ++ l')
| in~ l, ~-equiv l1 l2 r => ~-psequiv (EPerm.eperm-++-right r)
| ~-equiv l1 l2 r, in~ l => ~-psequiv (EPerm.eperm-++-left r)
}
| ide-left {x} => \case \elim x \with {
| in~ l => idp
}
| *-assoc {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
| in~ l1, in~ l2, in~ l3 => permSet-ext (pmap in~ ++-assoc)
}
| *-comm {x} {y} => \case \elim x, \elim y \with {
| in~ l, in~ l' => ~-psequiv EPerm.eperm-++-comm
}

\func permSet-map {A B : \Set} (f : A -> B) (s : PermSet A) : PermSet B \elim s
| in~ l => in~ (map f l)
| ~-equiv x y r => ~-psequiv (EPerm.EPerm_map f r)

\lemma permSet-map-comp {A B C : \Set} {f : A -> B} {g : B -> C} {s : PermSet A}
: permSet-map g (permSet-map f s) = permSet-map (\lam a => g (f a)) s \elim s
| in~ l => idp

\func permSet-hom {A B : \Set} (f : A -> B) : MonoidHom (PermSetMonoid A) (PermSetMonoid B) (permSet-map f) \cowith
| func-ide => idp
| func-* {x} {y} => \case \elim x, \elim y \with {
| in~ l, in~ l' => pmap inPS (map_++ f)
}

\lemma permSet-map_+ {A B : \Set} {f : A -> B} {x y : PermSet A} : permSet-map f (x * y) = permSet-map f x * permSet-map f y \elim x, y
| in~ l, in~ l' => permSet-ext \$ pmap in~ (map_++ f)

\func permSet-sum {A : CMonoid} (x : PermSet A) : A \elim x
| in~ l => A.BigProd l
| ~-equiv x y r => A.BigProd_EPerm r

\lemma permSet-sum-natural {A B : CMonoid} (f : MonoidHom A B) {x : PermSet A} : f (permSet-sum x) = permSet-sum (permSet-map f x) \elim x
| in~ l => f.func-BigProd

\lemma permSet-sum_+ {A : CMonoid} {x y : PermSet A} : permSet-sum (x * y) = permSet-sum x * permSet-sum y \elim x, y
| in~ l, in~ l' => A.BigProd_++

\func permSet-univ {A : \Set} {B : CMonoid} (f : A -> B) : MonoidHom (PermSetMonoid A) B \cowith
| func x => permSet-sum (permSet-map f x)
| func-ide => idp
| func-* => pmap permSet-sum permSet-map_+ *> permSet-sum_+

\lemma permSet-univ-natural {A B : CMonoid} (f : MonoidHom A B) {x : PermSet A} : f (permSet-sum x) = permSet-sum (permSet-map f x) \elim x
| in~ l => f.func-BigProd

\func permSet-zro-dec {A : \Set} (x : PermSet A) : Dec (x = 1) \elim x
| in~ nil => yes idp
| in~ (_ :: _) => no \lam p => \case unext p \with {
| inP e => \case EPerm.EPerm_len e
}

\lemma permSet-split {A : \Set} {l : Array A} : Monoid.BigProd (map (\lam a => inPS (a :: nil)) l) = inPS l \elim l
| nil => idp
| a :: l => pmap (_ *) permSet-split

\lemma permSet-pow {A : \Set} {a : A} {n : Nat} : Monoid.pow (inPS (a :: nil)) n = inPS (replicate n a)
=> inv Monoid.BigProd_replicate *> permSet-split

\func permSet-length {A : \Set} (p : PermSet A) : Nat \elim p
| in~ (l : Array) => l.len
| ~-equiv l l' e => EPerm.EPerm_len e```