Mercurial > hg > Members > kono > Proof > category
changeset 803:984d20c10c87
simpler graph to category
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Apr 2019 10:37:27 +0900 |
| parents | 7bc41fc7b563 |
| children | 2716d2945730 |
| files | CCChom.agda discrete.agda |
| diffstat | 2 files changed, 91 insertions(+), 102 deletions(-) [+] |
line wrap: on
line diff
--- a/CCChom.agda Thu Apr 25 03:50:30 2019 +0900 +++ b/CCChom.agda Thu Apr 25 10:37:27 2019 +0900 @@ -586,69 +586,75 @@ Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl -module ccc-from-graph ( Atom : Set ) ( homm : Atom → Atom → Set ) where +module ccc-from-graph where open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) - - data objs : Set where - atom : Atom → objs - ⊤ : objs - _∧_ : objs → objs → objs - _<=_ : objs → objs → objs - - data arrow : objs → objs → Set where - hom : {a b : Atom} → homm a b → arrow (atom a) (atom b) - id : (a : objs ) → arrow a a - ○ : (a : objs ) → arrow a ⊤ - π : {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 a → arrow c b → arrow c (a ∧ b) - _・_ : {a b c : objs } → arrow b c → arrow a b → arrow a c - _* : {a b c : objs } → arrow (c ∧ b ) a → arrow c ( a <= b ) - open import discrete open graphtocat + open Graph + + data Objs {G : Graph } : Set where + atom : (obj G) → Objs + ⊤ : Objs + _∧_ : Objs {G} → Objs {G} → Objs + _<=_ : Objs {G} → Objs {G} → Objs + + data Arrow {G : Graph } : Objs {G} → Objs {G} → Set where + arrow : {a b : obj G} → (hom G) a b → Arrow (atom a) (atom b) + id : (a : Objs ) → Arrow a a + ○ : (a : Objs ) → Arrow a ⊤ + π : {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 a → Arrow c b → Arrow c (a ∧ b) + _・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c + _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) + + -- positive intutionistic calculus - DX : Category Level.zero Level.zero Level.zero - DX = GraphtoCat objs arrow + DX : (G : Graph) → Category Level.zero Level.zero Level.zero + DX G = GraphtoCat ( record { obj = Objs {G} ; hom = Arrow {G}} ) -- open import Category.Sets -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - CS : Functor DX (Sets {Level.zero}) - FObj CS (atom x) = Atom + CS : {G : Graph } → Functor (DX G) (Sets {Level.zero}) + FObj (CS {G}) (atom x) = obj G FObj CS ⊤ = One' FObj CS (x ∧ x₁) = FObj CS x /\ FObj CS x₁ FObj CS (x <= x₁) = FObj CS x₁ → FObj CS x FMap CS {a} {.a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero}) - FMap CS {a} {b} (mono (x ・ y )) = Sets [ FMap CS (mono x) o FMap CS (mono y) ] - FMap CS {atom a} {atom b} (mono (hom f)) = λ x → b - FMap CS {a} {.a} (mono (id a)) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero}) - FMap CS {a} {⊤} (mono (○ a)) = λ x → OneObj' - FMap CS {(b ∧ _)} {b} (mono π) = proj₁ - FMap CS {(_ ∧ b)} {b} (mono π') = proj₂ - FMap CS {((b <= _) ∧ _)} {b} (mono ε) = λ x → ( proj₁ x ) ( proj₂ x ) - FMap CS {a} {(_ ∧ _)} (mono < f , g >) = λ x → ( FMap CS (mono f) x , FMap CS (mono g) x ) - FMap CS {a} {(_ <= _)} (mono (f *)) = λ x → λ y → FMap CS (mono f) ( x , y ) - FMap CS {a} {⊤} (connected x f) = λ x → OneObj' - FMap CS {a} {b} (connected x f) = Sets [ FMap CS (mono x) o FMap CS f ] + FMap CS {a} {b} (next (x ・ y )) = Sets [ FMap CS (next x) o FMap CS (next y) ] + FMap CS {atom a} {atom b} (next (arrow f)) = λ x → b + FMap CS {a} {.a} (next (id a)) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero}) + FMap CS {a} {⊤} (next (○ a)) = λ x → OneObj' + FMap CS {(b ∧ _)} {b} (next π) = proj₁ + FMap CS {(_ ∧ b)} {b} (next π') = proj₂ + FMap CS {((b <= _) ∧ _)} {b} (next ε) = λ x → ( proj₁ x ) ( proj₂ x ) + FMap CS {a} {(_ ∧ _)} (next < f , g >) = λ x → ( FMap CS (next f) x , FMap CS (next g) x ) + FMap CS {a} {(_ <= _)} (next (f *)) = λ x → λ y → FMap CS (next f) ( x , y ) isFunctor CS = isf where distrCS : {a b c : Obj DX } { g : Hom DX b c } { f : Hom DX a b } → Sets [ FMap CS (DX [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ] distrCS {a} {.a} {.a} {id a} {id a} = refl - distrCS {a} {b} {.b} {id b} {mono x} = refl - distrCS {a} {b} {.b} {id b} {connected x g} = refl - distrCS {a} {.(atom _)} {.(atom _)} {mono (hom x)} {g} = {!!} - distrCS {a} {.a₁} {.a₁} {mono (id a₁)} {g} = {!!} - distrCS {a} {.a₁} {.⊤} {mono (○ a₁)} {g} = {!!} - distrCS {a} {.(c ∧ _)} {c} {mono π} {g} = {!!} - distrCS {a} {.(_ ∧ c)} {c} {mono π'} {g} = {!!} - distrCS {a} {.((c <= _) ∧ _)} {c} {mono ε} {g} = {!!} - distrCS {a} {b} {.(_ ∧ _)} {mono < x , x₁ >} {g} = {!!} - distrCS {a} {b} {c} {mono (x ・ x₁)} {g} = {!!} - distrCS {a} {b} {.(_ <= _)} {mono (x *)} {g} = {!!} - distrCS {a} {b} {c} {connected x f} {g} = {!!} + distrCS {a} {b} {.b} {id b} {next x} = refl + distrCS {.(atom b)} {atom b} {atom c} {next (arrow x)} {id .(atom b)} = refl + distrCS {a} {atom b} {atom c} {next (arrow x)} {next x₁} = {!!} + distrCS {a} {atom(b)} {atom(c)} {next (arrow x)} {next x1} = extensionality Sets ( λ y → begin + FMap CS (DX [ next (arrow x) o next x1 ]) y + ≡⟨ {!!} ⟩ + c + ≡⟨⟩ + FMap CS (next (arrow x)) ( FMap CS (next x1) y) + ∎ ) where open ≡-Reasoning + distrCS {a} {.a₁} {.a₁} {next (id a₁)} {g} = {!!} + distrCS {a} {.a₁} {.⊤} {next (○ a₁)} {g} = {!!} + distrCS {a} {.(c ∧ _)} {c} {next π} {g} = {!!} + distrCS {a} {.(_ ∧ c)} {c} {next π'} {g} = {!!} + distrCS {a} {.((c <= _) ∧ _)} {c} {next ε} {g} = {!!} + distrCS {a} {b} {.(_ ∧ _)} {next < x , x₁ >} {g} = {!!} + distrCS {a} {b} {c} {next (x ・ x₁)} {g} = {!!} + distrCS {a} {b} {.(_ <= _)} {next (x *)} {g} = {!!} isf : IsFunctor DX Sets (FObj CS) ( FMap CS ) IsFunctor.identity isf = extensionality Sets ( λ x → refl ) IsFunctor.distr isf = distrCS
--- a/discrete.agda Thu Apr 25 03:50:30 2019 +0900 +++ b/discrete.agda Thu Apr 25 10:37:27 2019 +0900 @@ -6,71 +6,54 @@ open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) - +record Graph : Set (Level.suc Level.zero ) where + field + obj : Set + hom : obj → obj → Set module graphtocat where - data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where - id : ( a : obj ) → Arrow a a - mono : { a b : obj } → hom a b → Arrow a b - connected : {a b : obj } → {c : obj} → hom b c → Arrow {obj} {hom} a b → Arrow a c + open import Relation.Binary.PropositionalEquality - _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c - id a + id .a = id a - id b + mono x = mono x - id a + connected x y = connected x y - mono x + id a = mono x - mono x + mono y = connected x (mono y) - mono x + connected y z = connected x ( connected y z ) - connected x y + z = connected x ( y + z ) + data Chain { g : Graph } : ( a b : Graph.obj g ) → Set where + id : ( a : Graph.obj g ) → Chain a a + next : { a b c : Graph.obj g } → (Graph.hom g b c ) → Chain {g} a b → Chain a c - assoc-+ : { obj : Set } { hom : obj → obj → Set } {a b c d : obj } - (f : (Arrow {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) → - ( f + (g + h)) ≡ ((f + g) + h ) - assoc-+ (id a) (id .a) (id .a) = refl - assoc-+ (id a) (id .a) (mono x) = refl - assoc-+ (id a) (id .a) (connected h h₁) = refl - assoc-+ (id a) (mono x) (id a₁) = refl - assoc-+ (id a) (mono x) (mono x₁) = refl - assoc-+ (id a) (mono x) (connected h h₁) = refl - assoc-+ (id a) (connected g h) _ = refl - assoc-+ (mono x) (id a) (id .a) = refl - assoc-+ (mono x) (id a) (mono x₁) = refl - assoc-+ (mono x) (id a) (connected h h₁) = refl - assoc-+ (mono x) (mono x₁) (id a) = refl - assoc-+ (mono x) (mono x₁) (mono x₂) = refl - assoc-+ (mono x) (mono x₁) (connected h h₁) = refl - assoc-+ (mono x) (connected g g₁) _ = refl - assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y ) - - open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) - - GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) → Category Level.zero Level.zero Level.zero - GraphtoCat obj hom = record { - Obj = obj ; - Hom = λ a b → Arrow a b ; - _o_ = λ{a} {b} {c} x y → _+_ x y ; + GraphtoCat : (G : Graph ) → Category Level.zero Level.zero Level.zero + GraphtoCat G = record { + Obj = Graph.obj G ; + Hom = λ a b → Chain {G} 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 } → assoc-+ f g h + identityL = identityL; + identityR = identityR ; + o-resp-≈ = o-resp-≈ ; + associative = λ{a b c d f g h } → associative f g h } } where - identityL : {A B : obj } {f : ( Arrow A B) } → ((id B) + f) ≡ f - identityL {_} {_} {id a} = refl - identityL {_} {_} {mono x} = refl - identityL {_} {_} {connected x f} = refl - identityR : {A B : obj } {f : ( Arrow {obj} {hom} A B) } → ( f + id A ) ≡ f - identityR {_} {_} {id a} = refl - identityR {_} {_} {mono x} = refl - identityR {_} {_} {connected x f} = cong (λ k → connected x k) ( identityR {_} {_} {f} ) - o-resp-≈ : {A B C : obj } {f g : ( Arrow A B)} {h i : ( Arrow B C)} → - f ≡ g → h ≡ i → ( h + f ) ≡ ( i + g ) - o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl + open Chain + obj = Graph.obj G + hom = Graph.hom G + _++_ : {a b c : obj } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c + id _ ++ f = f + (next x f) ++ g = next x ( f ++ g ) + + identityL : {A B : Graph.obj G} {f : Chain A B} → (id B ++ f) ≡ f + identityL = refl + identityR : {A B : Graph.obj G} {f : Chain A B} → (f ++ id A) ≡ f + identityR {a} {_} {id a} = refl + identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} ) + o-resp-≈ : {A B C : Graph.obj G} {f g : Chain A B} {h i : Chain B C} → + f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g) + o-resp-≈ refl refl = refl + associative : {a b c d : Graph.obj G} (f : Chain c d) (g : Chain b c) (h : Chain a b) → + (f ++ (g ++ h)) ≡ ((f ++ g) ++ h) + associative (id a) g h = refl + associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h ) + data TwoObject : Set where @@ -95,7 +78,7 @@ arrow-g : TwoHom t0 t1 TwoCat' : Category Level.zero Level.zero Level.zero -TwoCat' = GraphtoCat TwoObject TwoHom +TwoCat' = GraphtoCat ( record { obj = TwoObject ; hom = TwoHom } ) where open graphtocat _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c @@ -167,7 +150,7 @@ open import Data.Empty DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero -DiscreteCat' S = GraphtoCat S ( λ _ _ → ⊥ ) +DiscreteCat' S = GraphtoCat ( record { obj = S ; hom = ( λ _ _ → ⊥ ) } ) where open graphtocat record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)