\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.SubSet

\func TranslationAction (G : Group) : TransitiveGroupAction G \cowith
  | E => G
  | ** => G.*
  | **-assoc => G.*-assoc
  | **_ide => 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) : GSet 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))
  | **_ide => exts (\lam (e1 : G) => rewrite (G.inverse_ide, G.ide-left) idp)

-- action by conjugating its own elements
\func conjAction (G : Group) : GSet G \cowith
  | E => G
  | ** (g : G)  => conjugate g
  | **-assoc => pmap (_ *) G.inverse_* *> equation.group
  | **_ide {e : G} : conjugate G.ide e = e => conjugate-via-id

\func trivialAction (G : Group) (E : \Set) : GSet G E \cowith
  | ** _ e => e
  | **-assoc => idp
  | **_ide => idp

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