Homomorphisms of higher group actions

module higher-group-theory.homomorphisms-higher-group-actions where
Imports 
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import higher-group-theory.higher-group-actions
open import higher-group-theory.higher-groups

Definition

Homomorphisms of higher group actions

module _
  {l1 l2 l3 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
  (Y : action-∞-Group l3 G)
  where

  hom-action-∞-Group : UU (l1 ⊔ l2 ⊔ l3)
  hom-action-∞-Group = (u : classifying-type-∞-Group G) → X u → Y u

  map-hom-action-∞-Group :
    hom-action-∞-Group → type-action-∞-Group G X → type-action-∞-Group G Y
  map-hom-action-∞-Group f = f (shape-∞-Group G)

  preserves-mul-hom-action-∞-Group :
    (f : hom-action-∞-Group) (g : type-∞-Group G)
    (x : type-action-∞-Group G X) →
    ( map-hom-action-∞-Group f (mul-action-∞-Group G X g x)) ＝
    ( mul-action-∞-Group G Y g (map-hom-action-∞-Group f x))
  preserves-mul-hom-action-∞-Group f g x = preserves-tr f g x

Homotopies of morphisms of higher group actions

module _
  {l1 l2 l3 : Level} (G : ∞-Group l1) (X : action-∞-Group l2 G)
  (Y : action-∞-Group l3 G) (f : hom-action-∞-Group G X Y)
  where

  htpy-hom-action-∞-Group : (g : hom-action-∞-Group G X Y) → UU (l1 ⊔ l2 ⊔ l3)
  htpy-hom-action-∞-Group g = (u : classifying-type-∞-Group G) → (f u) ~ (g u)

  extensionality-hom-action-∞-Group :
    (g : hom-action-∞-Group G X Y) →
    (f ＝ g) ≃ htpy-hom-action-∞-Group g
  extensionality-hom-action-∞-Group =
    extensionality-Π f
      ( λ u g → f u ~ g)
      ( λ u g → equiv-funext)

  htpy-eq-hom-action-∞-Group :
    (g : hom-action-∞-Group G X Y) →
    (f ＝ g) → htpy-hom-action-∞-Group g
  htpy-eq-hom-action-∞-Group g =
    map-equiv (extensionality-hom-action-∞-Group g)

  eq-htpy-hom-action-∞-Group :
    (g : hom-action-∞-Group G X Y) →
    htpy-hom-action-∞-Group g → (f ＝ g)
  eq-htpy-hom-action-∞-Group g =
    map-inv-equiv (extensionality-hom-action-∞-Group g)