\import Algebra.Group
\import Algebra.Group.GSet
\import Category
\import Category.Meta
\import Function (IsInj, IsSurj)
\import Paths
\import Paths.Meta
\import Set.SetHom

\record EquivariantMap (G : Group) \extends SetHom {
  \override Dom : GroupAction G
  \override Cod : GroupAction G
  | func-** {e : Dom} {g : G} : func (g ** e) = g ** func e -- equivariance

  \func IsIso => \Sigma (IsSurj func) (IsInj func)
}

\func id-equivar {G : Group} (X : GroupAction G) : EquivariantMap G X X \cowith
  | func (x : X) => x
  | func-** {x : X} {g : G} => idp

\instance GSet (G : Group) : Cat (GroupAction G)
  | Hom A B => EquivariantMap G A B
  | id X => id-equivar X
  | o {x y z : GroupAction G} (g : EquivariantMap G y z) (f : EquivariantMap G x y) => \new EquivariantMap G {
    | func (a : x) => g (f a)
    | func-** {a : x} {h : G} =>
      g ( f (h ** a)) ==< pmap g func-** >==
      g (h ** f a) ==< func-** >==
      h ** g (f a) `qed
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam e _ => exts \lam g x => func-** {e}