Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 817:177162990879

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Apr 2019 12:37:34 +0900
parents CCChom.agda@4e48b331020a
children bc244fc604c8
comparison
equal deleted inserted replaced
816:4e48b331020a 817:177162990879
1 open import Level
2 open import Category
3 module CCCgraph where
4
5 open import HomReasoning
6 open import cat-utility
7 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> )
8 open import Category.Constructions.Product
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10 open import CCC
11
12 open Functor
13
14 -- ccc-1 : Hom A a 1 ≅ {*}
15 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
16 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
17
18 open import Category.Sets
19
20 -- Sets is a CCC
21
22 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
23
24 data One {l : Level} : Set l where
25 OneObj : One -- () in Haskell ( or any one object set )
26
27 sets : {l : Level } → CCC (Sets {l})
28 sets {l} = record {
29 １ = One
30 ; ○ = λ _ → λ _ → OneObj
31 ; _∧_ = _∧_
32 ; <_,_> = <,>
33 ; π = π
34 ; π' = π'
35 ; _<=_ = _<=_
36 ; _* = _*
37 ; ε = ε
38 ; isCCC = isCCC
39 } where
40 １ : Obj Sets
41 １ = One
42 ○ : (a : Obj Sets ) → Hom Sets a １
43 ○ a = λ _ → OneObj
44 _∧_ : Obj Sets → Obj Sets → Obj Sets
45 _∧_ a b = a /\ b
46 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
47 <,> f g = λ x → ( f x , g x )
48 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
49 π {a} {b} = proj₁
50 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
51 π' {a} {b} = proj₂
52 _<=_ : (a b : Obj Sets ) → Obj Sets
53 a <= b = b → a
54 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
55 f * = λ x → λ y → f ( x , y )
56 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
57 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
58 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε
59 isCCC = record {
60 e2 = e2
61 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
62 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
63 ; e3c = e3c
64 ; π-cong = π-cong
65 ; e4a = e4a
66 ; e4b = e4b
67 ; *-cong = *-cong
68 } where
69 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ]
70 e2 {a} {f} = extensionality Sets ( λ x → e20 x )
71 where
72 e20 : (x : a ) → f x ≡ ○ a x
73 e20 x with f x
74 e20 x | OneObj = refl
75 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
76 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
77 e3a = refl
78 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
79 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
80 e3b = refl
81 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
82 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
83 e3c = refl
84 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
85 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
86 π-cong refl refl = refl
87 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
88 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
89 e4a = refl
90 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
91 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
92 e4b = refl
93 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
94 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
95 *-cong refl = refl
96
97 module ccc-from-graph where
98
99 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
100 open import discrete
101 open graphtocat
102
103 open Graph
104
105 data Objs (G : Graph ) : Set where -- formula
106 atom : (vertex G) → Objs G
107 ⊤ : Objs G
108 _∧_ : Objs G → Objs G → Objs G
109 _<=_ : Objs G → Objs G → Objs G
110
111 data Arrow (G : Graph ) : Objs G → Objs G → Set where --- proof
112 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b)
113 ○ : (a : Objs G ) → Arrow G a ⊤
114 π : {a b : Objs G } → Arrow G ( a ∧ b ) a
115 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
116 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
117 <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
118 _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
119
120 record SM {v : Level} : Set (suc v) where
121 field
122 graph : Graph {v}
123 sobj : vertex graph → Set
124 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b
125
126 open SM
127
128 -- positive intutionistic calculus
129 PL : (G : SM) → Graph
130 PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) }
131 DX : (G : SM) → Category Level.zero Level.zero Level.zero
132 DX G = GraphtoCat (PL G)
133
134 -- open import Category.Sets
135 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
136
137 fobj : {G : SM} ( a : Objs (graph G) ) → Set
138 fobj {G} (atom x) = sobj G x
139 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
140 fobj {G} (a <= b) = fobj {G} b → fobj {G} a
141 fobj ⊤ = One
142 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
143 amap {G} (arrow x) = smap G x
144 amap (○ a) _ = OneObj
145 amap π ( x , _) = x
146 amap π'( _ , x) = x
147 amap ε ( f , x ) = f x
148 amap < f , g > x = (amap f x , amap g x)
149 amap (f *) x = λ y → amap f ( x , y )
150 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
151 fmap {G} {a} (id a) = λ z → z
152 fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
153
154 -- CS is a map from Positive logic to Sets
155 -- Sets is CCC, so we have a cartesian closed category generated by a graph
156 -- as a sub category of Sets
157
158 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
159 FObj (CS G) a = fobj a
160 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
161 isFunctor (CS G) = isf where
162 _++_ = Category._o_ (DX G)
163 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
164 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)
165 distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
166 adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
167 ( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z ≡ fmap ( next x g ) (fmap f z )
168 adistr eq x = cong ( λ k → amap x k ) eq
169 distr {a} {b} {b} {f} {id b} z = refl
170 isf : IsFunctor (DX G) Sets fobj fmap
171 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
172 IsFunctor.≈-cong isf refl = refl
173 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
174
175 --- record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
176 --- field
177 --- cat : Category c₁ c₂ ℓ
178 --- ccc : CCC cat
179 ---
180 --- open CCCObj
181 ---
182 --- record CCCMap {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
183 --- field
184 --- cmap : Functor (cat A ) (cat B )
185 --- ccf : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
186 ---
187 --- Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
188 --- Cart {c₁} {c₂} {ℓ} = record {
189 --- Obj = CCCObj {c₁} {c₂} {ℓ}
190 --- ; Hom = CCCMap
191 --- ; _o_ = {!!}
192 --- ; _≈_ = {!!}
193 --- ; Id = {!!}
194 --- ; isCategory = record {
195 --- identityL = {!!}
196 --- ; identityR = {!!}
197 --- ; o-resp-≈ = {!!}
198 --- ; associative = {!!}
199 --- }}
200 ---
201 --- open import discrete
202 --- open Graph
203 ---
204 --- record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
205 --- vmap : vertex x → vertex y
206 --- emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
207 ---
208 --- Grp : {v : Level} → Category (suc v) v v
209 --- Grp {v} = record {
210 --- Obj = Graph {v}
211 --- ; Hom = {!!}
212 --- ; _o_ = {!!}
213 --- ; _≈_ = {!!}
214 --- ; Id = {!!}
215 --- ; isCategory = record {
216 --- identityL = {!!}
217 --- ; identityR = {!!}
218 --- ; o-resp-≈ = {!!}
219 --- ; associative = {!!}
220 --- }}
221 ---
222 --- UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁})
223 --- UX = {!!}
224 ---
225 --- open ccc-from-graph
226 ---
227 --- sm : {v : Level } → Graph {v} → SM {v}
228 --- SM.graph (sm g) = g
229 --- SM.sobj (sm g) = {!!}
230 --- SM.smap (sm g) = {!!}
231 ---
232 --- HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v})
233 --- HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ; ccc = sets } )
234 ---
235 ---
236 ---
237 ---