Rename transpose-self-inverse to transpose-comm

Author: Taneb

CHANGELOG.md

@@ -1866,7 +1866,7 @@ Other minor changes
 * Added new definitions and proofs in `Data.Fin.Permutation`:
   ```agda
   insert         : Fin (suc m) → Fin (suc n) → Permutation m n → Permutation (suc m) (suc n)
-  transpose-self-inverse : transpose i j ≈ transpose j i
+  transpose-comm : transpose i j ≈ transpose j i
   insert-punchIn : insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
   insert-remove  : insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
   remove-insert  : remove i (insert i j π) ≈ π

src/Data/Fin/Permutation.agda

@@ -223,8 +223,8 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 ------------------------------------------------------------------------
 -- Other properties
 
-transpose-self-inverse : ∀ (i j : Fin n) → transpose i j ≈ transpose j i
-transpose-self-inverse i j k with k ≟ i | k ≟ j
+transpose-comm : ∀ (i j : Fin n) → transpose i j ≈ transpose j i
+transpose-comm i j k with k ≟ i | k ≟ j
 ... | no ¬p | no ¬q = refl
 ... | no ¬p | yes q = refl
 ... | yes p | no ¬q = refl

src/Data/Fin/Permutation/Transposition/List.agda

@@ -93,6 +93,6 @@ eval-reverse (x@(a , b , _) ∷ xs) i = begin
   eval (L.reverse (x ∷ xs))            ⟨$⟩ʳ i ≡⟨ cong (λ p → eval p ⟨$⟩ʳ i) (L.unfold-reverse x xs) ⟩
   eval (L.reverse xs L.∷ʳ x)           ⟨$⟩ʳ i ≡⟨ eval-++ (L.reverse xs) L.[ x ] i ⟩
   eval (L.reverse xs) ∘ₚ transpose a b ⟨$⟩ʳ i ≡⟨ cong (transpose a b ⟨$⟩ʳ_) (eval-reverse xs i) ⟩
-  flip (eval xs) ∘ₚ transpose a b      ⟨$⟩ʳ i ≡⟨ transpose-self-inverse a b (flip (eval xs) ⟨$⟩ʳ i) ⟩
+  flip (eval xs) ∘ₚ transpose a b      ⟨$⟩ʳ i ≡⟨ transpose-comm a b (flip (eval xs) ⟨$⟩ʳ i) ⟩
   flip (eval xs) ∘ₚ transpose b a      ⟨$⟩ʳ i ∎