# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597658300 -32400
# Node ID bf12f26bacc3348254d4571e468f98174d0a7ab5
# Parent  b45ebc91a8d161b707bee2a97d1a204a75df40fe
...

diff -r b45ebc91a8d1 -r bf12f26bacc3 Gutil.agda
--- a/Gutil.agda	Mon Aug 17 15:24:58 2020 +0900
+++ b/Gutil.agda	Mon Aug 17 18:58:20 2020 +0900
@@ -49,11 +49,35 @@
     _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )
 
 mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
-mpf {x} (am x) y = x ∙ y
+mpf (am x) y = x ∙ y
 mpf (m o m₁) y = mpf m ( mpf m₁ y )
 
 mp-flatten : {x : Carrier } → (m : MP x ) → Carrier 
-mp-flatten {x} m = mpf {x} m ε 
+mp-flatten  m = mpf m ε 
+
+mpl1 : Carrier → {x : Carrier } → MP x → Carrier
+mpl1 x (am y) = x ∙ y
+mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1
+
+mpl : {x z : Carrier } → MP x → MP z  → Carrier
+mpl (am x)  m = mpl1 x m 
+mpl (m o m1) m2 = mpl m (m1 o m2)
+
+mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier
+mp-flattenl m = mpl m (am ε)
+
+test1 : ( f g : Carrier ) → Carrier
+test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) 
+
+test2 : ( f g : Carrier ) → test1 f g ≡  g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙  (f ∙ g) ⁻¹  ∙ ε
+test2 f g = _≡_.refl
+
+test3 : ( f g : Carrier ) → Carrier
+test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) 
+
+test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))
+test4 f g = _≡_.refl
+
   
 ∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
 ∙-flatten {x} (am x) = gsym (proj₂ identity _)
@@ -66,8 +90,7 @@
    mp-assoc (am x) = assoc _ _ _ 
    mp-assoc {p} {q} {r} (P o P₁) = begin
        mpf P (mpf  P₁ q) ∙ r      ≈⟨ mp-assoc P ⟩
-       mpf P (mpf P₁ q ∙ r)       ≈⟨ mp-cong P (mp-assoc P₁)  ⟩
-       mpf P ((mpf  P₁) (q ∙ r))
+       mpf P (mpf P₁ q ∙ r)       ≈⟨ mp-cong P (mp-assoc P₁)  ⟩ mpf P ((mpf  P₁) (q ∙ r))
     ∎ where open EqReasoning (Algebra.Group.setoid G)
    lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε →  x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
    lemma9 x y z t s = begin
@@ -79,6 +102,13 @@
        mpf p (mpf q (mpf r ε))
     ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+-- ∙-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 ε)
+-- ... | t = {!!}
+-- ∙-flattenl (q o (x o y )) with ∙-flattenl q 
+-- ... | t = gtrans (gsym (assoc _ _ _ )) {!!}
+
 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
 lemma5 f g = begin
      g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩