# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607393122 -32400
# Node ID feddff78bb24cf9a24e5cf8eebc162e12e075a29
# Parent  8c20b6710f1d028aeb4ac49b9fac0ad99a1ccf22
fpq

diff -r 8c20b6710f1d -r feddff78bb24 FLComm.agda
--- a/FLComm.agda	Tue Dec 08 10:45:01 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 11:05:22 2020 +0900
@@ -101,12 +101,12 @@
 CommFListN  (suc i) = CommFList (CommFListN i)
 
 -- all comm cobmbination in P and Q
-record AnyComm  (P Q : FList n) : Set where
+record AnyComm  (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where
    field
      commList : FList n
      commAny : (p q : FL n)
          → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
-         → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
+         → Any (fpq p q ≡_) commList
 
 -------------
 --    (p,q)   (p,qn) ....           (p,q0)
@@ -125,23 +125,21 @@
 ... | case1 eq = ⊥-elim ( neq eq )
 ... | case2 x = x
 
-open AnyComm -- q₂
-anyComm : (P Q : FList n) → AnyComm P Q
-anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
-anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
-anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
-anyComm (cons p P pr) (cons q Q qr) = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
-  fpq : (p q : FL n) → FL n
-  fpq p q = perm→FL [ FL→perm p , FL→perm q ]
+open AnyComm 
+anyComm : (P Q : FList n) → (fpq : (p q : FL n) → FL n)  → AnyComm P Q fpq
+anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () }
+anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () }
+anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () }
+anyComm (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
   commListP : (P1 : FList n) → FList n
-  commListP [] = commList (anyComm P Q)
+  commListP [] = commList (anyComm P Q fpq)
   commListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (commListP P1)
   commListQ : (Q1 : FList n) → FList n
   commListQ [] = commListP P
   commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1)
   anyc0n : (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr)
-    → Any (_≡_ (perm→FL [ FL→perm p₁ , FL→perm q₁ ])) (FLinsert (fpq p q) (commListQ Q))
-  anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q)
+    → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q))
+  anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q )
   anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where 
      anyc01 : (Q1 : FList n) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
      anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _
@@ -155,7 +153,7 @@
      anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1)
   anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where
      anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1)
-     anyc05 [] = commAny (anyComm P Q) p₁ q₁ anyp anyq
+     anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq
      anyc05 (cons a P1 x) = insAny _ (anyc05 P1)
      anyc04 : (Q1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
      anyc04 [] = anyc05 P