module PermAbel where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
open import Data.Fin
open import Data.Fin.Permutation
open import Function hiding (id ; flip)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.LeftInverse  using ( _LeftInverseOf_ )
open import Function.Equality using (Π)
open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality

f1 : Fin 3 → Fin 3
f1 zero = suc (suc zero)
f1 (suc zero) = zero
f1 (suc (suc zero)) = suc zero

lemma1  : Permutation 3 3
lemma1  = permutation f1 ( f1 ∘ f1 ) lemma2 where
   lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
   lemma3 zero = refl
   lemma3 (suc zero) = refl
   lemma3 (suc (suc zero)) = refl
   lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
   lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }

fid : {p : ℕ } → Fin p → Fin p
fid x = x

-- Data.Fin.Permutation.id
pid : {p : ℕ } → Permutation p p
pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }

-- Data.Fin.Permutation.flip
pinv : {p : ℕ } → Permutation p p → Permutation p p
pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

PPP0 : {p : ℕ } (P : Permutation p p ) (x : Fin p) →  (_⟨$⟩ˡ_ P) ((_⟨$⟩ʳ_ P) x) ≡ x
PPP0 P x =  inverseˡ P 

PPP1 : {p : ℕ } (P : Permutation p p ) (x : Fin p) →  (_⟨$⟩ʳ_ P) ((_⟨$⟩ˡ_ P) x) ≡ x
PPP1 P x = inverseʳ P

Pp :  {p : ℕ } → (P : Permutation p p ) → P ≡ permutation (_⟨$⟩ʳ_ P ) (_⟨$⟩ˡ_ P ) 
     record { left-inverse-of = λ x → PPP0 P x ; right-inverse-of = λ x → PPP1 P x } 
Pp P = {!!}

p-≅ : {p : ℕ } → {f0 g0 f1 g1 : Fin p → Fin p } → f0 ≡ f1 → g0 ≡ g1
   → {fg0 :  (x : Fin p ) → f0 (g0 x) ≡ x } → {fg1 : (x : Fin p ) → f1 (g1 x) ≡ x }
   → {gf0 :  (x : Fin p ) → g0 (f0 x) ≡ x } → {gf1 : (x : Fin p ) → g1 (f1 x) ≡ x }
   → fg0 ≅ fg1 → gf0 ≅ gf1 → permutation f0 g0 record {  left-inverse-of = gf0 ; right-inverse-of = fg0 }
                           ≡ permutation f1 g1 record {  left-inverse-of = gf1 ; right-inverse-of = fg1 }
p-≅ refl refl HE.refl HE.refl = refl

p-≡ : {p : ℕ } → (x y : Permutation p p ) → (_⟨$⟩ˡ_ x) ≡ (_⟨$⟩ˡ_ y) → (_⟨$⟩ʳ_ x ) ≡ (_⟨$⟩ʳ_ y ) → x ≡ y
p-≡ _ _ refl refl = {!!}

pgroup : ℕ → AbelianGroup  Level.zero Level.zero
pgroup p = record {
      Carrier        = Permutation p p
    ; _≈_            = _≡_
    ; _∙_            = _∘ₚ_
    ; ε              = pid
    ; _⁻¹            = pinv
    ; isAbelianGroup = record { isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record {refl = refl ; trans = trans ; sym = sym}
       ; ∙-cong = presp }
       ; assoc = passoc }
       ; identity = {!!} }
       ; inverse   = {!!}
       ; ⁻¹-cong   = {!!}
       } ; comm = {!!}
      }
   } where
       presp : {x y u v : Permutation p p } → x ≡ y → u ≡ v → (x ∘ₚ u) ≡ (y ∘ₚ v)
       presp refl refl = refl
       passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) ≡ (x ∘ₚ (y ∘ₚ z))
       passoc x y z = p-≡ _ _ refl refl