### changeset 816:4e48b331020a

simpler
author Shinji KONO Sat, 27 Apr 2019 12:58:12 +0900 bb9fd483f560 177162990879 CCChom.agda 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
```--- a/CCChom.agda	Sat Apr 27 12:17:49 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 12:58:12 2019 +0900
@@ -611,13 +611,13 @@

open Graph

-   data Objs (G : Graph ) : Set where
+   data Objs (G : Graph ) : Set where    -- formula
atom : (vertex G) → Objs G
⊤ : Objs G
_∧_ : Objs G → Objs G → Objs G
_<=_ : Objs G → Objs G → Objs G

-   data Arrow (G : Graph ) :  Objs G → Objs G → Set where
+   data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
○ : (a : Objs G ) → Arrow G a ⊤
π : {a b : Objs G } → Arrow G ( a ∧ b ) a
@@ -649,16 +649,16 @@
fobj {G} (a <= b) = fobj {G} b → fobj {G} a
fobj ⊤ = One'
amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
-   amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x
-   amap {G} {a} {.⊤} (○ a) _ = OneObj'
-   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 )
+   amap {G} (arrow x) = smap G x
+   amap (○ a) _ = OneObj'
+   amap π ( x , _) = x
+   amap π'( _ , x) = x
+   amap ε ( f , x ) = f x
+   amap < f , g > x = (amap f x , amap g x)
+   amap (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 ]
+   fmap {G} {a} (id a) = λ z → z
+   fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]

--   CS is a map from Positive logic to Sets
--    Sets is CCC, so we have a cartesian closed category generated by a graph```