This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Orbits of group actions

module group-theory.orbits-group-actions where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

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

Idea

The groupoid of orbits of a group action consists of elements of X, and a morphism from x to y is given by an element g of the group G such that gx ＝ y.

Definition

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

  hom-orbit-action-Group :
    (x y : type-action-Group G X) → UU (l1 ⊔ l2)
  hom-orbit-action-Group x y =
    Σ (type-Group G) (λ g → mul-action-Group G X g x ＝ y)