open import Algebra.Group
open import Level
open import Data.Product
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

module Algebra.G-Set {ℓ : Level} where
  open Group using () renaming (Carrier to ∣_∣)
  record G-Set (G : Group ℓ) : Set (suc ℓ) where
    open Group G using (ε; _∙_)
    field
      X : Set ℓ
      _⊳_ : ∣ G ∣ → X → X
    field
      ε⊳ : ∀ {x : X} → ε ⊳ x ≡ x
      ∘⊳ : ∀ {g h : ∣ G ∣} {x : X} → (g ∙ h) ⊳ x ≡ (g ⊳ (h ⊳ x))

    -- orb : X → Set ℓ
    -- orb x = Σ[ y ∈ X ] Σ[ g ∈ ∣ G ∣ ] g ⊳ x ≡ y

    -- Orb : Set ℓ
    -- Orb = Σ[ x ∈ X ] orb x

    record orb (x : X) : Set ℓ where
      constructor orb[_,_,_]
      field
        y : X
        g : ∣ G ∣
        .eq : g ⊳ x ≡ y

    orb-intro : ∀ {x : X} {y z : X} {g h : ∣ G ∣} {eq₁ : g ⊳ x ≡ y} {eq₂ : h ⊳ x ≡ z} (p : y ≡ z) (q : g ≡ h)
                → ≡.subst₂ (λ y g → g ⊳ x ≡ y) p q eq₁ ≡ eq₂
                → orb[ y , g , eq₁ ] ≡ orb[ z , h , eq₂ ]
    orb-intro ≡.refl ≡.refl ≡.refl = ≡.refl

    record Orb : Set ℓ where
      constructor Orb[_,_]
      field
        x : X
        o : orb x

    Orb-intro : ∀ {x y : X} {o₁ : orb x} {o₂ : orb y} (p : x ≡ y)
                → ≡.subst (λ x → orb x) p o₁ ≡ o₂
                → Orb[ x , o₁ ] ≡ Orb[ y , o₂ ]
    Orb-intro ≡.refl ≡.refl = ≡.refl


  open G-Set using () renaming (X to ∣_∣)

  IsEquivariant : ∀ {G : Group ℓ} (X Y : G-Set G) (f : ∣ X ∣ → ∣ Y ∣) → Set ℓ
  IsEquivariant {G} X Y f = ∀ {g : ∣ G ∣} {x : ∣ X ∣} → f (g ⊳ˣ x) ≡ g ⊳ʸ (f x)
    where
      open G-Set X using () renaming (_⊳_ to _⊳ˣ_)
      open G-Set Y using () renaming (_⊳_ to _⊳ʸ_)

  record G-Set-Morphism (G : Group ℓ) (X Y : G-Set G) : Set (suc ℓ) where
    field
      u : ∣ X ∣ → ∣ Y ∣ -- u for underlying
      equivariance : IsEquivariant X Y u