--- a/PermAbel.agda	Sun Aug 16 11:03:37 2020 +0900
+++ b/PermAbel.agda	Sun Aug 16 11:32:13 2020 +0900
@@ -45,10 +45,6 @@
 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 }
@@ -56,6 +52,20 @@
                            ≡ permutation f1 g1 record {  left-inverse-of = gf1 ; right-inverse-of = fg1 }
 p-≅ refl refl HE.refl HE.refl = refl
 
+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 → record { to = →-to-⟶ f0 ; from = →-to-⟶ g0 ; inverse-of = record {  left-inverse-of = gf0 ; right-inverse-of = fg0 } }
+                        ≡    record { to = →-to-⟶ f1 ; from = →-to-⟶ g1 ; inverse-of = record {  left-inverse-of = gf1 ; right-inverse-of = fg1 } }
+p-≅' refl refl HE.refl HE.refl = refl
+
+Pp :  {p : ℕ } → (P : Permutation p p ) → P ≡ record { to = →-to-⟶ (_⟨$⟩ʳ_ P ) ; from = →-to-⟶ (_⟨$⟩ˡ_ P ) 
+     ; inverse-of = record { left-inverse-of = λ x → inverseˡ P  ; right-inverse-of = λ x → inverseʳ P } }
+Pp P = {!!}
+
+lemma3 : {p : ℕ } {i j : Fin p} {y : Permutation p p } → i ≡ j → Inverse.to y Π.⟨$⟩ i ≡ Inverse.to y Π.⟨$⟩ j 
+lemma3 = {!!}
+
 p-≡ : {p : ℕ } → (x y : Permutation p p ) → (_⟨$⟩ˡ_ x) ≡ (_⟨$⟩ˡ_ y) → (_⟨$⟩ʳ_ x ) ≡ (_⟨$⟩ʳ_ y ) → x ≡ y
 p-≡ _ _ refl refl = {!!}