--- a/PermGroup.agda	Sun Aug 16 16:03:23 2020 +0900
+++ b/PermGroup.agda	Sun Aug 16 19:50:43 2020 +0900
@@ -1,4 +1,4 @@
-module PermAbel where
+module PermGroup where
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -53,8 +53,8 @@
 ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
 peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
 
-pgroup : ℕ → Group  Level.zero Level.zero
-pgroup p = record {
+Pgroup : ℕ → Group  Level.zero Level.zero
+Pgroup p = record {
       Carrier        = Permutation p p
     ; _≈_            = _=p=_
     ; _∙_            = _∘ₚ_
@@ -77,13 +77,10 @@
        passoc x y z = record { peq = λ q → refl }
        p-inv : {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
        p-inv {i} {j} i=j q = begin
-              i ⟨$⟩ˡ q
-           ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
-              i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q ))
-           ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
-              i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q ))
-           ≡⟨ inverseˡ i  ⟩
-              j ⟨$⟩ˡ q
+           i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
+           i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
+           i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
+           j ⟨$⟩ˡ q
            ∎ where open ≡-Reasoning