open import Algebra.G-Set
open import Algebra.Group
open import Category.G-Sets
open import Categories.FreeObjects.Free
open import Categories.Functor.Core
open import Categories.Category.Instance.Sets
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Data.Product

-- The category G-Sets has free objects

module Category.G-Sets.Properties.FreeObject {ℓ} (G : Group ℓ) where
  open Group using () renaming (Carrier to ∣_∣)
  open G-Set using () renaming (X to ∣_∣)
  open G-Set-Morphism using () renaming (u to <_>)
  open FreeObject
  open Group G hiding (Carrier)

  forgetfulF : Functor (G-Sets G) (Sets ℓ)
  forgetfulF = record
                { F₀ = λ GS → ∣ GS ∣
                ; F₁ = λ f → < f >
                ; identity = ≡.refl
                ; homomorphism = ≡.refl
                ; F-resp-≈ = λ x → x
                }

  free-G-Set : ∀ {X : Set ℓ} → FreeObject forgetfulF X
  free-G-Set {X} .FX = record
    { X = ∣ G ∣ × X
    ; _⊳_ = λ g (h , x) → (g ∙ h , x)
    ; ε⊳ = λ {(g , x)} → ≡.cong (_, x) idˡ
    ; ∘⊳ = λ {g} {h} {(f , x)} → ≡.cong (_, x) assoc
    }
  free-G-Set .η x = (ε , x)
  free-G-Set {X} ._* {GS} f = record
    { u = λ (g , x) → g ⊳ f x
    ; equivariance = λ {g} {x} → ∘⊳
    }
    where open G-Set GS
  free-G-Set {X} .*-lift {GS} f {x} = ε⊳
    where open G-Set GS
  free-G-Set {X} .*-uniq {GS} f f' g-prop {(h , y)} = ≡.trans (≡.cong < f' > (≡.cong (_, y) (≡.sym idʳ)) )
                                                     (≡.trans (f'.equivariance)
                                                              (≡.cong (h ⊳_) g-prop))
    where
      open G-Set GS
      module f' = G-Set-Morphism f'