|
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 ( [_] )
|
|
841
|
13 open import Relation.Binary.Core
|
|
832
|
14 open Graph
|
|
|
15
|
|
|
16 data Objs : Set (c₁ ⊔ c₂) where
|
|
|
17 atom : (vertex G) → Objs
|
|
|
18 ⊤ : Objs
|
|
|
19 _∧_ : Objs → Objs → Objs
|
|
|
20 _<=_ : Objs → Objs → Objs
|
|
|
21
|
|
837
|
22 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i
|
|
832
|
23 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b)
|
|
|
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
|
|
844
|
31 ○ : ( a : Objs ) → Arrows a ⊤ --- case i
|
|
876
|
32 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii
|
|
837
|
33 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv
|
|
833
|
34
|
|
852
|
35 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
|
|
876
|
36 id a ・ g = g
|
|
853
|
37 ○ a ・ g = ○ _
|
|
876
|
38 < f , g > ・ h = < f ・ h , g ・ h >
|
|
|
39 iv f g ・ h = iv f ( g ・ h )
|
|
868
|
40
|
|
876
|
41 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
|
|
|
42 identityR {a} {a} {id a} = refl
|
|
|
43 identityR {a} {⊤} {○ a} = refl
|
|
|
44 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR
|
|
|
45 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
|
|
877
|
46 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
|
|
|
47 identityL = refl
|
|
|
48 associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
|
|
|
49 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
|
|
|
50 associative (id a) g h = refl
|
|
|
51 associative (○ a) g h = refl
|
|
|
52 associative < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (associative f g h) (associative f₁ g h)
|
|
|
53 associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h )
|
|
864
|
54
|
|
838
|
55 PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
|
|
|
56 PL = record {
|
|
|
57 Obj = Objs;
|
|
|
58 Hom = λ a b → Arrows a b ;
|
|
|
59 _o_ = λ{a} {b} {c} x y → x ・ y ;
|
|
876
|
60 _≈_ = λ x y → x ≡ y ;
|
|
838
|
61 Id = λ{a} → id a ;
|
|
|
62 isCategory = record {
|
|
|
63 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
|
|
842
|
64 identityL = λ {a b f} → identityL {a} {b} {f} ;
|
|
|
65 identityR = λ {a b f} → identityR {a} {b} {f} ;
|
|
|
66 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
838
|
67 associative = λ{a b c d f g h } → associative f g h
|
|
|
68 }
|
|
877
|
69 } where
|
|
|
70 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
|
|
|
71 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
|
|
|
72 o-resp-≈ refl refl = refl
|
|
|
73
|
|
|
74
|
|
|
75 eval : {a b : Objs } (f : Arrows a b ) → Arrows a b
|
|
|
76 eval (id a) = id a
|
|
|
77 eval (○ a) = ○ a
|
|
|
78 eval < f , f₁ > = < eval f , eval f₁ >
|
|
|
79 eval (iv f (id a)) = iv f (id a)
|
|
|
80 eval (iv f (○ a)) = iv f (○ a)
|
|
|
81 eval (iv π < g , h >) = eval g
|
|
|
82 eval (iv π' < g , h >) = eval h
|
|
|
83 eval (iv ε < g , h >) = iv ε < eval g , eval h >
|
|
|
84 eval (iv (f *) < g , h >) = iv (f *) < eval g , eval h >
|
|
|
85 eval (iv f (iv g h)) with eval (iv g h)
|
|
|
86 eval (iv f (iv g h)) | id a = iv f (id a)
|
|
|
87 eval (iv f (iv g h)) | ○ a = iv f (○ a)
|
|
|
88 eval (iv π (iv g h)) | < t , t₁ > = t
|
|
|
89 eval (iv π' (iv g h)) | < t , t₁ > = t₁
|
|
|
90 eval (iv ε (iv g h)) | < t , t₁ > = iv ε < t , t₁ >
|
|
|
91 eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ >
|
|
|
92 eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t)
|
|
|
93
|
|
879
|
94 refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → f ≡ f1
|
|
|
95 refl-<l> refl = refl
|
|
|
96
|
|
|
97 refl-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c } → < f , g > ≡ < f1 , g1 > → g ≡ g1
|
|
|
98 refl-<r> refl = refl
|
|
|
99
|
|
880
|
100 idem-eval : {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
|
|
|
101 idem-eval (id a) = refl
|
|
|
102 idem-eval (○ a) = refl
|
|
|
103 idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
|
|
|
104 idem-eval (iv f (id a)) = refl
|
|
|
105 idem-eval (iv f (○ a)) = refl
|
|
|
106 idem-eval (iv π < g , g₁ >) = idem-eval g
|
|
|
107 idem-eval (iv π' < g , g₁ >) = idem-eval g₁
|
|
|
108 idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁)
|
|
|
109 idem-eval (iv (x *) < f , f₁ >) = cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁)
|
|
|
110 idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) | inspect eval (iv g h)
|
|
|
111 idem-eval (iv f (iv g h)) | id a | m | _ = refl
|
|
|
112 idem-eval (iv f (iv g h)) | ○ a | m | _ = refl
|
|
|
113 idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> m
|
|
|
114 idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> m
|
|
|
115 idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv ε k ) m
|
|
|
116 idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv (f *) k ) m
|
|
|
117 idem-eval (iv f (iv g h)) | iv f₁ t | m | record { eq = ee } = trans lemma (cong ( λ k → iv f k ) m ) where
|
|
|
118 lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t))
|
|
|
119 lemma = {!!}
|
|
|
120
|
|
877
|
121 PL1 : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
|
|
|
122 PL1 = record {
|
|
|
123 Obj = Objs;
|
|
|
124 Hom = λ a b → Arrows a b ;
|
|
|
125 _o_ = λ{a} {b} {c} x y → x ・ y ;
|
|
|
126 _≈_ = λ x y → eval x ≡ eval y ;
|
|
|
127 Id = λ{a} → id a ;
|
|
|
128 isCategory = record {
|
|
|
129 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
|
|
|
130 identityL = λ {a b f} → cong (λ k → eval k ) (identityL {a} {b} {f});
|
|
|
131 identityR = λ {a b f} → cong (λ k → eval k ) (identityR {a} {b} {f});
|
|
878
|
132 o-resp-≈ = λ {a b c f g h i} → ore {a} {b} {c} f g h i ;
|
|
877
|
133 associative = λ{a b c d f g h } → cong (λ k → eval k ) (associative f g h )
|
|
|
134 }
|
|
|
135 } where
|
|
880
|
136 iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
|
|
881
|
137 iv-e = {!!}
|
|
|
138 iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c ) ( g : Arrows a (atom b) )
|
|
|
139 → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
|
|
|
140 iv-e-arrow x (id (atom _)) = refl
|
|
|
141 iv-e-arrow x (iv f g) with eval (iv f g)
|
|
|
142 iv-e-arrow x (iv f g) | id (atom _) = refl
|
|
|
143 iv-e-arrow x (iv f g) | iv f₁ t = refl
|
|
880
|
144 iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
|
|
|
145 iv-d (arrow x) g = begin
|
|
|
146 eval (iv (arrow x) g)
|
|
881
|
147 ≡⟨ iv-e-arrow x g ⟩
|
|
880
|
148 iv (arrow x) (eval g)
|
|
881
|
149 ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
|
|
|
150 iv (arrow x) (eval (eval g))
|
|
|
151 ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
|
|
880
|
152 eval (iv (arrow x) (eval g))
|
|
|
153 ∎ where open ≡-Reasoning
|
|
|
154 iv-d π (id _) = refl
|
|
|
155 iv-d π < g , g₁ > = sym (idem-eval g)
|
|
|
156 iv-d π (iv f g) = {!!}
|
|
|
157 iv-d π' (id _) = refl
|
|
|
158 iv-d π' < g , g₁ > = sym (idem-eval g₁)
|
|
|
159 iv-d π' (iv f g) = {!!}
|
|
|
160 iv-d ε g = {!!}
|
|
|
161 iv-d (x *) g = {!!}
|
|
|
162 d-eval : {A B C : Objs} (f : Arrows B C) (g : Arrows A B) →
|
|
|
163 eval (f ・ g) ≡ eval (eval f ・ eval g)
|
|
|
164 d-eval (id a) g = sym (idem-eval g)
|
|
|
165 d-eval (○ a) g = refl
|
|
|
166 d-eval < f , f₁ > g = cong₂ (λ j k → < j , k > ) (d-eval f g) (d-eval f₁ g)
|
|
|
167 d-eval (iv x (id a)) g = iv-d x g
|
|
|
168 d-eval (iv (x *) (○ a)) g = {!!}
|
|
|
169 d-eval (iv π < f , f₁ >) g = d-eval f g
|
|
|
170 d-eval (iv π' < f , f₁ >) g = d-eval f₁ g
|
|
|
171 d-eval (iv ε < f , f₁ >) g = {!!}
|
|
|
172 d-eval (iv (x *) < f , f₁ >) g = {!!}
|
|
|
173 d-eval (iv x (iv f f₁)) g = {!!}
|
|
878
|
174 ore : {A B C : Objs} (f g : Arrows A B) (h i : Arrows B C) →
|
|
877
|
175 eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g)
|
|
880
|
176 ore f g h i f=g h=i = begin
|
|
|
177 eval (h ・ f)
|
|
|
178 ≡⟨ d-eval h f ⟩
|
|
|
179 eval (eval h ・ eval f)
|
|
|
180 ≡⟨ cong₂ (λ j k → eval ( j ・ k )) h=i f=g ⟩
|
|
|
181 eval (eval i ・ eval g)
|
|
|
182 ≡⟨ sym ( d-eval i g ) ⟩
|
|
|
183 eval (i ・ g)
|
|
|
184 ∎ where open ≡-Reasoning
|
|
|
185
|
|
877
|
186
|
|
|
187 fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
|
|
878
|
188 fmap f = {!!}
|
|
877
|
189
|
|
|
190 PLCCC : Functor PL PL
|
|
|
191 PLCCC = record {
|
|
|
192 FObj = λ x → x
|
|
878
|
193 ; FMap = fmap
|
|
877
|
194 ; isFunctor = record {
|
|
|
195 identity = {!!}
|
|
|
196 ; distr = {!!}
|
|
|
197 ; ≈-cong = {!!}
|
|
|
198 }
|
|
|
199 }
|
