Members/kono/Proof/category: CCCGraph.agda comparison

comparison CCCGraph.agda @ 911:b8c5f15ee561

small graph and small category on CCC to graph

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 02 May 2020 03:40:56 +0900
parents	8f41ad966eaa
children	635418b4b2f3

comparison

equal deleted inserted replaced

-:8f41ad966eaa
+:b8c5f15ee561
 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 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
+data Objs : Set c₁ where
-atom : (vertex G) → Objs G
+atom : (vertex G) → Objs
-⊤ : Objs G
+⊤ : Objs
-_∧_ : Objs G → Objs G → Objs G
+_∧_ : Objs  → Objs  → Objs
-_<=_ : Objs G → Objs G → Objs G
+_<=_ : Objs → Objs → Objs
-data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
+data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ )
-arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
+data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
-○ : (a : Objs G ) → Arrow G a ⊤
+arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-π : {a b : Objs G } → Arrow G ( a ∧ b ) a
+π : {a b : Objs } → Arrow ( a ∧ b ) a
-π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
+π' : {a b : Objs } → Arrow ( a ∧ b ) b
-ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
+ε : {a b : Objs } → Arrow ((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 } → Arrows (c ∧ b ) a → Arrow c ( a <= b )        --- case v
-_* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
+data  Arrows where
-data one {v : Level} {S : Set v} : Set v where
+id : ( a : Objs ) → Arrows a a                                      --- case i
-elm : (x : S ) → one
+○ : ( a : Objs ) → Arrows a ⊤                                       --- case i
+<_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b)      -- case iii
-iso→ : {v : Level} {S : Set v} → one → S
+iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
-iso→ (elm x) = x
+_・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where
+id a ・ g = g
-elmeq : {x : S} →  iso←  ( elm x ) x
+○ a ・ g = ○ _
+< f , g > ・ h = < f ・ h , g ・ h >
-iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a
+iv f g ・ h = iv f ( g ・ h )
-iso-left (elm x) .x elmeq = refl
+identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
-iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x )
+identityL = refl
-iso-right (elm x) = elmeq
+identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
---   record one {v : Level} {S : Set v} : Set (suc v) where
+identityR {a} {a} {id a} = refl
---      field
+identityR {a} {⊤} {○ a} = refl
---         elm : S
+identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR
+identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
+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 )
+-- 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
+-- Functor from Positive Logic to Sets
---   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₂
+-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂
-fobj : {G : SM} ( a  : Objs (graph G) ) → Set
+C = graphtocat.Chain G
-fobj {G} (atom x) = sobj G x
-fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
+tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
-fobj {G} (a <= b) = fobj {G} b → fobj {G} a
+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
-amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
+fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
-amap {G} (arrow x) = smap G x
+fobj  (a <= b) = fobj  b → fobj  a
-amap (○ a) _ = OneObj
-amap π ( x , _) = x
+fmap :  { a b : Objs  } → Hom PL a b → fobj  a → fobj  b
-amap π'( _ , x) = x
+amap :  { a b : Objs  } → Arrow  a b → fobj  a → fobj  b
-amap ε ( f , x ) = f x
+amap  (arrow x) =  tr x
-amap < f , g > x = (amap f x , amap g x)
+amap π ( x , y ) = x
-amap (f *) x = λ y → amap f ( x , y )
+amap π' ( x , y ) = y
-fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
+amap ε (f , x ) = f x
-fmap {G} {a} (id a) = λ z → z
+amap (f *) x = λ y →  fmap f ( x , y )
-fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
+fmap (id a) x = x
+fmap (○ a) x = OneObj
---   CS is a map from Positive logic to Sets
+fmap < f , g > x = ( fmap f x , fmap g x )
---    Sets is CCC, so we have a cartesian closed category generated by a graph
+fmap (iv x f) a = amap x ( fmap f a )
---       as a sub category of Sets
+--   CS is a map from Positive logic to Sets
-CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
+--    Sets is CCC, so we have a cartesian closed category generated by a graph
-FObj (CS G) a  = fobj a
+--       as a sub category of Sets
-FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
-isFunctor (CS G) = isf where
+CS :  Functor PL (Sets {c₁ ⊔ c₂ })
-_++_ = Category._o_ (DX G)
+FObj CS a  = fobj  a
-++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
+FMap CS {a} {b} f = fmap  {a} {b} f
-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)
+isFunctor CS = isf where
-distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
+_+_ = Category._o_ PL
-adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
+++idR = IsCategory.identityR ( Category.isCategory PL )
-( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
+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)
-adistr eq x = cong ( λ k → amap x k ) eq
+distr {a} {a₁} {a₁} {f} {id a₁} z = refl
-distr {a} {b} {b} {f} {id b} z =  refl
+distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
-isf : IsFunctor (DX G) Sets fobj fmap
+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)
-IsFunctor.identity isf = extensionality Sets ( λ x → refl )
+distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where
-IsFunctor.≈-cong isf refl = refl
+adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
-IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {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 )
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap
 ---
 ---     CCC ( SC (CS G)) Sets   have to be proved
 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
 record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
 }}
 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)
 open GMap
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 _&_ :  {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'))
+Grph : {v v' : Level} → Category (suc (v ⊔ v')) (v ⊔ v') (suc ( v ⊔ v'))
-Grp {v} {v'} = record {
+Grph {v} {v'} = record {
 Obj = Graph {v} {v'}
 ; Hom = GMap {v} {v'}
 ; _o_ = _&_
 ; _≈_ = _=m=_
 ; Id  = record { vmap = λ y → y ; emap = λ f → f }
 g
 ≈⟨ g=g' ⟩
 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  )
+UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}  )
-→ Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
+FObj UX a = fobj a
-FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
+FMap UX f =  fmap f
-FMap (UX ≈-to-≡)  f =  fmap f
+isFunctor UX  = isf where
-isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
+isf : IsFunctor Cart Grph fobj fmap
--- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
+IsFunctor.identity isf {a} {b} {f} e = mrefl refl
-open import HomReasoning
+IsFunctor.distr isf {a} {b} {c} f = mrefl refl
-isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
+IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 (
-IsFunctor.identity isf {a} {b} {f} e = mrefl refl
+≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
-IsFunctor.distr isf f = mrefl refl
+)))) (f=g e) where
-IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 (
+lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
-≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
+lemma4 (refl eqv) = refl
-))) (eq e) where
+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
-lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
+lemma refl (refl eqv) = mrefl (≡←≈ b eqv)
-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 )
+open ccc-from-graph.Objs
+open ccc-from-graph.Arrow
+open ccc-from-graph.Arrows
----
+open graphtocat.Chain
----   open ccc-from-graph
----
+ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁}  ) (Cart {c₁} {c₁} {c₁} ) UX
----   sm : {v : Level } → Graph {v} → SM {v}
+ccc-graph-univ {c₁}   = record {
----   SM.graph (sm g) = g
+F = λ g → csc g ;
----   SM.sobj (sm  g) = {!!}
+η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) } ;
----   SM.smap (sm  g) = {!!}
+_* = {!!} ;
----
+isUniversalMapping = record {
----   HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v})
+universalMapping = {!!} ;
----   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
+uniquness = {!!}
----
+}
----
+} where
----
+csc : Graph → Obj Cart
----
+csc g = record { cat = {!!} ; ccc = {!!} } where
+open ccc-from-graph g

Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 911:b8c5f15ee561