--- a/Putil.agda	Thu Aug 27 08:29:56 2020 +0900
+++ b/Putil.agda	Thu Aug 27 11:44:58 2020 +0900
@@ -210,28 +210,47 @@
           pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
           pleq2 = headeq eq
 
-pprep-cong : {n  : ℕ} → (x y : Permutation n n ) → x =p= y → pprep x =p= pprep y
-pprep-cong {n} x y x=y = {!!} where
-    pprep-cong02 : (x : Permutation 1 1 ) →  (q : Fin 1) → (x ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-    pprep-cong02 x zero with x ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ x) zero
-    ... | zero | record { eq = e } = refl
-    pprep-cong01 : (x : Permutation 1 1 ) → x =p= pid
-    pprep-cong01 x = record { peq = pprep-cong02 x  }
-    pprep-cong0 : (n  : ℕ) → (x : Permutation (suc n) (suc n) ) → toℕ (x ⟨$⟩ʳ fromℕ< a<sa ) ≡ n
-    pprep-cong0 zero x = begin
-        toℕ (x ⟨$⟩ʳ fromℕ< a<sa)
-       ≡⟨⟩ 
-        toℕ (x ⟨$⟩ʳ zero)
-       ≡⟨ cong (λ k → toℕ k) (pprep-cong02 x zero) ⟩ 
-        toℕ {suc zero} zero
-       ≡⟨⟩ 
-        zero
-       ∎ where open ≡-Reasoning
-    pprep-cong0 (suc n) x = {!!}
-    t1 = plist0 (pprep (pid {3}))
-    pprep-cong1 : (n  : ℕ) → (x : Permutation n n ) → plist0 (pprep x) ≡ n ∷ plist0 x
-    pprep-cong1 zero x = refl
-    pprep-cong1 (suc n)  x = {!!}
+pprep-cong : {n  : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y
+pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where
+   pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q)
+   pprep-cong1 zero = refl
+   pprep-cong1 (suc q) = begin
+          pprep x ⟨$⟩ʳ suc q
+        ≡⟨⟩
+          suc ( x ⟨$⟩ʳ q )
+        ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩
+          suc ( y ⟨$⟩ʳ q )
+        ≡⟨⟩
+          pprep y ⟨$⟩ʳ suc q
+        ∎  where open ≡-Reasoning
+
+pprep-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y)
+pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where
+   pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q)
+   pprep-dist1 zero = refl
+   pprep-dist1 (suc q) =  cong ( λ k → suc k ) refl
+
+pswap-cong : {n  : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y
+pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where
+   pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q)
+   pswap-cong1 zero = refl
+   pswap-cong1 (suc zero) = refl
+   pswap-cong1 (suc (suc q)) = begin
+          pswap x ⟨$⟩ʳ suc (suc q)
+        ≡⟨⟩
+          suc (suc (x ⟨$⟩ʳ q))
+        ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩
+          suc (suc (y ⟨$⟩ʳ q))
+        ≡⟨⟩
+          pswap y ⟨$⟩ʳ suc (suc q)
+        ∎  where open ≡-Reasoning
+ 
+pswap-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y)
+pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where
+   pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q)
+   pswap-dist1 zero = refl
+   pswap-dist1 (suc zero) = refl
+   pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
 data  FL : (n : ℕ )→ Set where
    f0 :  FL 0