Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 821:fbbc9c03bfed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Grp and Cart
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 May 2019 15:16:54 +0900
parents 658daaa74df3
children 4c0580d9dda4
comparison
equal deleted inserted replaced
820:658daaa74df3 821:fbbc9c03bfed
100 open import discrete 100 open import discrete
101 open graphtocat 101 open graphtocat
102 102
103 open Graph 103 open Graph
104 104
105 data Objs (G : Graph ) : Set where -- formula 105 data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where -- formula
106 atom : (vertex G) → Objs G 106 atom : (vertex G) → Objs G
107 ⊤ : Objs G 107 ⊤ : Objs G
108 _∧_ : Objs G → Objs G → Objs G 108 _∧_ : Objs G → Objs G → Objs G
109 _<=_ : Objs G → Objs G → Objs G 109 _<=_ : Objs G → Objs G → Objs G
110 110
166 166
167 167
168 168
169 record SM {v : Level} : Set (suc v) where 169 record SM {v : Level} : Set (suc v) where
170 field 170 field
171 graph : Graph {v} 171 graph : Graph {v} {v}
172 sobj : vertex graph → Set 172 sobj : vertex graph → Set
173 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b 173 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b
174 174
175 open SM 175 open SM
176 176
257 ; isCategory = record { 257 ; isCategory = record {
258 isEquivalence = λ {A} {B} → record { 258 isEquivalence = λ {A} {B} → record {
259 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} 259 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f}
260 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} 260 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g}
261 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } 261 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} }
262 ; identityL = let open ≈-Reasoning (CAT) in idL {_} {_} {_} {_} {_} 262 ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_}
263 ; identityR = let open ≈-Reasoning (CAT) in idR 263 ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f}
264 ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory CAT) 264 ; 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}
265 ; associative = let open ≈-Reasoning (CAT) in assoc 265 ; 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}
266 }} where 266 }} where
267 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 267 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
268 cart-refl {A} {B} {x} {a} {b} f = [_]_~_.refl ( IsFunctor.≈-cong (isFunctor ( cmap x )) 268 cart-refl {A} {B} {x} {a} {b} f = [_]_~_.refl ( IsFunctor.≈-cong (isFunctor ( cmap x ))
269 ( IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory ( cat A ))))) 269 ( IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory ( cat A )))))
270 _・_ : { A B C : CCCObj {c₁} {c₂} {ℓ} } → ( f : CCCMap B C ) → ( g : CCCMap A B ) → CCCMap A C 270 _・_ : { A B C : CCCObj {c₁} {c₂} {ℓ} } → ( f : CCCMap B C ) → ( g : CCCMap A B ) → CCCMap A C
275 ccmap ca = ccf f ( ccf g (ccc A )) 275 ccmap ca = ccf f ( ccf g (ccc A ))
276 276
277 open import discrete 277 open import discrete
278 open Graph 278 open Graph
279 279
280 record GMap {v : Level} (x y : Graph {v} ) : Set (suc v) where 280 record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc v ⊔ v' ) where
281 field 281 field
282 vmap : vertex x → vertex y 282 vmap : vertex x → vertex y
283 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) 283 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
284 284
285 open GMap 285 open GMap
286 286
287 Grp : {v : Level} → Category (suc v) (suc v) v 287 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
288 Grp {v} = record { 288
289 Obj = Graph {v} 289 data _=m=_ {v v' : Level} {x y : Graph {v} {v'}} ( f g : GMap x y ) : Set (v ⊔ v' ) where
290 ; Hom = GMap {v} 290 mrefl : ( vmap f ≡ vmap g ) → ( {a b : vertex x} → { e : edge x a b } → emap f e ≅ emap g e ) → f =m= g
291 ; _o_ = λ f g → record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } 291
292 ; _≈_ = λ {a} {b} f g → {!!} 292 _&_ : {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
293 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
294
295 Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (v ⊔ v')
296 Grp {v} {v'} = record {
297 Obj = Graph {v} {v'}
298 ; Hom = GMap {v} {v'}
299 ; _o_ = _&_
300 ; _≈_ = _=m=_
293 ; Id = record { vmap = λ y → y ; emap = λ f → f } 301 ; Id = record { vmap = λ y → y ; emap = λ f → f }
294 ; isCategory = record { 302 ; isCategory = record {
295 identityL = {!!} 303 isEquivalence = λ {A} {B} → ise {v} {v'} {A} {B}
296 ; identityR = {!!} 304 ; identityL = mrefl refl refl
297 ; o-resp-≈ = {!!} 305 ; identityR = mrefl refl refl
298 ; associative = {!!} 306 ; o-resp-≈ = m--resp-≈
299 }} 307 ; associative = mrefl refl refl
300 308 }} where
301 --- UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁}) 309 msym : {v v' : Level} {x y : Graph {v} {v'} } { f g : GMap x y } → f =m= g → g =m= f
302 --- UX = {!!} 310 msym (mrefl refl eq ) = mrefl refl ( ≅-sym eq )
311 mtrans : {v v' : Level} {x y : Graph {v} {v'}} { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
312 mtrans (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( ≅-trans eq eq1 )
313 ise : {v v' : Level} {x y : Graph {v} {v'}} → IsEquivalence {_} {v ⊔ v'} {_} ( _=m=_ {v} {v'} {x} {y} )
314 ise = record {
315 refl = λ {x} → mrefl refl refl
316 ; sym = msym
317 ; trans = mtrans
318 }
319 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 )
320 m--resp-≈ {_} {_} {_} {_} {f} {g} {h} {i} (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( λ {a} {b} {e} → begin
321 emap h (emap f e)
322 ≅⟨ ≅-cong ( λ k → emap h k ) eq ⟩
323 emap h (emap g e)
324 ≅⟨ eq1 ⟩
325 emap i (emap g e)
326 ∎ )
327 where open Relation.Binary.HeterogeneousEquality.≅-Reasoning
328 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 )
329 assoc-≈ = mrefl refl refl
330
331 --- Forgetful functor
332
333 fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grp {c₁} {c₂})
334 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
335 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
336 fmap f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
337
338 UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
339 FObj (UX {c₁} {c₂} {ℓ}) a = fobj a
340 FMap UX f = fmap f
341 isFunctor (UX {c₁} {c₂} {ℓ}) = isf where
342 isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
343 IsFunctor.identity isf = mrefl refl refl
344 IsFunctor.distr isf = mrefl refl refl
345 IsFunctor.≈-cong isf eq = mrefl {!!} {!!}
346
303 --- 347 ---
304 --- open ccc-from-graph 348 --- open ccc-from-graph
305 --- 349 ---
306 --- sm : {v : Level } → Graph {v} → SM {v} 350 --- sm : {v : Level } → Graph {v} → SM {v}
307 --- SM.graph (sm g) = g 351 --- SM.graph (sm g) = g