Higher group actions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-10.
Last modified on 2023-09-15.

module higher-group-theory.higher-group-actions where
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import higher-group-theory.higher-groups


An action of a higher group G on a type is just a type family over BG.


action-∞-Group :
  {l1 : Level} (l2 : Level) (G : ∞-Group l1)  UU (l1  lsuc l2)
action-∞-Group l2 G = classifying-type-∞-Group G  UU l2

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

  type-action-∞-Group : UU l2
  type-action-∞-Group = X (shape-∞-Group G)

  mul-action-∞-Group :
    type-∞-Group G  type-action-∞-Group  type-action-∞-Group
  mul-action-∞-Group = tr X

  associative-mul-action-∞-Group :
    (h g : type-∞-Group G) (x : type-action-∞-Group) 
    (mul-action-∞-Group (mul-∞-Group G h g) x) 
    (mul-action-∞-Group g (mul-action-∞-Group h x))
  associative-mul-action-∞-Group = tr-concat {B = X}

  unit-law-mul-action-∞-Group :
    (x : type-action-∞-Group)  mul-action-∞-Group refl x  x
  unit-law-mul-action-∞-Group x = refl

Recent changes