Mercurial > hg > Members > kono > Proof > category

changeset 926:a7332c329b57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove CSC and subcat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 05 May 2020 08:23:54 +0900
parents 5eed22f4a75d
children 2c5ae3015a05
files CCCGraph.agda subcat.agda
diffstat 2 files changed, 21 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon May 04 21:13:23 2020 +0900
+++ b/CCCGraph.agda	Tue May 05 08:23:54 2020 +0900
@@ -216,60 +216,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 subcat
-
-   CSC = FCat PL (Sets {c₁ ⊔ c₂ }) CS 
-
-   cc1 : CCC CSC       -- SCS is CCC
-   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  = λ {a} {f} → extensionality Sets ( λ x → e20 {a} {f} x ) ;
-               e3a = refl ;
-               e3b = refl ;
-               e3c = refl ;
-               π-cong = π-cong ;
-               e4a = refl ;
-               e4b = refl ;
-               *-cong = *-cong
-           }
-     } where
-        e20 : {a : Obj CSC } {f : Hom CSC a ⊤} (x : fobj a ) → f x ≡ OneObj
-        e20 {a} {f} x with f x
-        e20 x | OneObj = refl
-        π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
-                    Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
-        π-cong refl refl = refl
-        *-cong : {a b c : Obj CSC } {f f' : Hom CSC (a ∧ b) c} →
-                    Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
-        *-cong refl = refl
-
-   data plcase {b : vertex G}  : {a : Objs } → (f : Hom PL a (atom b)) → ( sf : Hom CSC a (atom b)) → Set (c₁ ⊔ c₂) where
-       pid :  plcase (id (atom b)) (id1 CSC (atom b))
-       parrow : {a : Objs } {c : vertex G} → (x : edge G c b) → (f : Arrows a (atom c))
-           → plcase (iv (arrow x) f) ( λ y z → graphtocat.next x (fmap f y z )) 
-       pπ : {a c : Objs } (f : Arrows a ((atom b) ∧ c))
-           → plcase (iv π f) (λ y → proj₁ (fmap f y ))
-       pπ' : {a c : Objs } (f : Arrows a (c ∧ (atom b) ))
-           → plcase (iv π' f) (λ y → proj₂ (fmap f y ))
-       pε : {a c : Objs } (f : Arrows a ((atom b <= c) ∧ c))
-           → plcase (iv ε f) (λ y → proj₁ (fmap f y ) (proj₂ (fmap f y )) )
-
-   rev : {a : Objs } → {b : vertex G}  → ( sf : Hom CSC a (atom b)) → ∀{f : Hom PL a (atom b)} → FMap CS f ≡ sf  →  Hom PL a (atom b) 
-   rev {atom b} {b} .(λ x → x) {id (atom b)} refl = id (atom b)
-   rev {a} {b} .(λ a₁ y → graphtocat.next x (fmap f₁ a₁ y)) {iv (arrow x) f₁} refl = iv (arrow x) f₁
-   rev {a} {b} .(λ a₁ → proj₁ (fmap f₁ a₁)) {iv π f₁} refl = iv π f₁
-   rev {a} {b} .(λ a₁ → proj₂ (fmap f₁ a₁)) {iv π' f₁} refl = iv π' f₁
-   rev {a} {b} .(λ a₁ → proj₁ (fmap f₁ a₁) (proj₂ (fmap f₁ a₁))) {iv ε f₁} refl = iv ε f₁
-
 
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
@@ -417,36 +363,38 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
-ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁}  ) (Cart {c₁} {c₁} {c₁} ) UX
+ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {suc c₁} {c₁}  ) (Cart {suc c₁} {c₁} {c₁} ) UX
 ccc-graph-univ {c₁}   = record {
      F = λ g → csc g ;
-     η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) } ;
-     _* = solution ;
+     η = λ a → record { vmap = λ y → {!!} ; emap = λ f x y →  next f (x y) } ;
+     _* = {!!} ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
          uniquness = {!!}
       }
   } where
-       csc : Graph → Obj Cart
-       csc g = record { cat = CSC  ; ccc = cc1 ; ≡←≈ = λ eq → eq } where 
-           open ccc-from-graph g
-       cobj  : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c)  → Obj (cat (csc g)) → Obj (cat c)
+       open ccc-from-graph
+       csc : Graph {suc c₁} {c₁} → Obj (Cart {suc c₁} {c₁} {c₁})
+       csc g = record { cat = Sets {c₁}  ; ccc = sets {c₁}; ≡←≈ = λ eq → eq } 
+       cs : (g : Graph {c₁} {c₁}) → Functor  (ccc-from-graph.PL g) (Sets {c₁})
+       cs g = CS g
+       pl : (g : Graph {c₁} {c₁} ) → Category  c₁  c₁  c₁
+       pl g = PL g
+       cobj  : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
        cobj {g} {c} f (atom x) = vmap f x
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
        cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
-       c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Obj (cat (csc g))}
-           → (f : Hom Grph g (FObj UX c) ) → Hom (cat (csc g)) A B → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       c-map {g} {c} {a} {atom x} f y with ccc-from-graph.rev g y {{!!}} refl
-       c-map {g} {c} {atom x} {atom x} f y | id (atom x) = id1 (cat c) (cobj {g} {c} f (atom x))
-       c-map {g} {c} {a} {atom x} f y | iv (arrow x₁) t = {!!}
-       c-map {g} {c} {a} {atom x} f y | iv π t = {!!}
-       c-map {g} {c} {a} {atom x} f y | iv π' t = {!!}
-       c-map {g} {c} {a} {atom x} f y | iv ε t = {!!}
+       c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Objs g}
+           → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
+       c-map {g} {c} {atom a} {atom x} f y = {!!}
+       c-map {g} {c} {⊤} {atom x} f y = {!!}
+       c-map {g} {c} {a ∧ b} {atom x} f y = {!!}
+       c-map {g} {c} {b <= a} {atom x} f y = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
-       c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ w → proj₁ (z w))) (c-map f (λ w → proj₂ (z w)))
-       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ w → x (proj₁ w) (proj₂ w)))
-       solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
-       solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = c-map {g} {c} f ; isFunctor = {!!} } ; ccf = {!!} }
+       c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!})
+       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
+       solution : {g : Obj (Grph {c₁} {c₁})} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c) → Hom (Cart  {suc c₁} {c₁} {c₁}) {!!} {!!}
+       solution {g} {c} f = record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
 
 
--- a/subcat.agda	Mon May 04 21:13:23 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-open import Category
-open import Level
-module subcat {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') (B : Category c₁ c₂ ℓ) (F : Functor A B) where
-
-    open import cat-utility
-    open import Relation.Binary.PropositionalEquality
-    open Functor
-
-    FCat : Category c₁' c₂ ℓ
-    FCat = record {
-          Obj = Obj A
-          ; Hom = λ a b → Hom B (FObj F a) (FObj F b)
-          ; _o_ = Category._o_ B
-          ; _≈_ = Category._≈_ B
-          ; Id  = λ {a} → id1 B (FObj F a)
-          ; isCategory = record {
-                    isEquivalence =  IsCategory.isEquivalence (Category.isCategory B) ;
-                    identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
-                    identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
-                    o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
-                    associative  = λ{a b c d f g h } → IsCategory.associative (Category.isCategory B) 
-             }
-      }