Mercurial > hg > Members > kono > Proof > category

changeset 894:2e52bb0a4097

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC is trivial
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Apr 2020 18:01:05 +0900
parents 4a66f48ffee5
children 4d64a90410c6
files CCCGraph.agda CCCGraph1.agda
diffstat 2 files changed, 44 insertions(+), 204 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon Apr 13 12:22:26 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 13 18:01:05 2020 +0900
@@ -165,68 +165,22 @@
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   data SL : (t : Objs ) → Set  (c₁ ⊔ c₂) where
-      term : SL ⊤
-      value : (x : vertex G) → SL (atom x)
-      _::_ : {a b : vertex G} → (f : edge G a b ) → (prev : SL (atom a)) → SL (atom b)
-      _,_ : {a b : Objs } → (f : SL a ) → (g : SL b) → SL (a ∧ b)
-      func0 : {a b : vertex G } → {c : Objs } →  edge G a b  → SL ( c <= atom b )  → SL (c <= atom a )  
-      func1 : {a b c : Objs } →  SL (b <= a) → SL ( c <= a )  → SL (( b ∧ c) <= a )  
-      func2 : {a b c  : Objs } →  SL ( ( c <= b ) <= a) →  SL ( c <= ( a ∧ b) )  
-      func3 : {a : Objs } → SL ( ⊤ <= a )  
-      func4 : {a : Objs } → SL a → SL ( a <= ⊤  )  
-      func5 : {a b c : Objs } → SL a  → SL ( c <= b ) → SL ( c <= (b <= a) )  
-      func6 : {a b c : Objs } → SL ( b <= a ) → SL ( c <= b ) → SL ( (c <= b )<= a )  
-      func7 : {a : Objs } →  SL ( a <= a )  
+   open import Data.List
 
-   fobj' :  ( a  : Objs  ) → Set (c₁ ⊔ c₂)
-   fobj' a = SL a
+   C = graphtocat.Chain G
 
-   fmap' : { a b : Objs  } → Hom PL a b → fobj'  a → fobj'  b
-   amap' : { a b : Objs  } → Arrow  a b → fobj' a → fobj' b
-   amap' (arrow x) f = {!!}
-   amap' π (f , f₁) = {!!}
-   amap' π' (f , f₁) = {!!}
-   amap' ε (f , f₁) = {!!}
-   amap' (x *) term = {!!}
-   amap' {atom v} {b <= a} (x *) (value v) = {!!} where
-       lemma : SL a → SL b
-       lemma = λ y → fmap' x ( (value v) , y )
-   amap' (x *) (f :: f₁) = {!!}
-   amap' (x *) (f , f₁) = {!!}
-   amap' (x *) (func0 x₁ f) = {!!}
-   amap' (x *) (func1 f f₁) = {!!}
-   amap' (x *) (func2 f) = {!!}
-   amap' (x *) func3 = {!!}
-   amap' (x *) (func4 f) = {!!}
-   amap' (x *) (func5 f f₁) = {!!}
-   amap' (x *) (func6 f f₁) = {!!}
-   amap' {c} {b <= a} (x *) func7 = {!!} where
-       lemma : SL a → SL b
-       lemma = λ y → fmap' x ( func7 , y )
-   fmap' = {!!}
+   tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
+   tr f x y  = graphtocat.next f (x y) 
+   
+   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂)
+   fobj  (atom x) = ( y : vertex G ) → C y x
+   fobj ⊤ = One
+   fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
+   fobj  (a <= b) = fobj  b → fobj  a
 
-   record SM : Set (suc (c₁ ⊔ c₂))  where
-      field
-        sobj : vertex G → Set (c₁ ⊔ c₂)
-        smap : { a b : vertex G } → edge G a b  → sobj a → sobj b
-   open SM
-
-   SSS : SM
-   SSS = record {
-        sobj = λ x →  {!!}
-       ;smap = λ {a} {b} f x → {!!}
-     }
-
-   fobj : {G : SM} ( a  : Objs  ) → Set (c₁ ⊔ c₂)
-   fobj {G} (atom x) = sobj G x
-   fobj ⊤ = One
-   fobj {G} (a ∧ b) = ( fobj {G} a /\ fobj {G} b)
-   fobj {G} (a <= b) = fobj {G} b → fobj {G} a
-
-   fmap : {G : SM } { a b : Objs  } → Hom PL a b → fobj {G} a → fobj {G} b
-   amap : {G : SM } { a b : Objs  } → Arrow  a b → fobj {G} a → fobj {G} b
-   amap {G} (arrow x) =  smap G x
+   fmap :  { a b : Objs  } → Hom PL a b → fobj  a → fobj  b
+   amap :  { a b : Objs  } → Arrow  a b → fobj  a → fobj  b
+   amap  (arrow x) =  tr x
    amap π ( x , y ) = x 
    amap π' ( x , y ) = y
    amap ε (f , x ) = f x
@@ -240,9 +194,9 @@
    --    Sets is CCC, so we have a cartesian closed category generated by a graph
    --       as a sub category of Sets
 
-   CS : {G : SM} → Functor PL (Sets {c₁ ⊔ c₂})
-   FObj (CS {G}) a  = fobj {G} a
-   FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
+   CS :  Functor PL (Sets {c₁ ⊔ c₂})
+   FObj CS a  = fobj  a
+   FMap CS {a} {b} f = fmap  {a} {b} f
    isFunctor CS = isf where
         _+_ = Category._o_ PL
         ++idR = IsCategory.identityR ( Category.isCategory PL )
@@ -259,6 +213,33 @@
         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 subcat
+
+   CSC = FCat PL (Sets {c₁ ⊔ c₂}) CS
+
+   cc1 : CCC CSC
+   cc1 = record {
+         １ = ⊤ ;
+         ○ =  λ a x → OneObj ;
+         _∧_ = λ x y →  x ∧ y   ;
+         <_,_> = λ f g x  → ( f x , g x ) ;
+         π = proj₁ ;
+         π' = proj₂ ;
+         _<=_ = λ b a → b <= a ;
+         _* = λ f x y → f ( x , y ) ;
+         ε = λ x → ( proj₁ x) (proj₂ x) ;
+         isCCC = record {
+               e2  =  extensionality Sets ( λ x → {!!} ) ;
+               e3a = refl ;
+               e3b = refl ;
+               e3c = refl ;
+               π-cong = {!!} ;
+               e4a = refl ;
+               e4b = refl ;
+               *-cong = {!!} 
+           }
+     }
+
 
 ------------------------------------------------------
 --  Cart     Category of CCC and CCC preserving Functor
@@ -322,7 +303,7 @@
 
 open GMap
 
-open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
+-- open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
 
 data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B)
      : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where
--- a/CCCGraph1.agda	Mon Apr 13 12:22:26 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-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 import  Relation.Binary.PropositionalEquality hiding ( [_] )
-   open import  Relation.Binary.Core 
-   open Graph
-   
-   data Objs : Set (c₁ ⊔ c₂) where
-      atom : (vertex G) → Objs 
-      ⊤ : Objs 
-      _∧_ : Objs  → Objs  → Objs 
-      _<=_ : Objs → Objs → Objs 
-
-   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) 
-   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
-      arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-      π : {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 } → Arrows (c ∧ b ) a → Arrow c ( a <= b )        --- case v
-
-   data  Arrows where
-      id : ( a : Objs ) → Arrows a a                                      --- case i
-      ○ : ( a : Objs ) → Arrows a ⊤                                       --- case i
-      <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b)      -- case iii
-      iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
-
-   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   id a ・ g = g
-   ○ a ・ g = ○ _
-   < f , g > ・ h = < f ・ h , g ・ h >
-   iv f g ・ h = iv f ( g ・ h )
-
-   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
-   identityR {a} {a} {id a} = refl
-   identityR {a} {⊤} {○ a} = refl
-   identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j  , k > ) identityR identityR
-   identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
-   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
-   identityL = refl
-   associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
-   associative (id a) g h = refl
-   associative (○ a) g h = refl
-   associative < f , f₁ > g h = cong₂ (λ j k → < j  , k > )  (associative f g h) (associative f₁ g h) 
-   associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h )
-
-   PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
-   PL = record {
-            Obj  = Objs;
-            Hom = λ a b →  Arrows  a b ;
-            _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x ≡  y ;
-            Id  =  λ{a} → id a ;
-            isCategory  = record {
-                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-                    identityL  = λ {a b f} → identityL {a} {b} {f} ; 
-                    identityR  = λ {a b f} → identityR {a} {b} {f} ; 
-                    o-resp-≈  = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}  ; 
-                    associative  = λ{a b c d f g h } → associative  f g h
-               }
-           } where  
-              o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
-                                    f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-              o-resp-≈ refl refl = refl 
-
-
-   eval :  {a b : Objs } (f : Arrows a b ) → Arrows a b
-   eval (id a) = id a
-   eval (○ a) = ○ a
-   eval < f , f₁ > = < eval f , eval f₁ >
-   eval (iv (f *) (id a)) = iv ((eval f) *) (id a)
-   eval (iv f (id a)) = iv f (id a)
-   eval (iv (f *) (○ a)) = iv ((eval f)*) (○ a)
-   eval (iv π < g , h >) = eval g
-   eval (iv π' < g , h >) = eval h
-   eval (iv ε < g , h >) = iv ε < eval g , eval h >
-   eval (iv (f *) < g , h >) = iv ((eval f) *) < eval g , eval h >
-   eval (iv f (iv g h)) with eval (iv g h)
-   eval (iv (f *) (iv g h)) | id a = iv ((eval f)*) (id a)  
-   eval (iv f (iv g h)) | id a = iv f (id a)  
-   eval (iv (f *) (iv g h)) | ○ a = iv ((eval f)*) (○ a)
-   eval (iv π (iv g h)) | < t , t₁ > = t
-   eval (iv π' (iv g h)) | < t , t₁ > = t₁
-   eval (iv ε (iv g h)) | < t , t₁ > =  iv ε < t , t₁ > 
-   eval (iv (f *) (iv g h)) | < t , t₁ > = iv ((eval f) *) < t , t₁ > 
-   eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) 
-
-
-   PL1 :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
-   PL1 = record {
-            Obj  = Objs;
-            Hom = λ a b →  Arrows  a b ;
-            _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → eval x ≡ eval y ;
-            Id  =  λ{a} → id a ;
-            isCategory  = record {
-                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-                    identityL  = λ {a b f} → cong (λ k → eval k ) (identityL {a} {b} {f});
-                    identityR  = λ {a b f} → cong (λ k → eval k ) (identityR {a} {b} {f});
-                    o-resp-≈  = λ {a b c f g h i} → ore {a} {b} {c} f g h i ; 
-                    associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
-               }
-           }  where 
-              d-eval  : {A B C : Objs} (f : Arrows B C) (g : Arrows A B) →
-                     eval (f ・ g) ≡ eval (eval f ・ eval g)
-              d-eval = {!!}
-              ore  : {A B C : Objs} (f g : Arrows A B) (h i : Arrows B C) →
-                                    eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g)
-              ore f g h i f=g h=i = begin
-                    eval (h ・ f)
-                ≡⟨ d-eval h f ⟩
-                    eval (eval h ・ eval f)
-                ≡⟨ cong₂ (λ j k → eval ( j ・ k )) h=i f=g  ⟩
-                    eval (eval i ・ eval g)
-                ≡⟨ sym ( d-eval i g ) ⟩
-                    eval (i ・ g)
-                ∎  where open ≡-Reasoning
-
-
---    fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
---    fmap f = {!!}
--- 
---    PLCCC :  Functor PL PL
---    PLCCC = record {
---          FObj = λ x → x
---        ; FMap = fmap
---        ; isFunctor = record {
---               identity = {!!}
---             ; distr = {!!}
---             ; ≈-cong = {!!}
---           }
---       }