# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556327440 -32400
# Node ID e4986625ddd73957f7dec04075c513ac9bb8e897
# Parent  9b8ee2ddd92d770fbefceb19f8e2243226d74c44
add <= and <,>

diff -r 9b8ee2ddd92d -r e4986625ddd7 CCChom.agda
--- a/CCChom.agda	Sat Apr 27 08:42:45 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 10:10:40 2019 +0900
@@ -606,8 +606,8 @@
       π : {a b : Objs G } → Arrow G ( a ∧ b ) a
       π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
       ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
-   --   <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
-   --   _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
+      <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
+      _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
 
    record SM  : Set (suc Level.zero)  where
       field
@@ -637,6 +637,8 @@
    amap {G} {.(b ∧ _)} {b} π ( x , _) = x
    amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x
    amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x
+   amap {G} {a} {.(_ ∧ _)} < f , g > x = (amap f x , amap g x)
+   amap {G} {a} {.(_ <= _)} (f *) x = λ y → amap f ( x , y )
    fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
    fmap {G} {a} {a} (id a) = λ z → z
    fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
@@ -648,6 +650,24 @@
        _++_ = Category._o_ (DX G)
        ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
        distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
+       distr {a} {b} {e ∧ e1} {f} {next {b} {d} {e ∧ e1} < x , y > g} z = begin
+            fmap (next < x , y > g ++ f) z
+          ≡⟨⟩
+             amap x (fmap (g ++ f) z) , amap y (fmap (g ++ f) z)
+          ≡⟨  cong ( λ k → ( amap x k , amap y k )) (distr {a} {b} {d} {f} {g} z) ⟩
+             amap x (fmap g (fmap f z)) , amap y (fmap g (fmap f z))
+          ≡⟨⟩
+            fmap (next < x , y > g) (fmap f z)
+          ∎  where open ≡-Reasoning
+       distr {a} {b} {c <= d} {f} {next {b} {e} {c <= d} (x *) g} z = begin
+             fmap (next (x *) g ++ f) z
+          ≡⟨⟩
+             (λ y → amap x (fmap (g ++ f) z , y) )
+          ≡⟨  extensionality Sets ( λ y →  cong ( λ k →  (amap x (k , y )) ) (distr {a} {b} {e} {f} {g} z) ) ⟩
+             (λ y → amap x (fmap g (fmap f z) , y))
+          ≡⟨⟩
+             fmap (next (x *) g) (fmap f z)
+          ∎  where open ≡-Reasoning
        distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z =  begin
              fmap (DX G [ next π g o f ]) z
           ≡⟨⟩
@@ -715,8 +735,3 @@
        IsFunctor.≈-cong isf refl = refl
        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
-   <_,_> : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) c a → Arrow (graph G) c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) )
-   <_,_> {G} {a} {b} {c}   f  g  = λ z → ( (FMap (CS G) ( next f (id c)))  z , FMap (CS G) (next g (id c)) z )
-
-   _* : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) (c ∧ b ) a →  Hom Sets (FObj (CS G) c)  (FObj (CS G) ( a <= b ))
-   _* {G} {a} {b} {c} f  = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y )