# HG changeset patch # User Shinji KONO # Date 1588358456 -32400 # Node ID b8c5f15ee561eb4ae4b7ac0ffcec365332d80087 # Parent 8f41ad966eaaedc9683d1d9d919d623c769efb24 small graph and small category on CCC to graph diff -r 8f41ad966eaa -r b8c5f15ee561 CCCGraph.agda --- a/CCCGraph.agda Fri May 03 17:11:33 2019 +0900 +++ b/CCCGraph.agda Sat May 02 03:40:56 2020 +0900 @@ -94,132 +94,129 @@ Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl -module ccc-from-graph where +open import graph +module ccc-from-graph {c₁ c₂ : Level} (G : Graph {c₁} {c₂} ) where open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) - open import graph - open graphtocat - open Graph - 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 + data Objs : Set c₁ where + atom : (vertex G) → Objs + ⊤ : Objs + _∧_ : Objs → Objs → Objs + _<=_ : Objs → Objs → Objs - 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 ) + 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 + + 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 - data one {v : Level} {S : Set v} : Set v where - elm : (x : S ) → one + _・_ : {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 ) - iso→ : {v : Level} {S : Set v} → one → S - iso→ (elm x) = x + identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f + identityL = refl - data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where - elmeq : {x : S} → iso← ( elm x ) x + 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 - iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a - iso-left (elm x) .x elmeq = refl - - iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x ) - iso-right (elm x) = elmeq + assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → + (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) + assoc≡ (id a) g h = refl + assoc≡ (○ a) g h = refl + assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) + assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) --- record one {v : Level} {S : Set v} : Set (suc v) where --- field --- elm : S + -- positive intutionistic calculus + PL : Category 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 } → assoc≡ 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 + +-------- -- --- iso→ : {v : Level} {S : Set v} → one {v} {S} → One {Level.zero} → S --- iso→ x OneObj = one.elm x --- iso← : {v : Level} {S : Set v} → one {v} {S} → S → One {Level.zero} --- iso← x y = OneObj +-- Functor from Positive Logic to Sets -- --- iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso→ x ( iso← x a ) ≡ a --- iso-left x a = {!!} --- --- iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x OneObj ) ≡ OneObj --- iso-right x = refl + + -- open import Category.Sets + -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ + + C = graphtocat.Chain G - record one' {v : Level} {S : Set v} : Set (suc v) where - field - elm' : S - iso→' : One {Level.zero} → S - iso←' : S → One {Level.zero} - iso-left' : iso→' ( iso←' elm' ) ≡ elm' - iso-right' : iso←' ( iso→' OneObj ) ≡ OneObj + tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b + tr f x y = graphtocat.next f (x y) + + fobj : ( a : Objs ) → Set (c₁ ⊔ c₂ ) + fobj (atom x) = ( y : vertex G ) → C y x + fobj ⊤ = One + fobj (a ∧ b) = ( fobj a /\ fobj b) + fobj (a <= b) = fobj b → fobj a + + fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b + amap : { a b : Objs } → Arrow a b → fobj a → fobj b + amap (arrow x) = tr x + amap π ( x , y ) = x + amap π' ( x , y ) = y + amap ε (f , x ) = f x + amap (f *) x = λ y → fmap f ( x , y ) + fmap (id a) x = x + fmap (○ a) x = OneObj + fmap < f , g > x = ( fmap f x , fmap g x ) + fmap (iv x f) a = amap x ( fmap f a ) - tmp : {v : Level} {S : Set v} → one {v} {S} → one' {v} {S} - tmp x = record { - elm' = iso→ x - ; iso→' = λ _ → iso→ x - ; iso←' = λ _ → OneObj - ; iso-left' = refl - ; iso-right' = refl - } - +-- 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 : Functor PL (Sets {c₁ ⊔ c₂ }) + FObj CS a = fobj a + FMap CS {a} {b} f = fmap {a} {b} f + isFunctor CS = isf where + _+_ = Category._o_ PL + ++idR = IsCategory.identityR ( Category.isCategory PL ) + distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z) + distr {a} {a₁} {a₁} {f} {id a₁} z = refl + distr {a} {a₁} {⊤} {f} {○ a₁} z = refl + distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z) + distr {a} {b} {c} {f} {iv {_} {_} {d} 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 d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) + adistr eq x = cong ( λ k → amap x k ) eq + isf : IsFunctor PL 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 ) - record SM {v : Level} : Set (suc v) where - field - graph : Graph {v} {v} - sobj : vertex graph → Set - smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b - - 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 ] - - -- 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 ) --- --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap @@ -233,6 +230,7 @@ record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where field cat : Category c₁ c₂ ℓ + ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g ccc : CCC cat open CCCObj @@ -268,7 +266,7 @@ open import graph open Graph -record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc (v ⊔ v') ) where +record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (v ⊔ v' ) where field vmap : vertex x → vertex y emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) @@ -288,8 +286,8 @@ _&_ : {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } -Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (suc ( v ⊔ v')) -Grp {v} {v'} = record { +Grph : {v v' : Level} → Category (suc (v ⊔ v')) (v ⊔ v') (suc ( v ⊔ v')) +Grph {v} {v'} = record { Obj = Graph {v} {v'} ; Hom = GMap {v} {v'} ; _o_ = _&_ @@ -340,41 +338,43 @@ g' ∎ ) -fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grp {c₁} {c₂}) +fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grph {c₁} {c₂}) fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } -fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b ) +fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b ) fmap f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) } -UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) → {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g ) - → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) -FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡ ) a = fobj a -FMap (UX ≈-to-≡) f = fmap f -isFunctor (UX {c₁} {c₂} {ℓ} ≈-to-≡) = isf where - -- if we don't need ≈-cong ( i.e. f ≈ g → UX f =m= UX g ), all lemmas are not necessary - open import HomReasoning - isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap - IsFunctor.identity isf {a} {b} {f} e = mrefl refl - IsFunctor.distr isf f = mrefl refl - IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 ( - ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) - ))) (eq e) where - lemma4 : {x y : vertex (fobj b) } → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y - lemma4 (refl eqv) = refl - lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e - lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv ) +UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} ) +FObj UX a = fobj a +FMap UX f = fmap f +isFunctor UX = isf where + isf : IsFunctor Cart Grph fobj fmap + IsFunctor.identity isf {a} {b} {f} e = mrefl refl + IsFunctor.distr isf {a} {b} {c} f = mrefl refl + IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 ( + ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) + )))) (f=g e) where + lemma4 : {x y : vertex (fobj b) } → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y + lemma4 (refl eqv) = refl + lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e + lemma refl (refl eqv) = mrefl (≡←≈ b eqv) ---- ---- open ccc-from-graph ---- ---- sm : {v : Level } → Graph {v} → SM {v} ---- SM.graph (sm g) = g ---- SM.sobj (sm g) = {!!} ---- SM.smap (sm g) = {!!} ---- ---- HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v}) ---- HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ; ccc = sets } ) ---- ---- ---- ---- +open ccc-from-graph.Objs +open ccc-from-graph.Arrow +open ccc-from-graph.Arrows +open graphtocat.Chain + +ccc-graph-univ : {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁} ) (Cart {c₁} {c₁} {c₁} ) UX +ccc-graph-univ {c₁} = record { + F = λ g → csc g ; + η = λ a → record { vmap = λ y → atom y ; emap = λ f x y → next f (x y) } ; + _* = {!!} ; + isUniversalMapping = record { + universalMapping = {!!} ; + uniquness = {!!} + } + } where + csc : Graph → Obj Cart + csc g = record { cat = {!!} ; ccc = {!!} } where + open ccc-from-graph g +