--- a/PermAbel.agda	Sun Aug 16 11:32:13 2020 +0900
+++ b/PermAbel.agda	Sun Aug 16 13:50:07 2020 +0900
@@ -63,11 +63,18 @@
      ; 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-≡ x y refl refl = lemma2 where
+        lemma3 : {p : ℕ } {i j : Fin p} {x y : Permutation p p } → i ≡ j
+           → (eq1 : Inverse.to x Π.⟨$⟩ i ≡ Inverse.to x Π.⟨$⟩ j  ) 
+           → (eq2 : Inverse.to y Π.⟨$⟩ i ≡ Inverse.to y Π.⟨$⟩ j  ) → eq1 ≅ eq2 
+        lemma3 refl refl refl = ?
+        lemma4 : {p : ℕ } {i j : Fin p} {x y : Permutation p p } → i ≡ j → (p q : Inverse.from y Π.⟨$⟩ i ≡ Inverse.from y Π.⟨$⟩ j  ) → p ≡ q 
+        lemma4 refl refl refl = refl
+        lemma2 :  record { to = record   { _⟨$⟩_ = Π._⟨$⟩_ (Inverse.to y)   ; cong = {!!} } ;
+                           from = record { _⟨$⟩_ = Π._⟨$⟩_ (Inverse.from y) ; cong = {!!} } ; inverse-of = Inverse.Inverse.inverse-of x } ≡ y
+        lemma2 = {!!}
 
-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 {