Members/kono/Proof/category: CCCGraph.agda comparison

comparison CCCGraph.agda @ 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

comparison

equal deleted inserted replaced

-:625baac95ec8
+:348ed0c473cc
 fmap (id a) x = x
 fmap (○ a) x = OneObj
 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₂ })
+CS :  Functor PL PLS
-FObj CS a  = fobj  a
+FObj CS a  = a
-FMap CS {a} {b} f = fmap  {a} {b} f
+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 )
 distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g + f) z ≡ fmap g (fmap f z)
 distr {a} {a₁} {a₁} {f} {id a₁} z = refl
 distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k  →  j , k  ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where
 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 {
 １ = ⊤ ;
-○ =  λ a x → OneObj ;
+○ =  λ a → record { func  = λ z → OneObj ; proof = ○ a} ;
 _∧_ = λ x y →  x ∧ y   ;
-<_,_> = λ f g x  → ( f x , g x ) ;
+<_,_> = λ f g  → record { func = λ x → ( (func f) x , (func g) x ) ; proof = < proof f , proof g > } ;
-π = proj₁ ;
+π = record { func = proj₁ ; proof = iv π (id _) } ;
-π' = proj₂ ;
+π' = record { func = proj₂ ; proof = iv π' (id _) } ;
 _<=_ = λ b a → b <= a ;
-_* = λ f x y → f ( x , y ) ;
+_* = λ f → record { func = λ x y → (func f )( x , y ) ; proof = iv ((proof f) *) (id _) }  ;
-ε = λ x → ( proj₁ x) (proj₂ x) ;
+ε = record { func = λ x → ( proj₁ x) (proj₂ x) ; proof = iv ε (id _)} ;
 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
+*-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 : Obj CSC } {f : Hom CSC a ⊤} (x : fobj a ) → (func f) x ≡ OneObj
-e20 {a} {f} x with f x
+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} →
+*-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)) ]
+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
 ---
 ---     CCC ( SC (CS G)) Sets   have to be proved
 open ccc-from-graph.Objs
 open ccc-from-graph.Arrow
 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 = {!!} ;
 uniquness = {!!}
 }
 } 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
 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 = ?
+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} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (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 (λ w → x (proj₁ w) (proj₂ w)))
+(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 = {!!} }

Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 922:348ed0c473cc