Mercurial > hg > Members > kono > Proof > category

changeset 832:a115daa7d30e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separete
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 26 Mar 2020 02:44:48 +0900
parents b6c87d98e631
children 9d23caa3864e
files CCCGraph.agda CCCGraph1.agda
diffstat 2 files changed, 48 insertions(+), 70 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon Mar 23 02:42:41 2020 +0900
+++ b/CCCGraph.agda	Thu Mar 26 02:44:48 2020 +0900
@@ -178,76 +178,6 @@
        IsFunctor.≈-cong isf refl = refl
        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
-open import graph
-module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
-   open Graph
-   
-   data Objs : Set (c₁ ⊔ c₂) where
-      atom : (vertex G) → Objs 
-      ⊤ : Objs 
-      _∧_ : Objs  → Objs  → Objs 
-      _<=_ : Objs → Objs → Objs 
-
-   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where
-      arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-      ○ : (a : Objs ) → Arrow a ⊤
-      π : {a b : Objs } → Arrow ( a ∧ b ) a
-      π' : {a b : Objs } → Arrow ( a ∧ b ) b
-      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
-      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
-      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
-      id : ( a : Objs ) → Arrow a a
-
-   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
-      i   : {b c : Objs} (k : Arrow b c ) → Arrows b c
-      iii : {b c' c'' : Objs } ( f : Arrows b c' ) ( g : Arrows b c'' ) → Arrows b (c'  ∧ c'')  
-      iv  : {b c d : Objs } ( f : Arrows d c ) ( g : Arrow b d ) → Arrows b c
-      v   : {b c' c'' : Objs } ( f : Arrows (b ∧ c') c'' ) → Arrows b (c'' <= c') 
-
-   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   i (id _) ・ g = g
-   f ・ i (id _)  = f
-   f ・ i g = iv f g
-   f ・ iii g h  = {!!} -- iii ( f ・ g ) ( f ・ h )
-   f ・ (iv g h ) = iv ( f ・ g ) h
-   f ・  v g = ?
---   v ( f ・ iii (g1 g) (iv (id _) (i π') )) where
---      g1 :  {a b c' : Objs} → Arrows a b → Arrows (a ∧ c') b
---      g1 {a} {b} {c'} (i k) = ? -- iv k (i π)
---      g1 {a} {.(_ ∧ _)} {c'} (iii g g₁) = iii (g1 g) (g1 g₁)
---      g1 {a} {b} {c'} (iv f g) = iv f ? -- (g1 g)
---      g1 {a} {b  <= d } {c'} (v g) = v (g2 g) where
---          g2 : Arrows (a ∧ d) b → Arrows ((a ∧ c') ∧ d) b
---          g2 = {!!}
-
-   -- e2 :  {a : Objs } {f : Arrow a ⊤ } → {!!} -- eval f ≡ eval (next (○ a) (id a))
-   -- e2 {⊤} {id ⊤} = refl
-   -- e2 {a} {next x f} = refl
-
-   -- e3a :  {a b c : Objs } {f : Arrow c a} {g : Arrow c b} → 
-   --    eval (next π ( next < {!!} , {!!}  > {!!} )) ≡ {!!} -- eval f -- Sets [ ( Sets [  π  o ( <,> f g)  ] ) ≈ f ]
-   -- e3a = {!!}
-
-   GtoCCC : Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
-   GtoCCC = record {
-            Obj = Objs 
-          ; Hom = Arrows
-          ; _o_ = λ {A} {B} {C} f g → f ・ g
-          ; _≈_ = λ {a} {b} f g → {!!}
-          ; Id  = λ {a} → {!!}
-          ; isCategory = record {
-             isEquivalence = λ {A} {B} → record {
-                  refl = λ {f} →  {!!}
-                ; sym = λ {f} {g}  → {!!}
-                ; trans = λ {f} {g} {h} → {!!} }
-             ; identityL = λ {x} {y} {f} → {!!}
-             ; identityR = λ {x} {y} {f} → {!!}
-             ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i}  → {!!}
-             ; associative =  λ {a} {b} {c} {d} {f} {g} {h} → {!!}
-           }}
-
-   FGisCCC : CCC GtoCCC 
-   FGisCCC = {!!}
 
 ------------------------------------------------------
 --  Cart     Category of CCC and CCC preserving Functor
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CCCGraph1.agda	Thu Mar 26 02:44:48 2020 +0900
@@ -0,0 +1,48 @@
+open import Level
+open import Category 
+module CCCgraph1 where
+
+open import HomReasoning
+open import cat-utility
+open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import CCC
+open import graph
+
+module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
+   open Graph
+   
+   data Objs : Set (c₁ ⊔ c₂) where
+      atom : (vertex G) → Objs 
+      ⊤ : Objs 
+      _∧_ : Objs  → Objs  → Objs 
+      _<=_ : Objs → Objs → Objs 
+
+   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where
+      arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
+      ○ : (a : Objs ) → Arrow a ⊤
+      π : {a b : Objs } → Arrow ( a ∧ b ) a
+      π' : {a b : Objs } → Arrow ( a ∧ b ) b
+      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
+      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
+      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
+      id : ( a : Objs ) → Arrow a a
+
+   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
+      i   : {b c : Objs} (k : Arrow b c ) → Arrows b c
+      iii : {b c' c'' : Objs } ( f : Arrows b c' ) ( g : Arrows b c'' ) → Arrows b (c'  ∧ c'')  
+      iv  : {b c d : Objs } ( f : Arrows d c ) ( g : Arrow b d ) → Arrows b c
+      v   : {b c' c'' : Objs } ( f : Arrows (b ∧ c') c'' ) → Arrows b (c'' <= c') 
+
+   eval :  {a b c : Objs } (f : Arrow b c ) → (g : Arrows a b) → Arrows a c
+   eval = {!!}
+
+   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
+   _・_ {a} {_} {⊤} _ _ = i ( ○ a )
+   i (id _)  ・ f = f
+   f ・ i (id _)  = f
+   (iv f g) ・ h  = f ・ eval g h 
+   f ・ (iv g h)  = iv ( f ・ g ) h
+   i f ・ g = eval f g 
+   iii f g ・  h = iii (f ・ h) ( g ・ h )
+   v f ・ g = {!!}
+