Mercurial > hg > Members > kono > Proof > category
changeset 874:484f19f16712
SC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Apr 2020 18:12:33 +0900 |
| parents | 0b5fb015009c |
| children | ad42e7661215 |
| files | CCCGraph.agda CCCGraph1.agda |
| diffstat | 2 files changed, 66 insertions(+), 148 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph.agda Thu Apr 09 09:47:00 2020 +0900 +++ b/CCCGraph.agda Thu Apr 09 18:12:33 2020 +0900 @@ -178,6 +178,72 @@ IsFunctor.≈-cong isf refl = refl IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) + data Sequence {G : Graph} : (a b : Objs G) → Set where + sid : (a : Objs G) → Sequence a a + sprod : {a b c d : Objs G} → Sequence a b → Sequence c d → Sequence (a ∧ c) (b ∧ d) + snext : {a b c : vertex G} → edge G b c → Sequence {G} (atom a) (atom b) → Sequence (atom a) (atom c) + + _+_ : {G : Graph} → {a b c : Objs G} → Sequence b c → Sequence a b → Sequence a c + sid a + g = g + sprod f g + sid _ = sprod f g + sprod f g + sprod h h₁ = sprod ( f + h ) ( g + h₁ ) + snext f g + sid _ = snext f g + snext f g + snext x h = snext f ( g + snext x h ) + + SC : Graph → Category Level.zero Level.zero Level.zero + SC G = record { + Obj = Objs G; + Hom = λ a b → Sequence a b ; + _o_ = λ{a} {b} {c} x y → x + y ; + _≈_ = λ x y → x ≡ y ; + Id = λ{a} → sid 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 + identityL : {A B : Objs G} {f : Sequence A B} → (sid B + f) ≡ f + identityL {a} {b} {f} = refl + identityR : {A B : Objs G} {f : Sequence A B} → (f + sid A) ≡ f + identityR {a} {a} {sid a} = refl + identityR {_} {_} {sprod f f₁} = refl + identityR {_} {_} {snext x f} = refl + associative : {a b c d : Objs G} (f : Sequence c d) (g : Sequence b c) (h : Sequence a b) → + (f + (g + h)) ≡ ((f + g) + h) + associative (sid a) g h = refl + associative (sprod f f₁) (sid _) h = refl + associative (sprod f f₁) (sprod g g₁) (sid _) = refl + associative (sprod f f₁) (sprod g g₁) (sprod h h₁) = cong₂ (λ j k → sprod j k ) (associative f g h) (associative f₁ g₁ h₁) + associative (snext x f) (sid _) h = refl + associative (snext x f) (snext y g) (sid _) = refl + associative (snext x f) (snext y g) (snext z h) = cong ( λ k → snext x k ) (associative f (snext y g) (snext z h)) + o-resp-≈ : {A B C : Objs G} {f g : Sequence A B} {h i : Sequence B C} → + f ≡ g → h ≡ i → (h + f) ≡ (i + g) + o-resp-≈ refl refl = refl + + DD : (G : Graph) → Category Level.zero Level.zero Level.zero + DD G = GraphtoCat (record { vertex = Objs G ; edge = Arrow G }) + scmap : {G : Graph} { a b : Objs G } → Hom (DD G) a b → Hom (SC G) a b + scmap = ? + + GtoSC : (G : Graph ) → Functor (DD G) (SC G) + FObj (GtoSC G) a = a + FMap (GtoSC G) {a} {b} f = ? + isFunctor (GtoSC G) = isf where + _++_ = Category._o_ (DD G) + ++idR = IsCategory.identityR ( Category.isCategory ( DD G ) ) + distr : {a b c d : Obj (DD G)} { f : Hom (DD G) b c } { g : Hom (DD G) c d } → (z : Hom (SC G) a b ) → scmap (g ++ f) + z ≡ scmap g + (scmap f + z) + distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = ? + distr {a} {b} {b} {f} {id b} z = ? + isf : IsFunctor (DD G) (SC G) ? scmap + IsFunctor.identity isf = ? + IsFunctor.≈-cong isf refl = refl + IsFunctor.distr isf {a} {b} {c} {g} {f} = ? + + ------------------------------------------------------ -- Cart Category of CCC and CCC preserving Functor
--- a/CCCGraph1.agda Thu Apr 09 09:47:00 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -open import Level -open import Category -module CCCgraph1 where - -open import HomReasoning -open import cat-utility -open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import CCC -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 - - 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 } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) --- case v - - data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) 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 - - eval : {a b : Objs } (f : Arrows a b ) → Arrows a b - eval (id a) = id a - eval (○ a) = ○ a - eval < f , f₁ > = < eval f , eval f₁ > - eval (iv f (id a)) = iv f (id a) - eval (iv f (○ a)) = iv 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 (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 f (id a) - eval (iv f (iv g h)) | ○ a = iv 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)) | iv f1 t = iv f (iv f1 t) - - pi : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a b - pi (id .(_ ∧ _)) = iv π (id _) - pi < x , x₁ > = x - pi (iv f x) = iv π (iv f x) - - pi' : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a c - pi' (id .(_ ∧ _)) = iv π' (id _) - pi' < x , x₁ > = x₁ - pi' (iv f x) = iv π' (iv f x) - - refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → f ≡ f1 - refl-<l> refl = refl - - 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 - - _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c - f ・ h with eval f - ... | id a = eval h - ... | ○ a = ○ _ - ... | < f1 , g > = < f1 ・ h , g ・ h > - ... | iv f1 (id _) = iv f1 h - ... | iv π < g , g₁ > = ? - ... | iv π' < g , g₁ > = {!!} -- g₁ ・ h - ... | iv ε < g , g₁ > = {!!} -- iv ε < g ・ h , g₁ ・ h > - ... | iv (x *) < g , g₁ > = {!!} -- iv (x *) < g ・ h , g₁ ・ h > - ... | iv x ( (○ a)) = iv x ( ○ _ ) - ... | iv x f1 = {!!} - - _==_ : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂) - _==_ {a} {b} x y = eval x ≡ eval y - - identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f - identityR = {!!} - - distr-e : {a b c : Objs } ( f : Arrows b c ) ( g : Arrows a b ) → eval ( f ・ g ) ≡ (eval f ・ eval g) - distr-e = {!!} - - open import Data.Empty - open import Relation.Nullary - - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl) - - idem-eval : {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f - 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 π < 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 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)) | < t , t₁ > | m | _ = cong ( λ k → iv (f *) k ) m - idem-eval (iv f (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} - -- trans lemma (cong ( λ k → iv f k ) m ) where - -- lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t)) - -- lemma = std-iv f f₁ t {!!} - - assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g) - assoc-iv = {!!} - - - ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g - ==←≡ eq = cong (λ k → eval k ) eq - - 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 - identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f - identityL = {!!} - 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 = {!!} - 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-≈ f=g h=i = {!!}