Mercurial > hg > Members > kono > Proof > category

changeset 830:232cea484067

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to CCC again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Mar 2020 14:26:39 +0900
parents 6c5cfb9b333e
children b6c87d98e631
files CCCGraph.agda deductive.agda freyd2.agda yoneda.agda
diffstat 4 files changed, 97 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/CCCGraph.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -96,7 +96,7 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
-module ccc-from-graph where
+module sets-from-graph where
 
 ------------------------------------------------------
 --  CCC generated from a graph
@@ -123,21 +123,6 @@
       <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
       _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
 
-   data one {v : Level} {S : Set v} : Set v where
-             elm : (x : S ) → one 
-
-   iso→ : {v : Level} {S : Set v} → one → S
-   iso→ (elm x) = x
-
-   data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where
-       elmeq : {x : S} →  iso←  ( elm x ) x
-
-   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a
-   iso-left (elm x) .x elmeq = refl
-
-   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x ) 
-   iso-right (elm x) = elmeq
-
    record SM {v : Level} : Set (suc v)  where
       field
         graph : Graph  {v} {v}
@@ -193,6 +178,89 @@
        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
+      next : { a b c : Objs } → Arrow b c  → Arrow a b → Arrow a c
+
+   _・_ :  {a b c : Objs } (f : Arrow b c ) → (g : Arrow a b) → Arrow a c
+   id _ ・ f = f
+   (next x f) ・ g = next x ( f ・ g )
+   f ・ g = next f g 
+
+   -- data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ) where
+   --   i   : {b c : Obj A} {k : Hom A b c } → φ x k
+   --   ii  : φ x {⊤} {a} x
+   --   iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
+   --   iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
+   --   v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
+
+   data  φ  : {b c : Objs } → Arrow b c → Set ( c₁  ⊔  c₂ ) where
+      i   : {b c : Objs} {k : Arrow b c } → φ k
+      iii : {b c' c'' : Objs } { f : Arrow b c' } { g : Arrow b c'' } (ψ : φ f ) (χ : φ g ) → φ {b} {c'  ∧ c''} < f , g > 
+      iv  : {b c d : Objs } { f : Arrow d c } { g : Arrow b d } (ψ : φ f ) (χ : φ g ) → φ ( f ・ g )
+      v   : {b c' c'' : Objs } { f : Arrow (b ∧ c') c'' }  (ψ : φ f )  → φ {b} {c'' <= c'} ( f * )
+
+
+   eval : {a b : Objs} → (f : Arrow a b ) → {fe : Arrow a b } → φ {a} {b} fe
+   eval {atom a} {atom b} (arrow f) = i
+   eval {a} {⊤} (○ a) = i
+   eval {b ∧ _} {b} π = i
+   eval {.(_ ∧ b)} {b} π' = i
+   eval {.((b <= _) ∧ _)} {b} ε = i
+   eval {a} {_ ∧ _} < f , g > = {!!} -- iii (eval f) (eval g)
+   eval {a} {_ <= _} (f *) = {!!} -- v {!!}
+   eval {a} {a} (id a) = i
+   eval {a} {b} (next {a} {a} {b} f (id a)) = eval f
+   eval {a} {b} (next {a} {c} {b} f (next {a} {d} {c} g h) ) = iv {a} {b} {d} (iv {d} {b} {c} (eval f) (eval g) ) (eval h)
+   eval {a} {b} (next {a} {c} {b} f g) with eval g
+   ... | t = {!!}
+
+   -- 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 = Arrow
+          ; _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
 ------------------------------------------------------
--- a/deductive.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/deductive.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -44,3 +44,6 @@
   k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
   k x∈a (iv ψ χ ) = k x∈a ψ  ・ < π , k x∈a χ  >
   k x∈a (v ψ ) = ( k x∈a ψ  ・ α ) *
+
+--  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
+--  toφ {a} {b} {c} x∈a z = {!!}
--- a/freyd2.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/freyd2.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -239,7 +239,7 @@
 
             
 
--- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable
+-- A is complete and K{*}↓U has preinitial full subcategory then U is representable (and U preserve Limit)
 
 -- if U preserve limit,  K{*}↓U has initial object from freyd.agda
 
--- a/yoneda.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/yoneda.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -91,7 +91,7 @@
          }
 
 -- A is Locally small
-postulate ≈-≡ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+postulate ≡←≈ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
@@ -117,10 +117,10 @@
         } 
     }  where
         lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
-        lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL
+        lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} idL
         lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ 
                Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x
-        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin
+        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} ( begin
                Category.op A [ Category.op A [ g o f ] o x ]
              ≈↑⟨ assoc ⟩
                Category.op A [ g o Category.op A [ f o x ] ]
@@ -128,7 +128,7 @@
                ( λ x →  Category.op A [ g o x  ]  ) ( ( λ x → Category.op A [ f o x ] ) x )
              ∎ )
         lemma-y-obj3 :  {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] →  Category.op A [ f o x ] ≡ Category.op A [ g o x ]
-        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A}   ( begin
+        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A}   ( begin
                 Category.op A [ f o x ]
              ≈⟨ resp refl-hom eq ⟩
                 Category.op A [ g o x ]
@@ -150,7 +150,7 @@
    lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) →
         Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈
         Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ]
-   lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ {_} {_} {_} {A} ( begin
+   lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x →  ≡←≈ {_} {_} {_} {A} ( begin
                 A [ A [ f o x ] o g ]
              ≈↑⟨ assoc ⟩
                 A [ f o A [ x  o g ] ]
@@ -177,7 +177,7 @@
   } where
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ]
         ≈-cong {a} {b} {f} {g} eq  =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
-             extensionality A ( λ h → ≈-≡ {_} {_} {_} {A}  ( begin
+             extensionality A ( λ h → ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ f o h ]
              ≈⟨ resp refl-hom eq ⟩
                 A [ g o h ]
@@ -185,7 +185,7 @@
           ) ) 
         identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a )  ]
         identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
-             extensionality A ( λ g →  ≈-≡ {_} {_} {_} {A}  ( begin
+             extensionality A ( λ g →  ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ id1 A a o g ] 
              ≈⟨ idL ⟩
                 g
@@ -193,7 +193,7 @@
           ) )  
         distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ]
         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]))) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
-           extensionality A ( λ h →  ≈-≡ {_} {_} {_} {A}  ( begin
+           extensionality A ( λ h →  ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ A [ g o f ]  o h ]
              ≈↑⟨ assoc  ⟩
                 A [  g o A [ f o h ] ]
@@ -277,7 +277,7 @@
                     TMap ha b (FMap (y-obj A a) g (Category.Category.Id A))
                 ≡⟨⟩
                     TMap ha b ( (A Category.o Category.Category.Id A) g )
-                ≡⟨  ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL  ( Category.isCategory A ))) ⟩
+                ≡⟨  ≡-cong ( TMap ha b ) ( ≡←≈ {_} {_} {_} {A} (IsCategory.identityL  ( Category.isCategory A ))) ⟩
                     TMap ha b g
                 ∎ 
              )) ⟩