{-# OPTIONS -WnoUnsupportedIndexedMatch #-}
module GpdCont.ActionContainer.Examples where

open import GpdCont.Prelude
open import GpdCont.ActionContainer.Base
open import GpdCont.Group.SymmetricGroup
open import GpdCont.GroupAction.Base using (Action ; _⁺_)
open import GpdCont.GroupAction.Integer using (ℤ ; 1ℤ ; ℤ-action)
open import GpdCont.Modulo
  using (Fin ; isSetFin ; suc-mod ; Modulo ; embed)
  renaming (shiftEquiv to sucEquiv)

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat

private
  ℕSet : hSet _
  ℕSet .fst = ℕ
  ℕSet .snd = isSetℕ

  FinSet : ℕ → hSet _
  FinSet n .fst = Fin n
  FinSet n .snd = isSetFin

  cycle : (n : ℕ) → Action ℤ (FinSet n)
  cycle n = ℤ-action $ the (Fin n ≃ Fin n) (sucEquiv n)

  -- The action of ℤ is freely generated by the equivalence sucEquivₙ : Fin n ≃ Fin n:
  _ : (n : ℕ) → (cycle n ⁺ 1ℤ) ≡ equivFun (sucEquiv n)
  _ = λ n → refl

  data isSuc : ℕ → Type where
    isSucSuc : ∀ {n} → isSuc (suc n)

  -- For n ≥ 1, sucEquivₙ is just successor function modulo n:
  _mod_ : (k : ℕ) (n : ℕ) {_ : isSuc n} → Fin n
  (k mod (suc n)) {isSucSuc {n}} = embed {suc n} k

  _ : ∀ {n} (k : ℕ) → equivFun (sucEquiv (suc n)) (embed k) ≡ (suc k) mod (suc n)
  _ = λ k → refl

CyclicList : ActionContainer ℓ-zero
CyclicList = mkActionContainer ℕSet FinSet (λ n → ℤ) cycle