changeset 922:348ed0c473cc

PLS
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 04 May 2020 18:54:24 +0900
parents 625baac95ec8
children 8380d1af9890
files CCCGraph.agda
diffstat 1 files changed, 59 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon May 04 15:45:20 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 18:54:24 2020 +0900
@@ -193,13 +193,40 @@
    fmap < f , g > x = ( fmap f x , fmap g x )
    fmap (iv x f) a = amap x ( fmap f a )
 
+   record PLHom (a b : Objs) : Set (c₁ ⊔ c₂) where
+     field
+        proof : Hom PL a b
+        func : fobj  a → fobj  b
+
+   open PLHom
+
+   PLS :  Category  c₁  (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PLS = record {
+            Obj  = Objs;
+            Hom = PLHom ;
+            _o_ =  λ{a} {b} {c} x y → record { proof = proof x ・ proof y ; func = λ z → func x ( func y z ) } ;
+            _≈_ =  λ x y → func x ≡ func y ;
+            Id  =  λ{a} → record { proof = id a ; func = λ x → x } ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym} ;
+                    identityL  = λ {a b f} → refl ; 
+                    identityR  = λ {a b f} → refl ; 
+                    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 } → refl
+               }
+           } where  
+              o-resp-≈  : {A B C : Objs} {f g : PLHom A B} {h i : PLHom B C} → 
+                                    func f ≡  func g → func h ≡  func i → (λ z → func h (func f z) ) ≡ (λ z → func i (func g z) )
+              o-resp-≈ refl refl = refl
+
+
 --   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
 
-   CS :  Functor PL (Sets {c₁ ⊔ c₂ })
-   FObj CS a  = fobj  a
-   FMap CS {a} {b} f = fmap  {a} {b} f
+   CS :  Functor PL PLS
+   FObj CS a  = a
+   FMap CS {a} {b} f = record { func = fmap  {a} {b} f ; proof = f }
    isFunctor CS = isf where
         _+_ = Category._o_ PL
         ++idR = IsCategory.identityR ( Category.isCategory PL )
@@ -211,26 +238,26 @@
            adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
                 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z  ≡ fmap ( iv x g ) (fmap f z )
            adistr eq x = cong ( λ k → amap x k ) eq
-        isf : IsFunctor PL Sets fobj fmap 
+        isf : IsFunctor PL PLS (λ x → x) (λ {a} {b} f → record { func = fmap  {a} {b} f ; proof = f } )
         IsFunctor.identity isf = extensionality Sets ( λ x → refl )
         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 
+   CSC = FCat PL PLS CS 
 
    cc1 : CCC CSC       -- SCS is CCC
    cc1 = record {
          1 = ⊤ ;
-         ○ =  λ a x → OneObj ;
+         ○ =  λ a → record { func  = λ z → OneObj ; proof = ○ a} ;
          _∧_ = λ x y →  x ∧ y   ;
-         <_,_> = λ f g x  → ( f x , g x ) ;
-         π = proj₁ ;
-         π' = proj₂ ;
+         <_,_> = λ f g  → record { func = λ x → ( (func f) x , (func g) x ) ; proof = < proof f , proof g > } ;
+         π = record { func = proj₁ ; proof = iv π (id _) } ;
+         π' = record { func = proj₂ ; proof = iv π' (id _) } ;
          _<=_ = λ b a → b <= a ;
-         _* = λ f x y → f ( x , y ) ;
-         ε = λ x → ( proj₁ x) (proj₂ x) ;
+         _* = λ f → record { func = λ x y → (func f )( x , y ) ; proof = iv ((proof f) *) (id _) }  ;
+         ε = record { func = λ x → ( proj₁ x) (proj₂ x) ; proof = iv ε (id _)} ;
          isCCC = record {
                e2  = λ {a} {f} → extensionality Sets ( λ x → e20 {a} {f} x ) ;
                e3a = refl ;
@@ -239,35 +266,21 @@
                π-cong = π-cong ;
                e4a = refl ;
                e4b = refl ;
-               *-cong = *-cong
+               *-cong = λ {a} {b} {c} {f} {f'} → *-cong  {a} {b} {c} {f} {f'}
            }
      } where
-        e20 : {a : Obj CSC } {f : Hom CSC a ⊤} (x : fobj a ) → f x ≡ OneObj
-        e20 {a} {f} x with f x
+        e20 : {a : Obj CSC } {f : Hom CSC a ⊤} (x : fobj a ) → (func f) x ≡ OneObj
+        e20 {a} {f} x with (func 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 :  {a b c : Obj CSC} {f f' : Hom CSC (a ∧ b) c} →
+            CSC [ f ≈ f' ] →
+            CSC [ record { proof = iv (proof f *) (id (FObj CS a)) ; func = λ x y → func f (x , y) }
+            ≈ record { proof = iv (proof f' *) (id (FObj CS a)) ; func = λ x y → func 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)} →  Hom PL a (atom b) 
-   rev {a} {b} sf {f} with plcase f sf
-   ... | t = {!!}
-
-
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
 ---
@@ -414,10 +427,12 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
+open ccc-from-graph.PLHom
+
 ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁}  ) (Cart {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) } ;
+     η = λ a → record { vmap = λ y → atom y ; emap = λ f → record { func = λ x y → next f (x y) ; proof = iv (arrow f ) (id _) }  } ; 
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
@@ -425,7 +440,7 @@
       }
   } where
        csc : Graph → Obj Cart
-       csc g = record { cat = CSC  ; ccc = cc1 ; ≡←≈ = λ eq → eq } where 
+       csc g = record { cat = CSC  ; ccc = cc1 ; ≡←≈ = λ 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)
        cobj {g} {c} f (atom x) = vmap f x
@@ -434,10 +449,17 @@
        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 = ?
+       c-map {g} {c} {a} {atom x} f y with proof y
+       c-map {g} {c} {atom x} {atom x} f y | id (atom x) = {!!}
+       c-map {g} {c} {a} {atom x} f y | iv {_} {_} {atom d} (arrow z) t with (func y) ?  d
+       ... | t11 = {!!}
+       c-map {g} {c} {a} {atom x} f y | iv π t = {!!} -- c-map f ( record { func = λ z → proj₁ ? ; proof = 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} {⊤} 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)))
+       c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (record { func = (λ w → proj₁ ((func z) w )); proof = iv π (proof z)} ))
+             (c-map f record { func = λ w → proj₂ ((func z) w) ; proof = iv π' (proof z)} )
+       c-map {g} {c} {d} {b <= a} f x = {!!} -- CCC._* (ccc c) ( c-map f record { func = λ w → (func 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 = {!!} }