### changeset 808:e4cc2ccd0f06

...
author Shinji KONO Fri, 26 Apr 2019 19:50:27 +0900 91a2efb67462 0976d576f5f6 CCChom.agda 1 files changed, 5 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
```--- a/CCChom.agda	Fri Apr 26 18:24:07 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 19:50:27 2019 +0900
@@ -637,7 +637,9 @@
fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ z → smap G x ( k z ) where
k : fobj a → fobj {G} c
k z = fmap f z
-   fmap {G} {a} {b} (next (id b) f) = fmap f
+   fmap {G} {a} {b} (next (id b) f) = λ z → k z where
+       k : fobj a → fobj {G} b
+       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
@@ -648,9 +650,9 @@
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
k z = fmap f z
-   fmap {G} {a} {b} (next {.a} {c} (_・_ {c} {d} {b} f g) h) =  λ z → fmap ( next f (id d)) ( fmap (next g (id c )) ( fmap h 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 )
+   fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = {!!} -- λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )

CS : {G : SM } → Functor (DX G) (Sets {Level.zero})
FObj CS a  = fobj a```