Mercurial > hg > Members > kono > Proof > category
view CCCGraph.agda @ 822:4c0580d9dda4
from cart to graph, hom equality to set equality
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 01 May 2019 21:16:58 +0900 |
parents | fbbc9c03bfed |
children | f57c9603d989 |
line wrap: on
line source
open import Level open import Category module CCCgraph where open import HomReasoning open import cat-utility open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import CCC open Functor -- ccc-1 : Hom A a 1 ≅ {*} -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c open import Category.Sets -- Sets is a CCC postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ data One {l : Level} : Set l where OneObj : One -- () in Haskell ( or any one object set ) sets : {l : Level } → CCC (Sets {l}) sets {l} = record { 1 = One ; ○ = λ _ → λ _ → OneObj ; _∧_ = _∧_ ; <_,_> = <,> ; π = π ; π' = π' ; _<=_ = _<=_ ; _* = _* ; ε = ε ; isCCC = isCCC } where 1 : Obj Sets 1 = One ○ : (a : Obj Sets ) → Hom Sets a 1 ○ a = λ _ → OneObj _∧_ : Obj Sets → Obj Sets → Obj Sets _∧_ a b = a /\ b <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) <,> f g = λ x → ( f x , g x ) π : {a b : Obj Sets } → Hom Sets (a ∧ b) a π {a} {b} = proj₁ π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b π' {a} {b} = proj₂ _<=_ : (a b : Obj Sets ) → Obj Sets a <= b = b → a _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) f * = λ x → λ y → f ( x , y ) ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) isCCC : CCC.IsCCC Sets 1 ○ _∧_ <,> π π' _<=_ _* ε isCCC = record { e2 = e2 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} ; e3c = e3c ; π-cong = π-cong ; e4a = e4a ; e4b = e4b ; *-cong = *-cong } where e2 : {a : Obj Sets} {f : Hom Sets a 1} → Sets [ f ≈ ○ a ] e2 {a} {f} = extensionality Sets ( λ x → e20 x ) where e20 : (x : a ) → f x ≡ ○ a x e20 x with f x e20 x | OneObj = refl e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] e3a = refl e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] e3b = refl e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] e3c = refl π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] π-cong refl refl = refl e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] e4a = refl e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] e4b = refl *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl module ccc-from-graph where open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) open import discrete 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 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 one {v : Level} {S : Set v} : Set v where elm : (x : S ) → one iso→ : {v : Level} {S : Set v} → one → S iso→ (elm x) = x data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where elmeq : {x : S} → iso← ( elm x ) x 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 -- record one {v : Level} {S : Set v} : Set (suc v) where -- field -- elm : S -- -- 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 -- -- 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 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 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 } 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 --- --- CCC ( SC (CS G)) Sets have to be proved --- SM can be eliminated if we have --- sobj (a : vertex g ) → {a} a set have only a --- smap (a b : vertex g ) → {a} → {b} record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where field cat : Category c₁ c₂ ℓ ccc : CCC cat open CCCObj record CCCMap {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where field cmap : Functor (cat A ) (cat B ) ccf : CCC (cat A) → CCC (cat B) open import Category.Cat open CCCMap open import Relation.Binary.Core Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ)) Cart {c₁} {c₂} {ℓ} = record { Obj = CCCObj {c₁} {c₂} {ℓ} ; Hom = CCCMap ; _o_ = _・_ ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x } ; isCategory = record { isEquivalence = λ {A} {B} → record { refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_} ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f} ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i} → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i} ; associative = λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h} }} where cart-refl : {A B : CCCObj {c₁} {c₂} {ℓ} } → { x : CCCMap A B } → {a b : Obj ( cat A ) } → (f : Hom ( cat A ) a b) → [ cat B ] FMap (cmap x) f ~ FMap (cmap x) f cart-refl {A} {B} {x} {a} {b} f = [_]_~_.refl ( IsFunctor.≈-cong (isFunctor ( cmap x )) ( IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory ( cat A ))))) _・_ : { A B C : CCCObj {c₁} {c₂} {ℓ} } → ( f : CCCMap B C ) → ( g : CCCMap A B ) → CCCMap A C _・_ {A} {B} {C} f g = record { cmap = F ; ccf = ccmap } where F : Functor (cat A) (cat C) F = (cmap f) ○ ( cmap g ) ccmap : CCC (cat A) → CCC (cat C) ccmap ca = ccf f ( ccf g (ccc A )) open import discrete open Graph record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc v ⊔ v' ) where field vmap : vertex x → vertex y emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) open GMap open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) data _=m=_ {v v' : Level} {x y : Graph {v} {v'}} ( f g : GMap x y ) : Set (v ⊔ v' ) where mrefl : ( vmap f ≡ vmap g ) → ( {a b : vertex x} → { e : edge x a b } → emap f e ≅ emap g e ) → f =m= g _&_ : {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') (v ⊔ v') Grp {v} {v'} = record { Obj = Graph {v} {v'} ; Hom = GMap {v} {v'} ; _o_ = _&_ ; _≈_ = _=m=_ ; Id = record { vmap = λ y → y ; emap = λ f → f } ; isCategory = record { isEquivalence = λ {A} {B} → ise {v} {v'} {A} {B} ; identityL = mrefl refl refl ; identityR = mrefl refl refl ; o-resp-≈ = m--resp-≈ ; associative = mrefl refl refl }} where msym : {v v' : Level} {x y : Graph {v} {v'} } { f g : GMap x y } → f =m= g → g =m= f msym (mrefl refl eq ) = mrefl refl ( ≅-sym eq ) mtrans : {v v' : Level} {x y : Graph {v} {v'}} { f g h : GMap x y } → f =m= g → g =m= h → f =m= h mtrans (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( ≅-trans eq eq1 ) ise : {v v' : Level} {x y : Graph {v} {v'}} → IsEquivalence {_} {v ⊔ v'} {_} ( _=m=_ {v} {v'} {x} {y} ) ise = record { refl = λ {x} → mrefl refl refl ; sym = msym ; trans = mtrans } m--resp-≈ : {v : Level} {A B C : Graph {v} } {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) m--resp-≈ {_} {_} {_} {_} {f} {g} {h} {i} (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( λ {a} {b} {e} → begin emap h (emap f e) ≅⟨ ≅-cong ( λ k → emap h k ) eq ⟩ emap h (emap g e) ≅⟨ eq1 ⟩ emap i (emap g e) ∎ ) where open Relation.Binary.HeterogeneousEquality.≅-Reasoning assoc-≈ : {v v' : Level} {A B C D : Graph {v} {v'} } {f : GMap C D} {g : GMap B C} {h : GMap A B} → ( f & ( g & h ) ) =m= ( (f & g ) & h ) assoc-≈ = mrefl refl refl --- Forgetful functor fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grp {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 f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) } ≃-cong : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } → { f f' : Hom B a b } → { g g' : Hom B a' b' } → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g' ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'} (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin f' ≈↑⟨ f=f' ⟩ f ≈⟨ eqv ⟩ g ≈⟨ g=g' ⟩ g' ∎ ) UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) FObj (UX {c₁} {c₂} {ℓ}) a = fobj a FMap UX f = fmap f isFunctor (UX {c₁} {c₂} {ℓ}) = isf where open import HomReasoning lemma0 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a b : Obj B} → [_]_~_ B (id1 B a) (id1 B b) → a ≡ b lemma0 {A} {B} {f} {g} (refl eqv) = refl lemma03 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → [_]_~_ B (FMap f ( id1 A a)) (FMap g ( id1 A a)) → FObj f a ≡ FObj g a lemma03 {A} {B} {f} {g} eq = lemma0 {A} {B} {f} {g} ( ≃-cong B eq (IsFunctor.identity (Functor.isFunctor (f)))(IsFunctor.identity (Functor.isFunctor (g))) ) lemma01 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → f ≃ g → FObj f a ≡ FObj g a lemma01 {A} {B} {f} {g} {a} eq = lemma03 {A} {B} {f} {g} (eq (id1 A a)) lemma1 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B } → (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ] → vmap (fmap f) ≡ vmap (fmap g) lemma1 {a} {b} {f} {g} eq = extensionality Sets ( λ z → lemma01 {cat a} {cat b} {cmap f} {cmap g} eq ) lemma20 : {A B : Category c₁ c₂ ℓ } {a b : Obj A} → ( e : Hom A a b ) → ( g : Functor A B ) → ( f : Hom A a b → Hom B (FObj g a) (FObj g b) ) → B [ f e ≈ FMap g e ] → f e ≅ FMap g e lemma20 e g f eq = {!!} lemma2 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B} → (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ] → vmap (fmap f) ≡ vmap (fmap g) → {a b : vertex (fobj A)} {e : edge (fobj A) a b} → emap (fmap f) e ≅ emap (fmap g) e lemma2 {A} {B} {f} {g} eq refl {a} {b} {e} with ( eq e ) ... | refl {h} eqv = lemma20 e (cmap g) (FMap (cmap f)) eqv isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap IsFunctor.identity isf = mrefl refl refl IsFunctor.distr isf = mrefl refl refl IsFunctor.≈-cong isf {a} {b} {f} {g} eq = mrefl (lemma1 {a} {b} {f} {g} eq ) (lemma2 {a} {b} {f} {g} eq (lemma1 {a} {b} {f} {g} eq )) --- --- 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 } ) --- --- --- ---