\import Algebra.Group.Category
\import Algebra.Monoid
\import Data.Array
\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 (\new Equivalence (Array A) (\lam l l' => TruncP (EPerm l l')) {
        | ~-reflexive => inP EPerm.eperm-refl
        | ~-symmetric (inP e) => inP (EPerm.eperm-sym e)
        | ~-transitive (inP e1) (inP e2) => inP (eperm-trans e1 e2)
      }) (\lam e => inP e) (path (\lam i => p i))
  }

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

\instance PermSetAbMonoid (A : \Set) : AbMonoid (PermSet A)
  | zro => in~ nil
  | + (x y : PermSet A) : PermSet A \with {
    | in~ l, in~ l' => in~ (l ++ l')
    | in~ l, ~-equiv l1 l2 r => permSet-ext $ ~-pequiv (EPerm.eperm-++-right r)
    | ~-equiv l1 l2 r, in~ l => permSet-ext $ ~-pequiv (EPerm.eperm-++-left r)
  }
  | zro-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' => permSet-ext (~-pequiv 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 => permSet-ext $ ~-pequiv (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) : AddMonoidHom (PermSetAbMonoid A) (PermSetAbMonoid B) (permSet-map f) \cowith
  | func-zro => idp
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap PermSet.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 : AbMonoid} (x : PermSet A) : A \elim x
  | in~ l => A.BigSum l
  | ~-equiv x y r => A.BigSum_EPerm r

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

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

\func permSet-univ {A : \Set} {B : AbMonoid} (f : A -> B) : AddMonoidHom (PermSetAbMonoid A) B \cowith
  | func x => permSet-sum (permSet-map f x)
  | func-zro => idp
  | func-+ => pmap permSet-sum permSet-map_+ *> permSet-sum_+

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

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

\lemma permSet-split {A : \Set} {l : Array A} : AddMonoid.BigSum (map (\lam a => PermSet.inPS (a :: nil)) l) = PermSet.inPS l \elim l
  | nil => idp
  | a :: l => pmap (_ +) 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