Mercurial > hg > Members > kono > Proof > category
changeset 804:2716d2945730
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Apr 2019 12:22:03 +0900 |
| parents | 984d20c10c87 |
| children | 979c0bf97a5a |
| files | CCChom.agda discrete.agda |
| diffstat | 2 files changed, 35 insertions(+), 53 deletions(-) [+] |
line wrap: on
line diff
--- a/CCChom.agda Thu Apr 25 10:37:27 2019 +0900 +++ b/CCChom.agda Thu Apr 25 12:22:03 2019 +0900 @@ -595,13 +595,13 @@ open Graph data Objs {G : Graph } : Set where - atom : (obj G) → Objs + atom : (vertex 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) + arrow : {a b : vertex G} → (edge 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 @@ -614,49 +614,31 @@ -- positive intutionistic calculus DX : (G : Graph) → Category Level.zero Level.zero Level.zero - DX G = GraphtoCat ( record { obj = Objs {G} ; hom = Arrow {G}} ) + DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} ) -- open import Category.Sets -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ CS : {G : Graph } → Functor (DX G) (Sets {Level.zero}) - FObj (CS {G}) (atom x) = obj G + FObj (CS {G}) (atom x) = vertex 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} (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} {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 ) + FObj CS (a ∧ b) = (FObj CS a ) /\ (FObj CS b ) + FObj CS (a <= b) = FObj CS b → FObj CS a + FMap CS {a} {a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero}) + FMap CS {a} {(atom b)} (next (arrow x) f) = λ _ → b + FMap CS {a} {.a₁} (next (id a₁) f) = FMap CS f + FMap CS {a} {.⊤} (next (○ a₁) f) = λ _ → OneObj' + FMap CS {a} {b} (next π f) = λ z → proj₁ ( FMap CS f z ) + FMap CS {a} {b} (next π' f) = λ z → proj₂ ( FMap CS f z ) + FMap CS {a} {b} (next ε f) = λ z → ( proj₁ (FMap CS f z) )( proj₂ (FMap CS f z) ) + FMap CS {a} {.(_ ∧ _)} (next < f , g > h) = λ z → ( FMap CS (next f h) z , FMap CS (next g h) z) + FMap CS {a} {b} (next (f ・ g) h) = λ z → FMap CS ( next f (next g h ) ) z + FMap CS {a} {(c <= b)} (next (e *) f) = {!!} + isFunctor (CS {G}) = isf where + distrCS : {a b c : Obj (DX G)} { g : Hom (DX G) b c } { f : Hom (DX G) a b } → Sets [ FMap CS ((DX G) [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ] + distrCS = {!!} + isf : IsFunctor (DX G) Sets (FObj CS) ( FMap CS ) + IsFunctor.identity isf = extensionality Sets ( λ x → {!!} ) IsFunctor.distr isf = distrCS IsFunctor.≈-cong isf refl = refl
--- a/discrete.agda Thu Apr 25 10:37:27 2019 +0900 +++ b/discrete.agda Thu Apr 25 12:22:03 2019 +0900 @@ -8,20 +8,20 @@ record Graph : Set (Level.suc Level.zero ) where field - obj : Set - hom : obj → obj → Set + vertex : Set + edge : vertex → vertex → Set module graphtocat where open import Relation.Binary.PropositionalEquality - 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 + data Chain { g : Graph } : ( a b : Graph.vertex g ) → Set where + id : ( a : Graph.vertex g ) → Chain a a + next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain {g} a b → Chain a c GraphtoCat : (G : Graph ) → Category Level.zero Level.zero Level.zero GraphtoCat G = record { - Obj = Graph.obj G ; + Obj = Graph.vertex G ; Hom = λ a b → Chain {G} a b ; _o_ = λ{a} {b} {c} x y → x ++ y ; _≈_ = λ x y → x ≡ y ; @@ -35,21 +35,21 @@ } } where open Chain - obj = Graph.obj G - hom = Graph.hom G + obj = Graph.vertex G + hom = Graph.edge 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 : {A B : Graph.vertex 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 B : Graph.vertex 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} → + o-resp-≈ : {A B C : Graph.vertex 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) → + associative : {a b c d : Graph.vertex 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 ) @@ -78,7 +78,7 @@ arrow-g : TwoHom t0 t1 TwoCat' : Category Level.zero Level.zero Level.zero -TwoCat' = GraphtoCat ( record { obj = TwoObject ; hom = TwoHom } ) +TwoCat' = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } ) where open graphtocat _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c @@ -150,7 +150,7 @@ open import Data.Empty DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero -DiscreteCat' S = GraphtoCat ( record { obj = S ; hom = ( λ _ _ → ⊥ ) } ) +DiscreteCat' S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ → ⊥ ) } ) where open graphtocat record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)