Permutation relation in Agda. In the indiuctive definition we have insertions on both sides, as opposed to one side. This makes the transitivity proof *horrible* (or at least I couldn't do better).

Perm.agda

open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Data.Sum

data _▶_≡_ {A : Set}(x : A) : List A → List A → Set where
  here  : ∀ {xs} → x ▶ xs ≡ (x ∷ xs)
  there : ∀ {y xs ys} → x ▶ xs ≡ ys → x ▶ (y ∷ xs) ≡ (y ∷ ys)

data Perm {A : Set} (xs : List A) : List A → Set where
  refl : Perm xs xs
  ins  : ∀ {x ys xs' ys'} → Perm xs' ys' → x ▶ xs' ≡ xs → x ▶ ys' ≡ ys → Perm xs ys

▶-inv : 
  ∀ {A}{a : A}{b as bs cs} 
  → a ▶ as ≡ cs
  → b ▶ bs ≡ cs 
  → (a ≡ b × as ≡ bs) ⊎ (∃ λ ds → b ▶ ds ≡ as × a ▶ ds ≡ bs)
▶-inv here here = inj₁ (refl , refl)
▶-inv here (there p2) = inj₂ (_ , p2 , here)
▶-inv (there p1) here = inj₂ (_ , here , p1)
▶-inv (there p1) (there p2) with ▶-inv p1 p2
... | inj₁ (refl , refl) = inj₁ (refl , refl)
... | inj₂ (ds , ias , ibs) = inj₂ (_ ∷ ds , there ias , there ibs)

▶-exch : 
  ∀ {A}{x : A}{y xs xxs yxxs} 
  → x ▶ xs ≡ xxs → y ▶ xxs ≡ yxxs → ∃ λ yxs → (y ▶ xs ≡ yxs) × (x ▶ yxs ≡ yxxs)
▶-exch p1 here = _ , here , there p1
▶-exch here (there p2) = _ , p2 , here
▶-exch (there p1) (there p2) with ▶-exch p1 p2
... | _ , p1' , p2' = _ , there p1' , there p2'

l1 : ∀ {A x xs xys} → Perm {A} (x ∷ xs) xys → ∃ λ ys → x ▶ ys ≡ xys × Perm xs ys
l1 refl = _ , here , refl
l1 (ins p here iys) = _ , iys , p
l1 (ins p (there ixs) iys) with l1 p
l1 {x = x}(ins {x = y}p (there ixs) iys) | ys , i , perm with ▶-exch i iys
l1 (ins p (there ixs) iys) | ys , i , perm | proj₁ , proj₂ , proj₃ 
  = proj₁ , proj₃ , ins perm ixs proj₂

▶-len : ∀ {A}{x : A}{xs ys} → x ▶ xs ≡ ys → suc (length xs) ≡ length ys
▶-len here = refl
▶-len (there p) rewrite ▶-len p = refl

extract-perm : 
  ∀ {A x xs xys xxs} 
  → (l : ℕ) 
  → length xxs ≡ l 
  → x ▶ xs ≡ xxs 
  → Perm {A} xxs xys 
  → ∃ λ ys → (x ▶ ys ≡ xys) × (Perm xs ys)
extract-perm zero () here p2
extract-perm zero () (there p1) p2
extract-perm (suc l) lp here refl = _ , here , refl
extract-perm (suc l) lp here (ins p2 here iys) = _ , iys , p2
extract-perm (suc l) lp here (ins p2 (there ixs) iys) with l1 p2 
... | proj₁ , proj₂ , proj₃ with ▶-exch proj₂ iys 
extract-perm (suc l) lp here (ins p2 (there ixs) iys) | proj₁ , proj₂ , proj₆ | proj₃ , proj₄ , proj₅ 
  = proj₃ , proj₅ , ins proj₆ ixs proj₄
extract-perm (suc l) lp (there p1) refl = _ , there p1 , refl
extract-perm (suc l) lp (there p1) (ins p2 here iys) with extract-perm l (cong pred lp) p1 p2
extract-perm (suc l) lp (there p1) (ins p2 here iys) | proj₁ , proj₂ , proj₃ with ▶-exch proj₂ iys
extract-perm (suc l) lp (there p1) (ins p2 here iys) | proj₁ , proj₂ , proj₆ | proj₃ , proj₄ , proj₅ 
  = proj₃ , proj₅ , ins proj₆ here proj₄
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) with ▶-inv p1 ixs
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) | inj₁ (refl , refl) = _ , iys , p2
extract-perm (suc l) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₁ , proj₂ , proj₃) with l1 p2
extract-perm (suc zero) lp (there {y} {xs₁} {[]} p1) (ins p2 (there ()) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃
extract-perm (suc zero) () (there {y} {xs₁} {x₁ ∷ ys} p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₅ , proj₆) | proj₁ , proj₂ , proj₃ with extract-perm l (cong pred $ trans (▶-len ixs) (cong pred lp)) proj₆ proj₃
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₄ , proj₉ , proj₆) | proj₁ , proj₈ , proj₃ | proj₂ , proj₅ , proj₇ with ▶-exch proj₅ proj₈
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₉ , proj₁₂ , proj₁₀) | proj₁ , proj₈ , proj₇ | proj₂ , proj₅ , proj₁₁ | proj₃ , proj₄ , proj₆ with ▶-exch proj₆ iys 
extract-perm (suc (suc l)) lp (there p1) (ins p2 (there ixs) iys) | inj₂ (proj₁₂ , proj₁₅ , proj₁₃) | proj₅ , proj₉ , proj₁₁ | proj₇ , proj₈ , proj₁₄ | proj₃ , proj₁₀ , proj₆ | proj₁ , proj₂ , proj₄ = proj₁ , proj₄ , ins (ins proj₁₄ here proj₁₀) (there proj₁₅) proj₂

perm-sym : ∀ {A xs ys} → Perm {A} xs ys → Perm ys xs
perm-sym refl = refl
perm-sym (ins p ix iy) = ins (perm-sym p) iy ix

perm-trans : ∀ {A xs ys zs} → Perm {A} xs ys → Perm ys zs → Perm xs zs
perm-trans refl p2 = p2
perm-trans p1 refl = p1
perm-trans {ys = ys} (ins xy ix iy) p2 with extract-perm (length ys) refl iy p2
perm-trans (ins xy ix iy) p2 | proj₁ , proj₂ , proj₃ = ins (perm-trans xy proj₃) ix proj₂