Mercurial > hg > Members > kono > Proof > category

changeset 905:47a0a9f2eee9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 01 May 2020 17:08:23 +0900
parents 3e164b00155f
children 91b8b7fb64eb
files CCCGraph.agda
diffstat 1 files changed, 19 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Fri May 01 11:10:34 2020 +0900
+++ b/CCCGraph.agda	Fri May 01 17:08:23 2020 +0900
@@ -209,37 +209,32 @@
 -- Functor from Positive Logic to Sets
 --
 
-   data SObj :  Set (c₁ ⊔ c₂ ⊔ ℓ)  
-   data SArrow : (a b : SObj) → Set (c₁ ⊔ c₂ ⊔ ℓ) 
-   data SObj where
-      satom : (vertex G) → SObj
-      stop : SObj
-      spair : SObj → SObj → SObj
-      sfunc : SObj → SObj → SObj
-   data SArrow where
-      seq : {a b : vertex G}  → graphtocat.Chain G a b → SArrow (satom a) (satom b)
-      top : {a  : SObj } → SArrow a stop
-      pair : {a b c : SObj } → SArrow a b → SArrow a c → SArrow a (spair b c )
-      func : {a b c : SObj } → SArrow b c → SArrow a (sfunc b c)
+   data SArrow : (a b : Objs) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
+      seq : {a b : vertex G}  → graphtocat.Chain G a b → SArrow (atom a) (atom b)
+      top : {a  : Objs } → SArrow a ⊤
+      pair : {a b c : Objs } → SArrow a b → SArrow a c → SArrow a (b ∧ c )
+      func : {a b c : Objs } → SArrow b c → SArrow a ( c <= b )
+      sid : {a : Objs } → SArrow a a 
 
-   sobj : Objs → SObj
-   sobj (atom x) = satom x
-   sobj ⊤ = stop
-   sobj (x ∧ y) = spair (sobj x) (sobj y)
-   sobj (b <= a) = sfunc (sobj a) (sobj b)
-
-   smap :  { a b : Objs  } → Hom PL a b → SArrow (sobj a) (sobj b)
-   samap :  { a b c : Objs  } → Arrow b c  → SArrow (sobj a) (sobj b) → SArrow (sobj a) (sobj c)
+   smap :  { a b : Objs  } → Hom PL a b → SArrow (a) (b)
+   samap :  { a b c : Objs  } → Arrow b c  → SArrow (a) (b) → SArrow (a) (c)
+   samap {atom a} (arrow x) sid  = {!!}
    samap {atom a} (arrow x) (seq y) = seq ( graphtocat.next x y )
    samap π (pair f g) = f
    samap π' (pair f g) = g
    samap ε (pair (func f) g) = {!!}
-   samap (f *) x = ?
+   samap (f *) x = func {!!} where
+      f1 : {!!}
+      f1 = smap f
+   samap ε (pair y y₁) = {!!}
+   samap π sid = ?
+   samap π' sid = ?
+   samap ε sid = ?
    smap (id (atom x)) = seq (graphtocat.id x)
    smap (id ⊤) = top
-   smap (id (a ∧ b)) = {!!} -- pair (smap (id a)) (smap (id b))
-   smap (id (b <= a)) = {!!}
-   smap (○ a) = top {sobj a}
+   smap (id (a ∧ b)) = sid -- pair (smap (id a)) (smap (id b))
+   smap (id (b <= a)) = sid 
+   smap (○ a) = top {a}
    smap < f , g > = pair ( smap f ) (smap g )
    smap (iv f g ) = samap f ( smap g )