# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598496298 -32400
# Node ID c68956f6c3ad7dddb94c93136c28b5bd20b6b975
# Parent  c5329963c583bd4798a2c50090a18067ca75ba7d
tc fix

diff -r c5329963c583 -r c68956f6c3ad Gutil.agda
--- a/Gutil.agda	Thu Aug 27 08:29:56 2020 +0900
+++ b/Gutil.agda	Thu Aug 27 11:44:58 2020 +0900
@@ -102,6 +102,12 @@
        mpf p (mpf q (mpf r ε))
     ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+grepl : { x y0 y1 z  : Carrier } → x ∙ y0 ≈ y1  → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z 
+grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )
+
+grm : { x y0 y1 z  : Carrier } → x ∙ y0 ≈ ε  → x ∙ ( y0 ∙ z ) ≈  z 
+grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ )
+
 -- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m
 -- ∙-flattenl (am x) = gsym (proj₂ identity _)
 -- ∙-flattenl (q o am x) with ∙-flattenl q    -- x₁ ∙ x ≈ mpl q (am x o am ε) ,  t : x₁ ≈ mpl q (am ε)
diff -r c5329963c583 -r c68956f6c3ad Putil.agda
--- a/Putil.agda	Thu Aug 27 08:29:56 2020 +0900
+++ b/Putil.agda	Thu Aug 27 11:44:58 2020 +0900
@@ -210,28 +210,47 @@
           pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
           pleq2 = headeq eq
 
-pprep-cong : {n  : ℕ} → (x y : Permutation n n ) → x =p= y → pprep x =p= pprep y
-pprep-cong {n} x y x=y = {!!} where
-    pprep-cong02 : (x : Permutation 1 1 ) →  (q : Fin 1) → (x ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-    pprep-cong02 x zero with x ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ x) zero
-    ... | zero | record { eq = e } = refl
-    pprep-cong01 : (x : Permutation 1 1 ) → x =p= pid
-    pprep-cong01 x = record { peq = pprep-cong02 x  }
-    pprep-cong0 : (n  : ℕ) → (x : Permutation (suc n) (suc n) ) → toℕ (x ⟨$⟩ʳ fromℕ< a<sa ) ≡ n
-    pprep-cong0 zero x = begin
-        toℕ (x ⟨$⟩ʳ fromℕ< a<sa)
-       ≡⟨⟩ 
-        toℕ (x ⟨$⟩ʳ zero)
-       ≡⟨ cong (λ k → toℕ k) (pprep-cong02 x zero) ⟩ 
-        toℕ {suc zero} zero
-       ≡⟨⟩ 
-        zero
-       ∎ where open ≡-Reasoning
-    pprep-cong0 (suc n) x = {!!}
-    t1 = plist0 (pprep (pid {3}))
-    pprep-cong1 : (n  : ℕ) → (x : Permutation n n ) → plist0 (pprep x) ≡ n ∷ plist0 x
-    pprep-cong1 zero x = refl
-    pprep-cong1 (suc n)  x = {!!}
+pprep-cong : {n  : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y
+pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where
+   pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q)
+   pprep-cong1 zero = refl
+   pprep-cong1 (suc q) = begin
+          pprep x ⟨$⟩ʳ suc q
+        ≡⟨⟩
+          suc ( x ⟨$⟩ʳ q )
+        ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩
+          suc ( y ⟨$⟩ʳ q )
+        ≡⟨⟩
+          pprep y ⟨$⟩ʳ suc q
+        ∎  where open ≡-Reasoning
+
+pprep-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y)
+pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where
+   pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q)
+   pprep-dist1 zero = refl
+   pprep-dist1 (suc q) =  cong ( λ k → suc k ) refl
+
+pswap-cong : {n  : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y
+pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where
+   pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q)
+   pswap-cong1 zero = refl
+   pswap-cong1 (suc zero) = refl
+   pswap-cong1 (suc (suc q)) = begin
+          pswap x ⟨$⟩ʳ suc (suc q)
+        ≡⟨⟩
+          suc (suc (x ⟨$⟩ʳ q))
+        ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩
+          suc (suc (y ⟨$⟩ʳ q))
+        ≡⟨⟩
+          pswap y ⟨$⟩ʳ suc (suc q)
+        ∎  where open ≡-Reasoning
+ 
+pswap-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y)
+pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where
+   pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q)
+   pswap-dist1 zero = refl
+   pswap-dist1 (suc zero) = refl
+   pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
 data  FL : (n : ℕ )→ Set where
    f0 :  FL 0 
diff -r c5329963c583 -r c68956f6c3ad Symmetric.agda
--- a/Symmetric.agda	Thu Aug 27 08:29:56 2020 +0900
+++ b/Symmetric.agda	Thu Aug 27 11:44:58 2020 +0900
@@ -54,6 +54,20 @@
        y ⟨$⟩ˡ q
    ∎ where open ≡-Reasoning
 
+presp : { p : ℕ } {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
+presp {p} {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
+   lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
+   lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
+passoc : { p : ℕ } (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
+passoc x y z = record { peq = λ q → refl }
+p-inv : { p : ℕ } {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
+p-inv {p} {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
+   ∎ where open ≡-Reasoning
+
 Symmetric : ℕ → Group  Level.zero Level.zero
 Symmetric p = record {
       Carrier        = Permutation p p
@@ -69,18 +83,5 @@
        ; inverse   = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))  
        ; ⁻¹-cong   = λ i=j → record { peq = λ q → p-inv i=j q }
       }
-   } where
-       presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
-       presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
-           lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
-           lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
-       passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
-       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
-           ∎ where open ≡-Reasoning
+   } 
 
diff -r c5329963c583 -r c68956f6c3ad sym5.agda
--- a/sym5.agda	Thu Aug 27 08:29:56 2020 +0900
+++ b/sym5.agda	Thu Aug 27 11:44:58 2020 +0900
@@ -70,62 +70,41 @@
      abc→dba : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
      abc→dba i<3 j<4 = lemma where
        open EqReasoning (Algebra.Group.setoid (Symmetric 5))
-       lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
-       lemma = begin
-          abc i<3 j<4 ∘ₚ abc i<3 j<4 
-         ≈⟨ prefl ⟩
-          ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ
-             ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ))
-         ≈⟨ {!!} ⟩
-          (((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ (flip (save2 i<3 j<4 ))) ∘ₚ
-             (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
-         ≈⟨ {!!} ⟩
-          (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )
-         ≈⟨ {!!} ⟩
-          (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
-         ≈⟨ prefl ⟩
-          dba i<3 j<4
-         ∎
+       S = Symmetric 5
+       open Group (Symmetric 5)
+       postulate lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
+       -- some kind of functional extentionaly required?
+       -- lemma = begin
+       --    abc i<3 j<4 ∘ₚ abc i<3 j<4 
+       --   ≈⟨ prefl ⟩
+       --    ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ
+       --       ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ))
+       --   ≈⟨  ∙-flatten (Symmetric 5) (((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am (flip (save2 i<3 j<4 ))) o 
+       --       ((am (save2 i<3 j<4) o am (pprep (pprep 3rot))) o am ( flip (save2 i<3 j<4 )))) ⟩
+       --       save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ (
+       --         save2 i<3 j<4  ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid  )))))
+       --   ≈⟨ ∙-cong prefl ( ∙-cong prefl (grm S (proj₁ inverse _))) ⟩
+       --       save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ (pprep (pprep 3rot) ∘ₚ (flip (save2 i<3 j<4 ) ∘ₚ pid  )))
+       --   ≈⟨ ∙-cong prefl (grepl S (pprep-cong prefl ) ) ⟩
+       --    (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
+       --   ≈⟨ prefl ⟩
+       --    dba i<3 j<4
+       --   ∎
 
-     dba→aec : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p=  aec i<3 j<4 
-     dba→aec = {!!}
+     postulate  -- someday
+        dba→aec : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p=  aec i<3 j<4 
+        aec→abc : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p=  abc i<3 j<4 
 
-     aec→abc : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p=  abc i<3 j<4 
-     aec→abc = {!!}
-
-     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where
+     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
        field 
          dba0<3 : Fin 4
          dba1<4 : Fin 5
          aec0<3 : Fin 4
          aec1<4 : Fin 5
-         abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
-
-     dba= :
-         {a a' : ℕ }  → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) →
-         {b b' : ℕ }  → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) →
-         {c c' : ℕ }  → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) →
-         abc a<3 a<4 =p= [ dba b<3 b<4  , aec c<3 c<4 ] →
-         dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ]
-     dba= a<3 a<4 b<3 b<4 c<3 c<4 dq = {!!} where
-         open EqReasoning (Algebra.Group.setoid (Symmetric 5))
-         lemma1 : dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ]
-         lemma1 = begin
-               dba a<3 a<4
-             ≈⟨ {!!} ⟩
-               [ aec b<3 b<4  , abc c<3 c<4 ]
-             ∎
-
-     aec= :
-         {a a' : ℕ }  → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) →
-         {b b' : ℕ }  → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) →
-         {c c' : ℕ }  → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) →
-         dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ] →
-         aec a<3 a<4 =p= [ abc b<3 b<4  , dba c<3 c<4 ] 
-     aec= = {!!}
+         abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , ins2 (pinv rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
 
      open Triple
-     triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4
+     triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
      triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
      triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
      triple z≤n (s≤s (s≤s z≤n)) =                   record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
@@ -148,21 +127,44 @@
      triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = 
                                                     record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }  
 
+     dba-triple : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → Triple i<3 j<4 (3rot  ∘ₚ 3rot )
+     dba-triple = ?
+
+     aec-triple : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot ) 
+     aec-triple = ?
+
 
      dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
           → deriving n (abc i<3 j<4 ) ∧ deriving n (dba i<3 j<4 ) ∧ deriving n (aec i<3 j<4 )
      dervie-any-3rot 0 i<3 j<4 = ⟪ lift tt , ⟪ lift tt , lift tt ⟫ ⟫
-     dervie-any-3rot (suc i) i<3 j<4 =  {!!}
-     --    ccong {deriving i} ( abc= (triple  i<3 j<4 ) ) (
-     --    comm {deriving i} {dba} {aec} 
-     --         ( dervie-any-3rot i (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4 tc}) ) 
-     --         ( dervie-any-3rot i (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4 tc}) )) where
-     --             tc : Triple i<3 j<4
-     --             tc = triple i<3 j<4
-     --             dba : Permutation 5 5
-     --             dba = abc (fin<n {3} {dba0<3 tc}) (fin<n {4} {dba1<4   tc})
-     --             aec : Permutation 5 5
-     --             aec = abc (fin<n {3} {aec0<3 tc}) (fin<n {4} {aec1<4   tc})
+     dervie-any-3rot (suc i) i<3 j<4 =  ⟪ d0 , ⟪ d1 , d2 ⟫ ⟫ where
+        tc : Triple i<3 j<4 3rot
+        tc = triple i<3 j<4
+        abc0 =  abc i<3 j<4
+        b<3 = fin≤n {3} (dba0<3 tc)
+        b<4 = fin≤n {4} (dba1<4 tc)
+        dba0 =  dba b<3 b<4
+        c<3 = fin≤n {3} (aec0<3 tc)
+        c<4 = fin≤n {4} (aec1<4 tc)
+        aec0 =  aec c<3 c<4
+        d0 : deriving (suc i) (abc i<3 j<4)
+        d0 = 
+         ccong {deriving i} ( psym (abc= tc )) (
+          comm {deriving i} {dba0} {aec0}
+              (proj1 (proj2 ( dervie-any-3rot i  b<3 b<4)))
+              (proj2 (proj2 ( dervie-any-3rot i  c<3 c<4 ))))
+        d1 : deriving (suc i) (dba i<3 j<4)
+        d1 = 
+         ccong {deriving i} ( psym {!!}) (   -- dba i<3 j<4 =p= [ aec0 , abc0 ]   --    dba= : dba b<3 b<4 =p= [ aec0 , abc0 ]  is not enough...
+          comm {deriving i} {aec0} {abc0}
+              (proj2 (proj2 ( dervie-any-3rot i  c<3 c<4 )))
+              (proj1 ( dervie-any-3rot i  i<3 j<4 )))
+        d2 : deriving (suc i) (aec i<3 j<4)
+        d2 = 
+         ccong {deriving i} ( psym {!!}) (
+          comm {deriving i} {abc0} {dba0}
+              (proj1 ( dervie-any-3rot i  i<3 j<4 ))
+              (proj1 (proj2 ( dervie-any-3rot i  b<3 b<4 ) )))
 
      open _=p=_
      counter-example :  ¬ (abc 0<3 0<4  =p= pid )