# The precategory of group actions

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-03-17.

module group-theory.precategory-of-group-actions where

Imports
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

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


## Idea

The large precategory of group actions consists of group actions and morphisms of group actions between them.

## Definitions

### The large precategory of G-sets

module _
{l1 : Level} (G : Group l1)
where

action-Group-Large-Precategory :
Large-Precategory (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
action-Group-Large-Precategory =
make-Large-Precategory
( action-Group G)
( hom-set-action-Group G)
( λ {l1} {l2} {l3} {X} {Y} {Z} → comp-hom-action-Group G X Y Z)
( λ {l1} {X} → id-hom-action-Group G X)
( λ {l1} {l2} {l3} {l4} {X} {Y} {Z} {W} →
associative-comp-hom-action-Group G X Y Z W)
( λ {l1} {l2} {X} {Y} → left-unit-law-comp-hom-action-Group G X Y)
( λ {l1} {l2} {X} {Y} → right-unit-law-comp-hom-action-Group G X Y)


### The small precategory of G-sets

module _
{l1 : Level} (G : Group l1)
where

action-Group-Precategory :
(l2 : Level) → Precategory (l1 ⊔ lsuc l2) (l1 ⊔ l2)
action-Group-Precategory =
precategory-Large-Precategory (action-Group-Large-Precategory G)