\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.GSet
\import Algebra.Meta
\import Algebra.Monoid
\import Logic
\import Paths
\import Paths.Meta
\import Set

\func TranslationAction (G : Group) : TransitiveGroupAction G \cowith
  | E => G
  | ** => G.*
  | **-assoc => inv G.*-assoc
  | id-action => G.ide-left
  | isTransAction => \lam (v v' : G) => inP (v' G.* inverse v, rewrite (G.*-assoc, G.inverse-left) G.ide-right)

\func TranslationActionOnSubsets (G : Group) : GroupAction G \cowith
  | E => SubSet G
  | ** (g : G) (p : SubSet G) => \new SubSet G {| contains h => p.contains (inverse g G.* h)}
  | **-assoc {_ : G} {_ : G} {_ : SubSet G} => ext (ext (\lam (_ : G) => rewrite (inv G.*-assoc, inv G.inverse_*) idp))
  | id-action => exts (\lam (e1 : G) => rewrite (G.inverse_ide, G.ide-left) idp)

-- action by conjugating its own elements
\func conjAction (G : Group) : GroupAction G \cowith
  | E => G
  | ** (g : G)  => conjugate g
  | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e =>
      conjugate m (conjugate n e) ==< pmap (conjugate m) idp >==
      conjugate m (n * e * inverse n ) ==< idp >==
      m * (n * e * inverse n ) * inverse m ==< equation >==
      (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >==
      (m * n) * e * inverse (m * n) ==< idp >==
      conjugate (m * n) e `qed
  | id-action {e : G} : conjugate G.ide e = e => conjugate-via-id

\func trivialAction (G : Group) (E : BaseSet) : GroupAction G E \cowith
  | ** _ e => e
  | **-assoc => idp
  | id-action => idp

\func conjugate-subset {G : Group} (g : G) (S : SubSet G) : SubSet G \cowith
  | contains h => S.contains (conjugate (inverse g) h)