index ∙ source

module Shuffle where

open import 1Lab.Prelude
open import Algebra.Group
open import Algebra.Group.Instances.Cyclic
open import Data.Fin
open import Data.Fin.Closure
open import Data.Int
open import Data.Nat
open import Data.Product.NAry
open import Data.Set.Coequaliser
open import Data.Vec.Base

n : Nat
n = 

module ℤ/n = Group-on ((ℤ/ n) .snd)

k : Fin (factorial n)
k = 

E : Fin (factorial n) → Fin n ≃ Fin n -- ([n] ≃ [n]) = [n!]
E = Equiv.from (Fin-permutations _)

path : ⌞ ℤ/ n ⌟ ≡ Fin n
path = ua $
  ⌞ ℤ/ n ⌟ ≃⟨ Finite-ℤ/n n ⟩
  Fin n    ≃⟨ E k ⟩
  Fin n    ≃∎

suc/n : ⌞ ℤ/ n ⌟ → ⌞ ℤ/ n ⌟
suc/n = ℤ/n._⋆ 

next : Fin n → Fin n
next = subst (λ X → X → X) path suc/n

_ : tabulate (lower ∘ next) ≡ [  ,  ,  ,  ,  ,  ]
_ = refl

postulate
  is-cycle : ∀ {X : Type} → (f : X → X) → Type
  suc-is-cycle : is-cycle suc/n -- follows from ℤ/n being generated by 1

next-is-cycle : is-cycle next
next-is-cycle = substd {A = λ i → path i → path i} is-cycle
  (transport-filler _ suc/n)
  suc-is-cycle