|
832
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module CCCgraph1 where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
838
|
7 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
832
|
8 open import CCC
|
|
|
9 open import graph
|
|
|
10
|
|
|
11 module ccc-from-graph {c₁ c₂ : Level} (G : Graph {c₁} {c₂} ) where
|
|
838
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
832
|
13 open Graph
|
|
|
14
|
|
|
15 data Objs : Set (c₁ ⊔ c₂) where
|
|
|
16 atom : (vertex G) → Objs
|
|
|
17 ⊤ : Objs
|
|
|
18 _∧_ : Objs → Objs → Objs
|
|
|
19 _<=_ : Objs → Objs → Objs
|
|
|
20
|
|
837
|
21 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i
|
|
832
|
22 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b)
|
|
|
23 ○ : (a : Objs ) → Arrow a ⊤
|
|
|
24 π : {a b : Objs } → Arrow ( a ∧ b ) a
|
|
|
25 π' : {a b : Objs } → Arrow ( a ∧ b ) b
|
|
|
26 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
|
|
837
|
27 _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) --- case v
|
|
832
|
28
|
|
|
29 data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) where
|
|
837
|
30 id : ( a : Objs ) → Arrows a a --- case i
|
|
|
31 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) --- case iii
|
|
|
32 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv
|
|
833
|
33
|
|
834
|
34 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
|
|
837
|
35 id a ・ g = g
|
|
838
|
36 < f , g > ・ h = < f ・ h , g ・ h >
|
|
837
|
37 iv f (id _) ・ h = iv f h
|
|
839
|
38 iv (○ a) g ・ h = iv (○ _) (id _)
|
|
837
|
39 iv π < g , g₁ > ・ h = g ・ h
|
|
|
40 iv π' < g , g₁ > ・ h = g₁ ・ h
|
|
|
41 iv ε < g , g₁ > ・ h = iv ε < g ・ h , g₁ ・ h >
|
|
838
|
42 iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h >
|
|
837
|
43 iv f (iv f₁ g) ・ h = iv f ( (iv f₁ g) ・ h )
|
|
832
|
44
|
|
838
|
45 PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
|
|
|
46 PL = record {
|
|
|
47 Obj = Objs;
|
|
|
48 Hom = λ a b → Arrows a b ;
|
|
|
49 _o_ = λ{a} {b} {c} x y → x ・ y ;
|
|
|
50 _≈_ = λ x y → x ≡ y ;
|
|
|
51 Id = λ{a} → id a ;
|
|
|
52 isCategory = record {
|
|
|
53 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
|
|
|
54 identityL = identityL;
|
|
|
55 identityR = identityR ;
|
|
|
56 o-resp-≈ = o-resp-≈ ;
|
|
|
57 associative = λ{a b c d f g h } → associative f g h
|
|
|
58 }
|
|
|
59 } where
|
|
|
60 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
|
|
839
|
61 identityL {_} {_} {id a} = refl
|
|
|
62 identityL {a} {b} {< f , f₁ >} = refl
|
|
|
63 identityL {_} {_} {iv f f₁} = refl
|
|
838
|
64 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
|
|
839
|
65 identityR {a} {_} {id a} = refl
|
|
|
66 identityR {a} {b} {< f , g >} = cong₂ ( λ j k → < j , k > ) ( identityR {_} {_} {f} ) ( identityR {_} {_} {g} )
|
|
838
|
67 identityR {a} {b} {iv x f} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
|
|
|
68 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
|
|
|
69 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
|
|
|
70 o-resp-≈ refl refl = refl
|
|
|
71 associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
|
|
|
72 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
|
|
839
|
73 associative (id a) g h = refl
|
|
|
74 associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
|
|
|
75 associative (iv x f) g h = ? -- cong ( λ k → iv x k ) ( associative f g h )
|
|
838
|
76
|
