--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/PermAbel.agda	Sun Aug 16 11:03:37 2020 +0900
@@ -0,0 +1,84 @@
+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 
+
+