\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 = ) \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