Mercurial > hg > Members > kono > Proof > category

changeset 906:91b8b7fb64eb

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:49:45 +0900
parents 47a0a9f2eee9
children 549933e67978
files CCCGraph.agda
diffstat 1 files changed, 12 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Fri May 01 17:08:23 2020 +0900
+++ b/CCCGraph.agda	Fri May 01 17:49:45 2020 +0900
@@ -227,9 +227,9 @@
       f1 : {!!}
       f1 = smap f
    samap ε (pair y y₁) = {!!}
-   samap π sid = ?
-   samap π' sid = ?
-   samap ε sid = ?
+   samap π sid = {!!}
+   samap π' sid = {!!}
+   samap ε sid = {!!}
    smap (id (atom x)) = seq (graphtocat.id x)
    smap (id ⊤) = top
    smap (id (a ∧ b)) = sid -- pair (smap (id a)) (smap (id b))
@@ -264,6 +264,15 @@
    fmap < f , g > x = ( fmap f x , fmap g x )
    fmap (iv x f) a = amap x ( fmap f a )
 
+   _==_ : { a   : Objs  } → (f g : fobj a ) →  Set ℓ 
+   _==_ {atom x} f g = {!!}
+   _==_ {⊤} OneObj OneObj = OneObj ≡ OneObj
+   _==_ {a ∧ b} (f , g) (h , i) = ( f == h ) /\ ( g == i )
+   _==_ {b <= a} f g = {!!} -- λ (x : fobj a) →  ? -- _≑_ f g {x}
+   
+   _≑_ :  { a  b : Objs  } → (f g : fobj  a → fobj  b ) → {x :  fobj a}  → Set ℓ
+   _≑_ {a} {b} f g {x} = f x == g x
+
 --   CS is a map from Positive logic to Sets
 --    Sets is CCC, so we have a cartesian closed category generated by a graph
 --       as a sub category of Sets