--- a/CCChom.agda	Fri Apr 26 21:24:12 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 22:53:57 2019 +0900
@@ -635,11 +635,11 @@
        k : fobj a → fobj {G} c 
        k z = fmap f z
    fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next {a} {x ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
-       k : fobj a → fobj x /\ fobj y  
+   fmap {G} {a} {b} (next {a} {b ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
+       k : fobj a → fobj b /\ fobj y  
        k z = fmap f z
-   fmap {G} {a} {b} (next {.a} {x ∧ y} π' f) =  λ z → proj₂ ( k z ) where
-       k : fobj a → fobj x /\ fobj y  
+   fmap {G} {a} {b} (next {.a} {x ∧ b} π' f) =  λ z → proj₂ ( k z ) where
+       k : fobj a → fobj x /\ fobj b  
        k z = fmap f z
    fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (k z))(  proj₂ (k z)) where
        k :  fobj a →  (fobj y → fobj x) /\ fobj y
@@ -662,15 +662,51 @@
              Sets [ fmap (next x g) o fmap (Chain.id a) ]
           ∎  where open ≈-Reasoning Sets
        distrCS {a} {b} {b} {f} {id b} =  refl
-       distrCS {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} = {!!}
+       distrCS {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} = begin
+             fmap (DX G [ next (arrow x) g o f ])
+          ≈⟨⟩
+             fmap ( next (arrow x) (g ++ f ) )
+          ≈⟨⟩
+             ( λ y → smap G x ( fmap (g ++ f) y )  )
+          ≈⟨ extensionality Sets ( λ y → ( cong ( λ k → smap G x (k y) ) distrCS )) ⟩
+             (λ z → fmap (next (arrow x) g) ( fmap f z ))
+          ≈⟨⟩
+             (Sets [ fmap (next (arrow x) g) o fmap f ])
+          ∎  where open ≈-Reasoning Sets
        distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
              fmap (DX G [ next (○ a₁) g o f ])
-          ≈⟨ {!!} ⟩
+          ≈⟨⟩
              Sets [ fmap (next (○ a₁) g) o fmap f ]
           ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π g} = {!!}
-       distrCS {a} {b} {c} {f} {next π' g} = {!!}
-       distrCS {a} {b} {c} {f} {next ε g} = {!!}
+       distrCS {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} =  begin
+             fmap (DX G [ next π g o f ])
+          ≈⟨⟩
+             fmap (next π (g ++ f))
+          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl ))  ⟩
+             ( λ z → proj₁ (fmap (g ++ f) z))
+          ≈⟨ extensionality Sets ( λ z → cong ( λ k → proj₁ (k z)  ) distrCS )  ⟩
+             Sets [ fmap (next π g) o fmap f ]
+          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {c} {f} {next π' g} =   begin
+             fmap (DX G [ next π' g o f ])
+          ≈⟨⟩
+             fmap (next π' (g ++ f))
+          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl ))  ⟩
+             ( λ z → proj₂ (fmap (g ++ f) z))
+          ≈⟨ extensionality Sets ( λ z → cong ( λ k → proj₂ (k z)  ) distrCS )  ⟩
+             Sets [ fmap (next π' g) o fmap f ]
+          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {c} {f} {next ε g} =  begin
+             fmap (DX G [ next ε g o f ] )
+          ≈⟨⟩
+              fmap (next ε (g ++ f))
+          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl )) ⟩
+             ( λ z →  proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ))
+          ≈⟨  extensionality Sets ( λ z → cong ( λ k → proj₁ (k z) (  proj₂ (k z))  ) distrCS )    ⟩
+             ( λ x → fmap (next ε g) (fmap f x) )
+          ≈⟨⟩
+             Sets [ fmap (next ε g) o fmap f ]
+          ∎  where open ≈-Reasoning Sets
        isf : IsFunctor (DX G) Sets fobj fmap 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf refl = refl