Mercurial > hg > Members > kono > Proof > category
changeset 888:32c11e2fdf82
another approach
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Apr 2020 09:57:22 +0900 |
| parents | 9c41a7851817 |
| children | 07fdaecc17b3 |
| files | CCCGraph.agda CCCGraph1.agda |
| diffstat | 2 files changed, 128 insertions(+), 85 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph.agda Sun Apr 12 04:10:01 2020 +0900 +++ b/CCCGraph.agda Sun Apr 12 09:57:22 2020 +0900 @@ -96,32 +96,71 @@ Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl -module sets-from-graph where - ------------------------------------------------------- --- CCC generated from a graph ------------------------------------------------------- +open import graph +module ccc-from-graph {c₁ c₂ : Level} (G : Graph {c₁} {c₂} ) where + open import Relation.Binary.PropositionalEquality hiding ( [_] ) + open import Relation.Binary.Core + open Graph + + data Objs : Set (c₁ ⊔ c₂) where + atom : (vertex G) → Objs + ⊤ : Objs + _∧_ : Objs → Objs → Objs + _<=_ : Objs → Objs → Objs - open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) - open import graph - open graphtocat + data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) + data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i + arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) + π : {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 } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v - open Graph + data Arrows where + id : ( a : Objs ) → Arrows a a --- case i + ○ : ( a : Objs ) → Arrows a ⊤ --- case i + <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii + iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv + + _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c + id a ・ g = g + ○ a ・ g = ○ _ + < f , g > ・ h = < f ・ h , g ・ h > + iv f g ・ h = iv f ( g ・ h ) - data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where -- formula - atom : (vertex G) → Objs G - ⊤ : Objs G - _∧_ : Objs G → Objs G → Objs G - _<=_ : Objs G → Objs G → Objs G + identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f + identityR {a} {a} {id a} = refl + identityR {a} {⊤} {○ a} = refl + identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR + identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR + identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f + identityL = refl + associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → + (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) + associative (id a) g h = refl + associative (○ a) g h = refl + associative < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (associative f g h) (associative f₁ g h) + associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h ) - data Arrow (G : Graph ) : Objs G → Objs G → Set where --- proof - arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b) - ○ : (a : Objs G ) → Arrow G a ⊤ - π : {a b : Objs G } → Arrow G ( a ∧ b ) a - π' : {a b : Objs G } → Arrow G ( a ∧ b ) b - ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a - <_,_> : {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 ) + -- positive intutionistic calculus + PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) + PL = record { + Obj = Objs; + Hom = λ a b → Arrows a b ; + _o_ = λ{a} {b} {c} x y → x ・ y ; + _≈_ = λ x y → x ≡ y ; + Id = λ{a} → id a ; + isCategory = record { + isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; + identityL = λ {a b f} → identityL {a} {b} {f} ; + identityR = λ {a b f} → identityR {a} {b} {f} ; + 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 } → associative f g h + } + } where + o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → + f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) + o-resp-≈ refl refl = refl record SM {v : Level} : Set (suc v) where field @@ -131,52 +170,46 @@ open SM - -- positive intutionistic calculus - PL : (G : SM) → Graph - PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) } - DX : (G : SM) → Category Level.zero Level.zero Level.zero - DX G = GraphtoCat (PL G) - -- open import Category.Sets -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - fobj : {G : SM} ( a : Objs (graph G) ) → Set - fobj {G} (atom x) = sobj G x - fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) - fobj {G} (a <= b) = fobj {G} b → fobj {G} a - fobj ⊤ = One - amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b - amap {G} (arrow x) = smap G x - amap (○ a) _ = OneObj - amap π ( x , _) = x - amap π'( _ , x) = x - amap ε ( f , x ) = f x - amap < f , g > x = (amap f x , amap g x) - amap (f *) x = λ y → amap f ( x , y ) - fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b - fmap {G} {a} (id a) = λ z → z - fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ] + -- fobj : {G : SM} ( a : Objs (graph G) ) → Set + -- fobj {G} (atom x) = sobj G x + -- fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) + -- fobj {G} (a <= b) = fobj {G} b → fobj {G} a + -- fobj ⊤ = One + -- amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b + -- amap {G} (arrow x) = smap G x + -- amap (○ a) _ = OneObj + -- amap π ( x , _) = x + -- amap π'( _ , x) = x + -- amap ε ( f , x ) = f x + -- amap < f , g > x = (amap f x , amap g x) + -- amap (f *) x = λ y → amap f ( x , y ) + -- fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b + -- fmap {G} {a} (id a) = λ z → z + -- fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ] -- 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 : (G : SM ) → Functor (DX G) (Sets {Level.zero}) - FObj (CS G) a = fobj a - FMap (CS G) {a} {b} f = fmap {G} {a} {b} f - isFunctor (CS G) = isf where - _++_ = Category._o_ (DX G) - ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) - distr : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z) - distr {a} {b} {c} {f} {next {b} {d} {c} 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 (graph G) d c ) → fmap ( next x (g ++ f) ) z ≡ fmap ( next x g ) (fmap f z ) - adistr eq x = cong ( λ k → amap x k ) eq - distr {a} {b} {b} {f} {id b} z = refl - isf : IsFunctor (DX G) Sets fobj fmap - 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 ) + -- CS : (G : SM ) → Functor (DX G) (Sets {Level.zero}) + -- FObj (CS G) a = fobj a + -- FMap (CS G) {a} {b} f = fmap {G} {a} {b} f + -- isFunctor (CS G) = isf where + -- _++_ = Category._o_ (DX G) + -- ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) + -- distr : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z) + -- distr {a} {b} {c} {f} {next {b} {d} {c} 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 (graph G) d c ) → fmap ( next x (g ++ f) ) z ≡ fmap ( next x g ) (fmap f z ) + -- adistr eq x = cong ( λ k → amap x k ) eq + -- distr {a} {b} {b} {f} {id b} z = refl + -- isf : IsFunctor (DX G) Sets fobj fmap + -- 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 ) ------------------------------------------------------
--- a/CCCGraph1.agda Sun Apr 12 04:10:01 2020 +0900 +++ b/CCCGraph1.agda Sun Apr 12 09:57:22 2020 +0900 @@ -77,19 +77,21 @@ eval (id a) = id a eval (○ a) = ○ a eval < f , f₁ > = < eval f , eval f₁ > + eval (iv (f *) (id a)) = iv ((eval f) *) (id a) eval (iv f (id a)) = iv f (id a) - eval (iv f (○ a)) = iv f (○ a) + eval (iv (f *) (○ a)) = iv ((eval f)*) (○ a) eval (iv π < g , h >) = eval g eval (iv π' < g , h >) = eval h eval (iv ε < g , h >) = iv ε < eval g , eval h > eval (iv (f *) < g , h >) = iv ((eval f) *) < eval g , eval h > eval (iv f (iv g h)) with eval (iv g h) + eval (iv (f *) (iv g h)) | id a = iv ((eval f)*) (id a) eval (iv f (iv g h)) | id a = iv f (id a) - eval (iv f (iv g h)) | ○ a = iv f (○ a) + eval (iv (f *) (iv g h)) | ○ a = iv ((eval f)*) (○ a) eval (iv π (iv g h)) | < t , t₁ > = t eval (iv π' (iv g h)) | < t , t₁ > = t₁ eval (iv ε (iv g h)) | < t , t₁ > = iv ε < t , t₁ > - eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > + eval (iv (f *) (iv g h)) | < t , t₁ > = iv ((eval f) *) < t , t₁ > eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → f ≡ f1 @@ -98,6 +100,8 @@ refl-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → g ≡ g1 refl-<r> refl = refl + idem-eval : {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f + iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c ) ( g : Arrows a (atom b) ) → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g) iv-e-arrow x (id (atom _)) = refl @@ -113,15 +117,16 @@ iv-e-ε (iv f g) | < t , t₁ > = refl iv-e-ε (iv f g) | iv f₁ t = refl iv-e-* : { a b c d : Objs } → { f : Arrows (d ∧ b) c} → ( g : Arrows a d ) - → eval (iv (f *) g) ≡ iv (f *) (eval g) + → eval (iv (f *) g) ≡ iv ((eval f) *) (eval g) iv-e-* (id a) = refl iv-e-* (○ a) = refl - iv-e-* < g , g₁ > = {!!} + iv-e-* < g , g₁ > = refl iv-e-* (iv f g) with eval (iv f g) iv-e-* (iv f g) | id a = refl iv-e-* (iv f g) | ○ a = refl iv-e-* (iv f g) | < t , t₁ > = refl - iv-e-* (iv f g) | iv f₁ t = refl + iv-e-* (iv (f *) g) | iv f₁ t = {!!} + iv-e-* (iv f g) | iv f₁ t = {!!} iv-e : { a b c : Objs } → (x : Arrow b c ) ( f : Arrows a b) → { d : Objs } { y : Arrow d b } { g : Arrows a d } → eval f ≡ iv y g @@ -130,7 +135,7 @@ iv-e x (○ a) () iv-e x < f , f₁ > () iv-e x (iv f g) {_} {y} {h} eq with eval (iv f g) - iv-e x (iv f g) {_} {y} {h} refl | iv y h = refl + iv-e x (iv f g) {_} {y} {h} refl | iv y h = {!!} π-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c ) → eval g ≡ < f1 , f2 > → eval (iv π g ) ≡ f1 @@ -152,7 +157,6 @@ π'-lemma (iv ε g) f1 f2 eq with eval (iv ε g) π'-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl - idem-eval : {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g)) iv-d (arrow x) g = begin eval (iv (arrow x) g) @@ -227,9 +231,9 @@ iv-d (x *) g = begin eval (iv (x *) g) ≡⟨ iv-e-* g ⟩ - iv (x *) (eval g) - ≡⟨ cong (λ k → iv (x *) k ) ( sym ( idem-eval g) ) ⟩ - iv (x *) (eval (eval g)) + iv ((eval x) *) (eval g) + ≡⟨ cong (λ k → iv ((eval x) *) k ) ( sym ( idem-eval g) ) ⟩ + iv ((eval x) *) (eval (eval g)) ≡⟨ sym (iv-e-* (eval g)) ⟩ eval (iv (x *) (eval g)) ∎ where open ≡-Reasoning @@ -237,22 +241,26 @@ idem-eval (id a) = refl idem-eval (○ a) = refl idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁) - idem-eval (iv f (id a)) = refl - idem-eval (iv f (○ a)) = refl + idem-eval (iv (f *) (id a)) = {!!} + idem-eval (iv f (id a)) = {!!} + idem-eval (iv (f *) (○ a)) = {!!} + idem-eval (iv f (○ a)) = {!!} idem-eval (iv π < g , g₁ >) = idem-eval g idem-eval (iv π' < g , g₁ >) = idem-eval g₁ idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁) - idem-eval (iv (x *) < f , f₁ >) = {!!} -- cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁) + idem-eval (iv (x *) < f , f₁ >) = {!!} -- cong₂ ( λ j k → iv ((eval x) *) < j , k > ) (idem-eval f) (idem-eval f₁) idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) | inspect eval (iv g h) - idem-eval (iv f (iv g h)) | id a | m | _ = refl - idem-eval (iv f (iv g h)) | ○ a | m | _ = refl - idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> m - idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> m - idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv ε k ) m + idem-eval (iv f (iv g h)) | id a | m | _ = {!!} + idem-eval (iv f (iv g h)) | ○ a | m | _ = {!!} + idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> {!!} + idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> {!!} + idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv ε k ) ? idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv (f *) k ) m - idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m ) - idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-* (iv f₁ t)) (cong ( λ k → iv (x *) k ) m ) + idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m ) + idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-* (iv f₁ t)) {!!} -- (cong ( λ k → iv (x *) k ) m ) idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = begin + {!!} + ≡⟨ {!!} ⟩ eval (iv π ( iv f₁ t)) ≡⟨ {!!} ⟩ eval (iv π (eval (iv g h ))) @@ -262,9 +270,11 @@ iv π (eval (iv g h)) ≡⟨ cong (λ k → iv π k ) ee ⟩ iv π ( iv f₁ t) + ≡⟨ {!!} ⟩ + {!!} ∎ where open ≡-Reasoning idem-eval (iv π' (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} - idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m ) + idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m ) PL1 : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL1 = record { @@ -286,13 +296,13 @@ d-eval (id a) g = sym (idem-eval g) d-eval (○ a) g = refl d-eval < f , f₁ > g = cong₂ (λ j k → < j , k > ) (d-eval f g) (d-eval f₁ g) - d-eval (iv x (id a)) g = iv-d x g - d-eval (iv (x *) (○ a)) g = refl + d-eval (iv x (id a)) g = {!!} -- iv-d x g + d-eval (iv (x *) (○ a)) g = {!!} -- refl d-eval (iv π < f , f₁ >) g = d-eval f g d-eval (iv π' < f , f₁ >) g = d-eval f₁ g d-eval (iv ε < f , f₁ >) g = cong₂ (λ j k → iv ε k ) (d-eval f g) ( cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) - d-eval (iv (x *) < f , f₁ >) g = {!!} -- cong₂ (λ j k → iv (x *) k ) (d-eval f g) ( + d-eval (iv (x *) < f , f₁ >) g = {!!} -- cong₂ (λ j k → iv ((eval x) *) k ) (d-eval f g) ( -- cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) d-eval (iv x (iv f f₁)) g = begin eval (iv x (iv f f₁) ・ g)