Mercurial > hg > Members > kono > Proof > category

changeset 904:3e164b00155f

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 11:10:34 +0900
parents 2f0ffd5733a8
children 47a0a9f2eee9
files CCCGraph.agda
diffstat 1 files changed, 35 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Thu Apr 30 17:42:12 2020 +0900
+++ b/CCCGraph.agda	Fri May 01 11:10:34 2020 +0900
@@ -203,16 +203,49 @@
               o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ i} f=g (piv h=i) = piv ( o-resp-≈ f=g  h=i)
               o-resp-≈ {_} {_} {_} {f} {g} {iv (arrow x) h} {iv (arrow y) i} f=g (aiv x=y h=i) = aiv x=y (o-resp-≈ f=g  h=i)
 
+
 --------
 --
 -- 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)
+
+   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)
+   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 = ?
+   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 < f , g > = pair ( smap f ) (smap g )
+   smap (iv f g ) = samap f ( smap g )
+
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   open import Data.List
-
    C = graphtocat.Chain G
 
    tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b