# HG changeset patch # User Shinji KONO # Date 1556131830 -32400 # Node ID 7bc41fc7b563e20b99034eb2c864b3b238319592 # Parent aa4fbd00724786fbf131f1dfc6645fcfd8f43c05 graph with positive logic to Sets diff -r aa4fbd007247 -r 7bc41fc7b563 CCChom.agda --- a/CCChom.agda Wed Apr 24 11:09:41 2019 +0900 +++ b/CCChom.agda Thu Apr 25 03:50:30 2019 +0900 @@ -588,138 +588,69 @@ module ccc-from-graph ( Atom : Set ) ( homm : Atom → Atom → Set ) where - open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) + open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) - data Objs : Set where - ⊤ : Objs - atom : Atom → Objs - _∧_ : Objs → Objs → Objs - _<=_ : Objs → Objs → Objs + data objs : Set where + atom : Atom → objs + ⊤ : objs + _∧_ : objs → objs → objs + _<=_ : objs → objs → objs - data arrow : Objs → Objs → Set where + 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 b c : Objs } → arrow b c → arrow a b → arrow a c - ○ : (a : Objs ) → arrow a ⊤ - π : {a b : Objs } → arrow ( a ∧ b ) a - π' : {a b : Objs } → arrow ( a ∧ b ) b - <_,_> : {a b c : Objs } → arrow c a → arrow c b → arrow c (a ∧ b) - ε : {a b : Objs } → arrow ((a <= b) ∧ b ) a - _* : {a b c : Objs } → arrow (c ∧ b ) a → arrow c ( a <= 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 - GC : Category Level.zero Level.zero Level.zero - GC = GraphtoCat Objs arrow - - product : {a b c : Objs } → Arrow c a → Arrow c b → Arrow {Objs} {arrow} c ( a ∧ b ) - product {a} {b} {c} y (connected {_} {_} {d} x g) = connected (< π , x ・ π' >) ( product y g ) - product {a} {b} {c} (connected {_} {_} {d} x g) y = connected (< x ・ π , π' >) ( product g y ) - product {a} {.a} {.a} (id a) (id .a) = mono ( < id a , id a > ) - product {a} {b} {.a} (id a) (mono x) = mono ( < id a , x > ) - product {a} {.a₁} {.a₁} (mono x) (id a₁) = mono ( < x , id a₁ > ) - product {a} {b} {c} (mono x) (mono x₁) = mono ( < x , x₁ > ) - - star : {a b c : Objs} → Arrow (a ∧ b) c → Arrow {Objs} {arrow} a (c <= b) - star {a} {b} {.(a ∧ b)} (id .(a ∧ b)) = mono ( id (a ∧ b ) * ) - star {a} {b} {c} (mono x) = mono ( x * ) - star {a} {b} {c} (connected {_} {d} {_} x y) = connected ( ( x ・ ε ) * ) ( star y ) - - - data _==_ : {a b : Objs } → (f g : Arrow {Objs} {arrow} a b ) → Set where - rrefl : {a b : Objs } → {f : Arrow {Objs} {arrow} a b } → f == f - trefl : {a b : Objs} → {h i : Arrow {Objs} {arrow} ⊤ b } {f g : Arrow {Objs} {arrow} a ⊤ } → h == i → (h + f) == (i + g) - - ≡→== : {a b : Objs } → {f g : Arrow {Objs} {arrow} a b } → f ≡ g → f == g - ≡→== refl = rrefl + -- positive intutionistic calculus + DX : Category Level.zero Level.zero Level.zero + DX = GraphtoCat objs arrow - r== : {a b : Objs } → { f : Arrow {Objs} {arrow} a b } → f == f - r== = ≡→== refl - - s== : {a b : Objs } → { f g : Arrow {Objs} {arrow} a b } → f == g → g == f - s== rrefl = rrefl - s== (trefl rrefl) = trefl rrefl - s== (trefl (trefl eq)) = trefl {!!} - - t== : {a b : Objs } → { i j k : Arrow {Objs} {arrow} a b } → i == j → j == k → i == k - t== rrefl rrefl = rrefl - t== eq eq1 = {!!} - - ctcong : {a b c : Objs } → { f g : Arrow {Objs} {arrow} a b } → { x : arrow b c } → f == g → connected x f == connected x g - ctcong rrefl = rrefl - ctcong (trefl eq) = trefl {!!} - - ccc-e2 : {a : Objs } → ∀ { f : Arrow {Objs} {arrow} a ⊤ } → f == mono (○ a) - ccc-e2 {a} {f} = {!!} - - -- Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _ - -- Reflexive _∼_ = ∀ {x} → x ∼ x - - open import Relation.Binary.Core - open import Relation.Binary - import Relation.Binary.EqReasoning as EqR + -- open import Category.Sets + -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - cccIEQ : {a b : Objs } → Setoid Level.zero Level.zero - cccIEQ {a} {b} = record { - Carrier = Arrow {Objs} {arrow} a b - ; _≈_ = _==_ - ; isEquivalence = record {refl = r== ; trans = t== ; sym = s== } - } - + CS : Functor DX (Sets {Level.zero}) + FObj CS (atom x) = Atom + 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 ] + 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} = {!!} + isf : IsFunctor DX Sets (FObj CS) ( FMap CS ) + IsFunctor.identity isf = extensionality Sets ( λ x → refl ) + IsFunctor.distr isf = distrCS + IsFunctor.≈-cong isf refl = refl - GraphtoCCC : Category Level.zero Level.zero Level.zero - GraphtoCCC = record { - Obj = Objs ; - Hom = λ a b → Arrow {Objs} {arrow} a b ; - _o_ = _+_ ; - _≈_ = _==_ ; - Id = λ{a} → id a ; - isCategory = record { - isEquivalence = record {refl = r== ; trans = t== ; sym = s== } - ; identityL = identityL - ; identityR = identityR - ; o-resp-≈ = λ{a b c f g h i} → {!!} - ; associative = λ{a b c d f g h } → {!!} - } - } where - identityL : {a b : Objs } → { f : Arrow {Objs} {arrow} a b } → (id b + f) == f - identityL {a} {.a} {id a} = rrefl - identityL {a} {b} {mono x} = rrefl - identityL {a} {b} {connected x f} = rrefl - identityR : {a b : Objs } → { f : Arrow {Objs} {arrow} a b } → (f + id a ) == f - identityR {a} {.a} {id a} = rrefl - identityR {a} {b} {mono x} = rrefl - identityR {a} {b} {connected x f} = ctcong identityR - --- ≈⟨ {!!} ⟩ --- ∎ where open EqR cccIEQ -- open IsEquivalence cccIEQ - --- GLCCC : CCC GraphtoCCC --- GLCCC = record { --- １ = ⊤ --- ; ○ = λ f → mono (○ f) --- ; _∧_ = _∧_ --- ; <_,_> = λ f g → product f g --- ; π = mono π --- ; π' = mono π' --- ; _<=_ = _<=_ --- ; _* = star --- ; ε = mono ε --- ; isCCC = isc --- } where --- GC = GraphtoCCC --- e2 : {a : Obj GC } → ∀ { f : Hom GC a ⊤ } → GC [ f ≈ mono (○ a) ] --- e2 {.⊤} {id .⊤} = {!!} --- e2 {a} {mono x} = {!!} --- e2 {a} {connected x f} = {!!} --- e3a = {!!} --- e3b = {!!} --- e3c = {!!} --- π-cong = {!!} --- e4a = {!!} --- e4b = {!!} --- *-cong = {!!} --- ---