# HG changeset patch # User Shinji KONO # Date 1588586064 -32400 # Node ID 348ed0c473ccd11b52e22bce982d662ef4f33a13 # Parent 625baac95ec8bb82d71daf20ee8fb68e018763bf PLS diff -r 625baac95ec8 -r 348ed0c473cc CCCGraph.agda --- 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 { １ = ⊤ ; - ○ = λ 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 = {!!} }