\import Algebra.Group
\import Algebra.Group.GSet.GSet
\import Algebra.Group.Sub
\import Category
\import Category.Meta
\import Function (isInj, isSurj)
\import Function.Meta ($)
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Category

\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 { | Dom => X | Cod => X} \cowith
  | func (x : X) => x
  | func-** {x : X} {g : G} => idp

\instance GSet (G : Group) : Cat (GroupAction G)
  | Hom A B => EquivariantMap G { | Dom => A | Cod => 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}