--- a/Symmetric.agda	Thu Aug 20 00:26:38 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 09:07:54 2020 +0900
@@ -78,7 +78,7 @@
 open import  Relation.Binary.Core
 open import fin
 
--- An inductive definition of permutation
+-- An inductive construction of permutation
 
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
 pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
@@ -167,3 +167,24 @@
     plist1  (suc i) (s≤s lt) = toℕ (  perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1  i (<-trans lt a<sa) 
 
 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
+
+NL : (n : ℕ ) → Set
+NL 0 = ℕ
+NL (suc n) = List ( NL n )
+
+pls : (n : ℕ ) → List (List ℕ )
+pls n = pls1 n n lem0 where
+   lem0 : {n : ℕ } → n ≤ n
+   lem0 {zero} = z≤n
+   lem0 {suc n} = s≤s lem0
+   lem1 : {i n : ℕ } → i ≤ n → i < suc n
+   lem1 z≤n = s≤s z≤n
+   lem1 (s≤s lt) = s≤s (lem1 lt)
+   lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
+   lem2 i≤n = ≤-trans i≤n ( refl-≤s )
+   pls2 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation (suc n) (suc n)
+   pls2 0 n i≤<n = pid 
+   pls2 (suc i) (suc n) (s≤s i≤n) = eperm {suc n} {i} (lem1 i≤n) ( pls2 i n i≤n)
+   pls1 : ( i n : ℕ ) → i ≤ n  → List (List ℕ)
+   pls1 0 n _ = []
+   pls1 (suc i) n (s≤s i≤n) = plist ( pls2 i n (lem2 i≤n)) ∷ pls1 i n (lem2 i≤n)