# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556182590 -32400
# Node ID 979c0bf97a5a64b0b355dafc21bbabdcec388bec
# Parent  2716d2945730f045063209c6c36e0e580d2464e9
...

diff -r 2716d2945730 -r 979c0bf97a5a CCChom.agda
--- a/CCChom.agda	Thu Apr 25 12:22:03 2019 +0900
+++ b/CCChom.agda	Thu Apr 25 17:56:30 2019 +0900
@@ -619,26 +619,64 @@
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
+   fobj : {G : Graph} ( a  : Obj (DX G) ) → Set
+   fobj {G} (atom x) = vertex G
+   fobj (a ∧ b) = (fobj a ) /\ (fobj b )
+   fobj (a <= b) = fobj b → fobj a
+   fobj ⊤ = One'
+   {-# TERMINATING #-}
+   fmap : {G : Graph} { a b : Obj (DX G) } → Hom (DX G) a b → fobj a → fobj b
+   fmap {G} {a} {a} (id a) = id1 Sets (fobj a) where open ≈-Reasoning (Sets {Level.zero})
+   fmap {G} {a} {(atom b)} (next (arrow x) f) = λ _ → b
+   fmap {G} {a} {b} (next (id b) f) = fmap f
+   fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
+   fmap {G} {a} {b} (next π f) = λ z → proj₁ ( fmap f z )
+   fmap {G} {a} {b} (next π' f) =  λ z → proj₂ ( fmap f z )
+   fmap {G} {a} {b} (next ε f) =  λ z → (  proj₁ (fmap f z) )(  proj₂ (fmap f z) )
+   fmap {G} {a} {b} (next (f ・ g) h) = λ z →  fmap ( next f (next g h ) ) z
+   fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z ,  fmap (next g h) z)
+   fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
+
    CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
-   FObj (CS {G}) (atom x) = vertex G
-   FObj CS ⊤ = One'
-   FObj CS (a ∧ b) = (FObj CS a ) /\ (FObj CS b )
-   FObj CS (a <= b) = FObj CS b → FObj CS a
-   FMap CS {a} {a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
-   FMap CS {a} {(atom b)} (next (arrow x) f) = λ _ → b
-   FMap CS {a} {.a₁} (next (id a₁) f) = FMap CS f
-   FMap CS {a} {.⊤} (next (○ a₁) f) = λ _ → OneObj'
-   FMap CS {a} {b} (next π f) = λ z → proj₁ ( FMap CS f z )
-   FMap CS {a} {b} (next π' f) =  λ z → proj₂ ( FMap CS f z )
-   FMap CS {a} {b} (next ε f) =  λ z → (  proj₁ (FMap CS f z) )(  proj₂ (FMap CS f z) )
-   FMap CS {a} {.(_ ∧ _)} (next < f , g > h) = λ z → ( FMap CS (next f h) z ,  FMap CS (next g h) z)
-   FMap CS {a} {b} (next (f ・ g) h) = λ z →  FMap CS ( next f (next g h ) ) z
-   FMap CS {a} {(c <= b)} (next (e *) f) = {!!}
+   FObj CS a  = fobj a
+   FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
    isFunctor (CS {G}) = isf where
-       distrCS : {a b c : Obj (DX G)} { g : Hom (DX G) b c } { f : Hom (DX G) a b } → Sets [ FMap CS ((DX G) [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ]
-       distrCS = {!!}
-       isf : IsFunctor (DX G) Sets (FObj CS) ( FMap CS ) 
-       IsFunctor.identity isf = extensionality Sets ( λ x → {!!} )
-       IsFunctor.distr isf = distrCS
+       _++_ = Category._o_ (DX G)
+       distrCS : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → Sets [ fmap ((DX G) [ g o f ]) ≈ Sets [ fmap g o fmap f ] ]
+       distrCS {a} {.a} {.a} {id a} {id .a} = refl
+       distrCS {a} {.a} {c} {id a} {next x g} = begin
+             fmap (DX G [ next x g o Chain.id a ])
+          ≈⟨⟩
+             fmap ( next x ( g ++ (Chain.id a)))
+          ≈⟨ extensionality Sets ( λ y → cong ( λ k → fmap ( next x k ) y ) (idR1 (DX G)) ) ⟩
+             fmap ( next x  g )
+          ≈↑⟨ idL ⟩
+             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 _)} {f} {next (arrow x) g} = refl
+       distrCS {a} {b} {c} {f} {next (id c) g} = begin
+             fmap (DX G [ next (Arrow.id c) g o f ])
+          ≈⟨ {!!} ⟩
+             Sets [ fmap (next (Arrow.id c) g) o fmap f ]
+          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
+             fmap (DX G [ next (○ a₁) g o f ])
+          ≈⟨ extensionality Sets ( λ x → refl ) ⟩
+             Sets [ fmap (next (○ a₁) g) o fmap f ]
+          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {c} {f} {next π g} = {!!}
+       distrCS {a} {b} {c} {f} {next π' g} = {!!}
+       distrCS {a} {b} {c} {f} {next ε g} = {!!}
+       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = {!!}
+       distrCS {a} {b} {c} {f} {next (x ・ x₁) g} = extensionality Sets ( λ z → begin
+             fmap (DX G [ next (x ・ x₁) g o f ]) z
+          ≡⟨ {!!} ⟩
+             ( Sets [ fmap (next (x ・ x₁) g) o fmap f ]  ) z
+          ∎ ) where open ≡-Reasoning 
+       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
+       isf : IsFunctor (DX G) Sets fobj fmap 
+       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf refl = refl
+       IsFunctor.distr isf {a} {b} {c} {g} {f} = distrCS {a} {b} {c} {g} {f}