--------------------------------------------------------------------------------
Ettore Aldrovandi ealdrovandi@fsu.edu
Keri D'Angelo kd349@cornell.edu

June 2022
--------------------------------------------------------------------------------

Group actions on sets and Torsors, following the UniMath blueprint. We
add a couple of things:

1. actions give homomorphisms into groups of automorphisms and
   viceversa.
2. pullbacks of actions.
3. G Sets

Torsors are in their own file Torsos.lagda


\begin{code}

{-# OPTIONS --safe --without-K #-}

open import Groups.Type renaming (_β‰…_ to _≣_)
open import MLTT.Spartan
open import UF.Base hiding (_β‰ˆ_)
open import UF.Embeddings
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.FunExt
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.UA-FunExt
open import UF.Univalence

module Groups.GroupActions where

module _ (G : Group 𝓀) where

  action-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
  action-structure X = ⟨ G ⟩ β†’ X β†’ X

  action-axioms : (X : 𝓀 Μ‡ ) β†’ action-structure X β†’ 𝓀 Μ‡
  action-axioms X _Β·_ = is-set X Γ—
                        ((g h : ⟨ G ⟩)(x : X) β†’ (g ·⟨ G ⟩ h) Β· x ＝ g Β· (h Β· x)) Γ—
                        ((x : X) β†’ (unit G) Β· x ＝ x)

  Action-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
  Action-structure X = Ξ£ _Β·_ κž‰ action-structure X , (action-axioms X _Β·_)

  Action : 𝓀 ⁺ Μ‡
  Action = Ξ£ X κž‰ 𝓀 Μ‡ , Action-structure X


  action-carrier : Action β†’ 𝓀 Μ‡
  action-carrier (X , _ ) = X

  action-op : (𝕏 : Action) β†’ action-structure ⟨ 𝕏 ⟩
  action-op (X , op , _) = op

  carrier-is-set : (𝕏 : Action) β†’ is-set (action-carrier 𝕏)
  carrier-is-set (X , op , i , _) = i

  action-assoc : (𝕏 : Action) (g h : ⟨ G ⟩) (x : ⟨ 𝕏 ⟩)
               β†’  (action-op 𝕏) (g ·⟨ G ⟩ h) x ＝ (action-op 𝕏) g ((action-op 𝕏) h x)
  action-assoc (X , op , i , a , u) = a

  action-unit : (𝕏 : Action) (x : ⟨ 𝕏 ⟩)
              β†’  (action-op 𝕏) (unit G) x ＝ x
  action-unit (X , op , i , a , u) = u

  action-tofun : (𝕏 : Action) (g : ⟨ G ⟩) β†’ ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩
  action-tofun 𝕏 g = Ξ» x β†’ action-op 𝕏 g x

  action-to-fun = action-tofun

  action-tofun-is-equiv : (𝕏 : Action) (g : ⟨ G ⟩) β†’ is-equiv (action-tofun 𝕏 g)
  action-tofun-is-equiv 𝕏 g =
            (f⁻¹ , Ξ» x β†’ (f (f⁻¹ x)                   ＝⟨ (action-assoc 𝕏 _ _ _) ⁻¹ ⟩
                          (g ·⟨ G ⟩ (inv G g)) β—‚βŸ¨ 𝕏 ⟩ x ＝⟨ ap (Ξ» v β†’ v β—‚βŸ¨ 𝕏 ⟩ x) (inv-right G g) ⟩
                          (unit G) β—‚βŸ¨ 𝕏 ⟩ x            ＝⟨ action-unit 𝕏 x  ⟩
                           x ∎)) ,
            (f⁻¹ , Ξ» x β†’ (f⁻¹ (f x)                   ＝⟨ (action-assoc 𝕏 _ _ _) ⁻¹ ⟩
                          ((inv G g) ·⟨ G ⟩ g) β—‚βŸ¨ 𝕏 ⟩ x ＝⟨ ap (Ξ» v β†’ v β—‚βŸ¨ 𝕏 ⟩ x) (inv-left G g) ⟩
                          (unit G) β—‚βŸ¨ 𝕏 ⟩ x            ＝⟨ action-unit 𝕏 x ⟩
                           x  ∎))
    where
      _β—‚βŸ¨_⟩_ : ⟨ G ⟩ β†’ (𝕏 : Action) β†’ ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩
      g β—‚βŸ¨ 𝕏 ⟩ x = action-op 𝕏 g x

      f : ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩
      f = action-tofun 𝕏 g

      f⁻¹ : ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩
      f⁻¹ = action-tofun 𝕏 (inv G g)

  action-to-fun-is-equiv = action-tofun-is-equiv

  action-to-Aut : (𝕏 : Action) (g : ⟨ G ⟩) β†’ Aut ⟨ 𝕏 ⟩
  action-to-Aut 𝕏 g = (action-to-fun 𝕏 g) , action-to-fun-is-equiv 𝕏 g

  -- same names as in UniMath
  left-mult = action-to-fun
  right-mult : (𝕏 : Action) (x : ⟨ 𝕏 ⟩) β†’ ⟨ G ⟩ β†’ ⟨ 𝕏 ⟩
  right-mult 𝕏 x = Ξ» g β†’ action-op 𝕏 g x
  ----------------------------------

  -- the total action map is often used, especiall for torsors
  ------------------------------------------------------------
  mult : (𝕏 : Action)
       β†’  ⟨ G ⟩ Γ— ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩ Γ— ⟨ 𝕏 ⟩
  mult 𝕏 (g , x) = action-op 𝕏 g x , x

\end{code}

In this submodule we prove that an action as defined above induces a
homomorphism from the group G to the automorphism group of the carrier
set. It requires funext 𝓀 𝓀 because Aut (X) (as a group)
does. Conversely, a homomorphism to Aut (X) gives an action.

\begin{code}
  module to-automorphism (fe : funext 𝓀 𝓀)
                         (𝕏 : Action)
                           where

    open import Groups.Aut
    open import Groups.Opposite

    is-hom-action-to-fun : is-hom G ((𝔸ut fe ⟨ 𝕏 ⟩ (carrier-is-set 𝕏)) α΅’α΅–) (action-to-Aut 𝕏)
    is-hom-action-to-fun {g} {h} =
                         to-Ξ£-＝ ((dfunext fe (Ξ» x β†’ action-assoc 𝕏 g h x)) ,
                                  being-equiv-is-prop'' fe (Ξ» x β†’ g Β· (h Β· x)) _ _)
                         where
                                   _Β·_ : ⟨ G ⟩ β†’ ⟨ 𝕏 ⟩ β†’ ⟨ 𝕏 ⟩
                                   _Β·_ = action-op 𝕏


  module from-automorphism (fe : funext 𝓀 𝓀)
                           (X : 𝓀 Μ‡ )(i : is-set X)
                           (Οƒ : ⟨ G ⟩ β†’ Aut X)
                             where
    open import Groups.Aut
    open import Groups.Opposite

    hom-to-Aut-gives-action : is-hom G ((𝔸ut fe X i) α΅’α΅– ) Οƒ β†’ Action
    hom-to-Aut-gives-action is = X , ((Ξ» g β†’ pr₁ (Οƒ g)) ,
                            (i , (Ξ» g h β†’ happly (ap pr₁ (is {g} {h}))) ,
                             Ξ» x β†’ ( pr₁ (Οƒ (unit G)) x  ＝⟨ happly (ap pr₁ t) x ⟩
                                     pr₁ (unit 𝔸utX) x    ＝⟨ happly' id id refl x ⟩
                                     x ∎ ) ) )
      where
        𝔸utX : Group 𝓀
        𝔸utX = 𝔸ut fe X i
        t : Οƒ (unit G) ＝ unit 𝔸utX
        t = homs-preserve-unit G ((𝔸ut fe X i) α΅’α΅– ) Οƒ is


\end{code}

Resuming the general theory, the group action axioms form a proposition
and the Action-structure is a set.

\begin{code}
  action-axioms-is-prop : funext 𝓀 𝓀
                        β†’ (X : 𝓀 Μ‡)
                        β†’ (_Β·_ : action-structure X)
                        β†’ is-prop (action-axioms X _Β·_)
  action-axioms-is-prop fe X _Β·_ s = Ξ³ s
    where
      i : is-set X
      i = pr₁ s

      Ξ³ : is-prop (action-axioms X _Β·_)
      Ξ³ = Γ—-is-prop (being-set-is-prop fe)
                    (Γ—-is-prop (Ξ -is-prop fe
                                  (Ξ» g β†’ Ξ -is-prop fe
                                     (Ξ» h β†’ Ξ -is-prop fe
                                        (Ξ» x β†’ i))))
                        (Ξ -is-prop fe (Ξ» x β†’ i)))


  Action-structure-is-set : funext 𝓀 𝓀
                          β†’ (X : 𝓀 Μ‡)
                          β†’ is-set (Action-structure X)
  Action-structure-is-set fe X {s} = Ξ³ {s}
    where
      i : is-set X
      i = pr₁ (prβ‚‚ s)

      Ξ³ : is-set (Action-structure X)
      Ξ³ = Ξ£-is-set (Ξ -is-set fe
                      (Ξ» g β†’ Ξ -is-set fe
                               (Ξ» x β†’ i)))
            Ξ» op β†’ props-are-sets (action-axioms-is-prop fe X op)

\end{code}


Equivariant maps.

\begin{code}

  is-equivariant : (𝕏 𝕐 : Action) (f : ⟨ 𝕏 ⟩ β†’ ⟨ 𝕐 ⟩) β†’ 𝓀 Μ‡
  is-equivariant 𝕏 𝕐 f = βˆ€ g x β†’ f (g Β· x) ＝ g * (f x)
    where
      _Β·_ = action-op 𝕏
      _*_ = action-op 𝕐


  is-equivariant-is-prop : funext 𝓀 𝓀
                         β†’ (𝕏 𝕐 : Action) β†’ (f : ⟨ 𝕏 ⟩ β†’ ⟨ 𝕐 ⟩)
                         β†’ is-prop (is-equivariant 𝕏 𝕐 f)
  is-equivariant-is-prop fe 𝕏 𝕐 f s = Ξ³ s
    where
      i : is-set (action-carrier 𝕐)
      i = carrier-is-set 𝕐

      Ξ³ : is-prop (is-equivariant 𝕏 𝕐 f)
      Ξ³ = Ξ -is-prop fe
                    (Ξ» g β†’ Ξ -is-prop fe
                                     (Ξ» x β†’ i))

  is-equivariant-comp : (𝕏 𝕐 β„€ : Action)
                      β†’ (p : ⟨ 𝕏 ⟩ β†’ ⟨ 𝕐 ⟩) (i : is-equivariant 𝕏 𝕐 p)
                      β†’ (q : ⟨ 𝕐 ⟩ β†’ ⟨ β„€ ⟩) (j : is-equivariant 𝕐 β„€ q)
                      β†’ (is-equivariant 𝕏 β„€ (q ∘ p))
  is-equivariant-comp 𝕏 𝕐 β„€ p i q j g x = q (p (g Β· x)) ＝⟨ ap q (i g x) ⟩
                                          q (g * (p x)) ＝⟨ j g (p x) ⟩
                                          g ✡ (q (p x)) ∎
    where
      _Β·_ = action-op 𝕏
      _*_ = action-op 𝕐
      _✡_ = action-op β„€

\end{code}

The following "fundamental" fact from UniMath is that an
identification p : ⟨ 𝕏 ⟩ ＝ ⟨ 𝕐 ⟩ between the carriers of two actions
essentially gives rise to an equivariant map. More precisely,
equivariance of the identity is the same as the identification of the
structures.

\begin{code}

  ＝-is-equivariant : funext 𝓀 𝓀
                    β†’ (𝕏 𝕐 : Action)
                    β†’ (p : ⟨ 𝕏 ⟩ ＝ ⟨ 𝕐 ⟩)
                    β†’ (transport Action-structure p (prβ‚‚ 𝕏)  ＝ prβ‚‚ 𝕐 ) ≃
                     is-equivariant 𝕏 𝕐 (idtofun ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ p)
  pr₁ (＝-is-equivariant fe (X , as) (.X , .as) refl) refl = Ξ» g x β†’ refl
  prβ‚‚ (＝-is-equivariant fe (X , as) (.X , as') refl) =
    logically-equivalent-props-give-is-equiv
      is (is-equivariant-is-prop fe ((X , as)) (X , as') id)
        (pr₁ (＝-is-equivariant fe (X , as) (X , as') refl))
        Ξ» i β†’ to-Ξ£-＝ ((Ξ³ i) , (action-axioms-is-prop fe X _Β·'_ _ _))
      where
        _Β·_ _Β·'_ : action-structure X
        _Β·_  = pr₁ as
        _Β·'_ = pr₁ as'

        is : is-prop (as ＝ as')
        is = Action-structure-is-set fe X {as} {as'}

        Ξ³ : is-equivariant (X , as) (X , as') id β†’ _Β·_ ＝ _Β·'_
        Ξ³ = Ξ» i β†’ dfunext fe
                  (Ξ» g β†’ dfunext fe Ξ» x β†’ i g x)
\end{code}

The above function is called is_equivariant_identity in UniMath.

\begin{code}

  Action-Map : (𝕏 𝕐 : Action) β†’ 𝓀  Μ‡
  Action-Map 𝕏 𝕐 = Ξ£ f κž‰ (⟨ 𝕏 ⟩ β†’ ⟨ 𝕐 ⟩) , is-equivariant 𝕏 𝕐 f

  underlying-function : (𝕏 𝕐 : Action) (u : Action-Map 𝕏 𝕐) β†’ ⟨ 𝕏 ⟩ β†’ ⟨ 𝕐 ⟩
  underlying-function _ _ u = pr₁ u

  equivariance : {𝕏 𝕐 : Action} (u : Action-Map 𝕏 𝕐) β†’
                 is-equivariant 𝕏 𝕐 (underlying-function 𝕏 𝕐 u)
  equivariance u = prβ‚‚ u


  Action-Map-is-set : funext 𝓀 𝓀
                    β†’ (𝕏 𝕐 : Action)
                    β†’ is-set (Action-Map 𝕏 𝕐)
  Action-Map-is-set fe 𝕏 𝕐 {s} = Ξ³ {s}
    where
      Ξ³ : is-set (Action-Map 𝕏 𝕐)
      Ξ³ = Ξ£-is-set (Ξ -is-set fe
                     (Ξ» u β†’ carrier-is-set 𝕐))
                   Ξ» f β†’ props-are-sets (is-equivariant-is-prop fe 𝕏 𝕐 f)

  compose-Action-Map : {𝕏 𝕐 β„€ : Action}
                     β†’ (Action-Map 𝕏 𝕐) β†’ (Action-Map 𝕐 β„€)
                     β†’ (Action-Map 𝕏 β„€)
  compose-Action-Map {𝕏} {𝕐} {β„€} (p , i) (q , j) =
                     (q ∘ p) , (is-equivariant-comp 𝕏 𝕐 β„€ p i q j)

  Action-Iso : (𝕏 𝕐 : Action) β†’ 𝓀 Μ‡
  Action-Iso 𝕏 𝕐 = Ξ£ f κž‰ ⟨ 𝕏 ⟩ ≃ ⟨ 𝕐 ⟩ , is-equivariant 𝕏 𝕐 (eqtofun f)

  Action-Iso-is-set : funext 𝓀 𝓀
                    β†’ (𝕏 𝕐 : Action)
                    β†’ is-set (Action-Iso 𝕏 𝕐)
  Action-Iso-is-set fe 𝕏 𝕐 {s} = Ξ³ {s}
    where
      Ξ³ : is-set (Action-Iso 𝕏 𝕐)
      Ξ³ = Ξ£-is-set (Ξ£-is-set (Ξ -is-set fe (Ξ» _ β†’ carrier-is-set 𝕐))
                             Ξ» f β†’ props-are-sets (being-equiv-is-prop'' fe f))
                   Ξ» u β†’ props-are-sets (is-equivariant-is-prop fe 𝕏 𝕐 (pr₁ u))

  underlying-iso : (𝕏 𝕐 : Action) β†’ Action-Iso 𝕏 𝕐 β†’ ⟨ 𝕏 ⟩ ≃ ⟨ 𝕐 ⟩
  underlying-iso 𝕏 𝕐 u = pr₁ u

  underlying-iso-is-embedding : funext 𝓀 𝓀
                              β†’ (𝕏 𝕐 : Action)
                              β†’ is-embedding (underlying-iso 𝕏 𝕐)
  underlying-iso-is-embedding fe 𝕏 𝕐 =
    pr₁-is-embedding (Ξ» f β†’ is-equivariant-is-prop fe 𝕏 𝕐 (pr₁ f))

  underlying-iso-injectivity : funext 𝓀 𝓀
                             β†’ (𝕏 𝕐 : Action)
                             β†’ (u v : Action-Iso 𝕏 𝕐)
                             β†’ (u ＝ v) ≃ (underlying-iso 𝕏 𝕐 u ＝ underlying-iso 𝕏 𝕐 v)
  underlying-iso-injectivity fe 𝕏 𝕐 u v =
    ≃-sym (embedding-criterion-converse
             (underlying-iso 𝕏 𝕐)
             (underlying-iso-is-embedding fe 𝕏 𝕐) u v)


  underlying-Action-Map : (𝕏 𝕐 : Action) β†’ Action-Iso 𝕏 𝕐
                        β†’ Action-Map 𝕏 𝕐
  underlying-Action-Map _ _ ((f , _) , is) = f , is

  id-Action-Iso : (𝕏 : Action) β†’ Action-Iso 𝕏 𝕏
  id-Action-Iso 𝕏 = (id , (id-is-equiv ⟨ 𝕏 ⟩)) , (Ξ» g x β†’ refl)

  ＝-to-Action-Iso : {𝕏 𝕐 : Action}
                   β†’ 𝕏 ＝ 𝕐 β†’ Action-Iso 𝕏 𝕐
  ＝-to-Action-Iso {𝕏} {𝕐} p = transport (Action-Iso 𝕏) p (id-Action-Iso 𝕏)

  ＝-to-Action-Iso₁ : {𝕏 𝕐 : Action}
                    β†’ 𝕏 ＝ 𝕐 β†’ Action-Iso 𝕏 𝕐
  ＝-to-Action-Iso₁ {𝕏} {.𝕏} refl = id-Action-Iso 𝕏

  ＝-to-Action-Iso-compare : {𝕏 𝕐 : Action} β†’ (u : 𝕏 ＝ 𝕐)
                           β†’ ＝-to-Action-Iso {𝕏} {𝕐} u ＝ ＝-to-Action-Iso₁ {𝕏} {𝕐} u
  ＝-to-Action-Iso-compare {𝕏} {.𝕏} refl = refl


  compose-Action-Iso : {𝕏 𝕐 β„€ : Action}
                     β†’ Action-Iso 𝕏 𝕐 β†’ Action-Iso 𝕐 β„€
                     β†’ Action-Iso 𝕏 β„€
  compose-Action-Iso {𝕏} {𝕐} {β„€} (f , i) (g , j) =
                     (f ● g) , (is-equivariant-comp 𝕏 𝕐 β„€ (pr₁ f) i (pr₁ g) j)

  compose-Action-Iso-id : funext 𝓀 𝓀
                        β†’ {𝕏 𝕐 : Action} β†’ (u : Action-Iso 𝕏 𝕐)
                        β†’ compose-Action-Iso {𝕏} {𝕐} {𝕐} u (id-Action-Iso 𝕐) ＝ u
  compose-Action-Iso-id fe {𝕏} {𝕐} u = to-subtype-＝
                           (Ξ» f β†’ is-equivariant-is-prop fe 𝕏 𝕐 (eqtofun f))
                           (≃-refl-right' fe fe fe (pr₁ u))

  compose-id-Action-Iso : funext 𝓀 𝓀
                        β†’ {𝕏 𝕐 : Action} β†’ (u : Action-Iso 𝕏 𝕐)
                        β†’ compose-Action-Iso {𝕏} {𝕏} {𝕐} (id-Action-Iso 𝕏) u ＝ u
  compose-id-Action-Iso fe {𝕏} {𝕐} u = to-subtype-＝
                           (Ξ» f β†’ is-equivariant-is-prop fe 𝕏 𝕐 (eqtofun f))
                           (≃-refl-left' fe fe fe (pr₁ u))
\end{code}

Univalence for group actions. The abstract clause below is to speed up
type-checking.

\begin{code}

  module _ (ua : is-univalent 𝓀) where

    private
      fe : funext 𝓀 𝓀
      fe = univalence-gives-funext ua

    Id-equiv-Action-Iso_prelim : (𝕏 𝕐 : Action)
                               β†’ (𝕏 ＝ 𝕐) ≃ (Action-Iso 𝕏 𝕐)
    Id-equiv-Action-Iso_prelim 𝕏 𝕐 = ≃-comp (Ξ¦ , ll) (Ξ¨ , ii)
      where
        T : (𝕏 𝕐 : Action) β†’ (𝓀 ⁺) Μ‡
        T 𝕏 𝕐 = Ξ£ u κž‰ ⟨ 𝕏 ⟩ ＝ ⟨ 𝕐 ⟩ , transport Action-structure u (prβ‚‚ 𝕏) ＝ prβ‚‚ 𝕐

        Ξ¦ : (𝕏 ＝ 𝕐) β†’ T 𝕏 𝕐
        Φ = from-Σ-＝

        Ξ¦' : T 𝕏 𝕐 β†’ (𝕏 ＝ 𝕐)
        Φ' = to-Σ-＝

        Ξ¨ : T 𝕏 𝕐 β†’ Action-Iso 𝕏 𝕐
        Ξ¨ (p , is) = (idtoeq ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ p) , pr₁ (＝-is-equivariant fe 𝕏 𝕐 p) is

        abstract
          Ξ¨' : Action-Iso 𝕏 𝕐 β†’ T 𝕏 𝕐
          Ξ¨' (e , is) = p , pr₁ (≃-sym (＝-is-equivariant fe 𝕏 𝕐 p)) i
            where
              p : ⟨ 𝕏 ⟩ ＝ ⟨ 𝕐 ⟩
              p = eqtoid ua ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ e
              i : is-equivariant 𝕏 𝕐 (idtofun ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ p)
              i = transport (is-equivariant 𝕏 𝕐) (t ⁻¹) is
                where
                  t : idtofun ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ p ＝ eqtofun e
                  t = idtofun-eqtoid ua e

          Ξ¨'Ξ¨-id : (Οƒ : T 𝕏 𝕐) β†’ Ξ¨' (Ξ¨ Οƒ) ＝ Οƒ
          Ξ¨'Ξ¨-id (p , is) = to-Ξ£-＝ (eqtoid-idtoeq ua ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ p ,
                                   Action-structure-is-set fe _ _ _)

          ΨΨ'-id : (u : Action-Iso 𝕏 𝕐) β†’ Ξ¨ (Ξ¨' u) ＝ u
          ΨΨ'-id (e , is) = to-Ξ£-＝ ((idtoeq-eqtoid ua ⟨ 𝕏 ⟩ ⟨ 𝕐 ⟩ e) ,
                                   (is-equivariant-is-prop fe 𝕏 𝕐 _ _ _))
        ii : is-equiv Ξ¨
        ii = qinvs-are-equivs Ξ¨ inv-Ξ¨
          where
            inv-Ξ¨ : invertible Ξ¨
            inv-Ψ = Ψ' , (Ψ'Ψ-id , ΨΨ'-id)

        ll : is-equiv Ξ¦
        ll = qinvs-are-equivs Ξ¦ inv-Ξ¦
          where
            inv-Ξ¦ : invertible Ξ¦
            inv-Φ = Φ' , (tofrom-Σ-＝ , fromto-Σ-＝)


    ＝-to-Action-Iso-is-equiv : {𝕏 𝕐 : Action}
                              β†’ is-equiv (＝-to-Action-Iso {𝕏} {𝕐})
    ＝-to-Action-Iso-is-equiv {𝕏} {𝕐} = equiv-closed-under-∼'
                             (prβ‚‚ (Id-equiv-Action-Iso_prelim 𝕏 𝕐)) h
      where
        f = pr₁ (Id-equiv-Action-Iso 𝕏 prelim 𝕐)
        g = ＝-to-Action-Iso
        h : f ∼ g
        h refl = refl


    Id-equiv-Action-Iso : (𝕏 𝕐 : Action)
                        β†’ (𝕏 ＝ 𝕐) ≃ (Action-Iso 𝕏 𝕐)
    Id-equiv-Action-Iso 𝕏 𝕐 = ＝-to-Action-Iso , ＝-to-Action-Iso-is-equiv

\end{code}

A shorthand for the action structure. Convenient in function signature types.

\begin{code}

action-op-syntax : (G : Group 𝓀) (𝕏 : Action G) β†’ action-structure G ⟨ 𝕏 ⟩
action-op-syntax G 𝕏 = action-op G 𝕏
syntax action-op-syntax G 𝕏 g x = g β—‚βŸ¨ G ∣ 𝕏 ⟩ x

\end{code}

When explicitly expressed in terms of a group G, the type Action is
just that of G-Sets, so we also use this notation.

\begin{code}

_Sets : Group 𝓀 β†’ 𝓀 ⁺ Μ‡
G Sets = Action G

\end{code}

For a group homomorphism Ο† : H β†’ G the action pulls back, because it
is a functor from the one-object category G[1] to sets.

\begin{code}

action-pullback : {H G : Group 𝓀}
                β†’ (f : ⟨ H ⟩ β†’ ⟨ G ⟩) β†’ is-hom H G f
                β†’ G Sets β†’ H Sets
action-pullback {H = H} {G} f i ρ = (action-carrier G ρ) ,
                (Ξ» h x β†’ (f h) Β· x) ,
                  (carrier-is-set G ρ) ,
                    ((Ξ» h h₁ β†’ Ξ» x β†’ (f (h ·⟨ H ⟩ h₁) Β· x       ＝⟨ ap (_Β· x) i ⟩
                                      ((f h) ·⟨ G ⟩ (f h₁)) Β· x ＝⟨ action-assoc G ρ _ _ _ ⟩
                                      (f h Β· (f h₁ Β· x)) ∎  )) ,
                     Ξ» x β†’ (f (unit H) Β· x ＝⟨ ap (_Β· x) p ⟩
                            unit G · x     ＝⟨ action-unit G ρ x ⟩
                            x  ∎))
  where
    _·_ = action-op G ρ
    p  = homs-preserve-unit H G f i
\end{code}

TODO: The left adjoint, that is, the map H Sets β†’ G Sets along the
homomorphism H β†’ G. It uses the quotient module.