Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 903:2f0ffd5733a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Positive Logic with equivalence
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 30 Apr 2020 17:42:12 +0900
parents 6633314ba902
children 3e164b00155f
comparison
equal deleted inserted replaced
902:6633314ba902 903:2f0ffd5733a8
132 id a ・ g = g 132 id a ・ g = g
133 ○ a ・ g = ○ _ 133 ○ a ・ g = ○ _
134 < f , g > ・ h = < f ・ h , g ・ h > 134 < f , g > ・ h = < f ・ h , g ・ h >
135 iv f g ・ h = iv f ( g ・ h ) 135 iv f g ・ h = iv f ( g ・ h )
136 136
137 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f 137 data _≐_ : {a b : Objs } → Arrows a b → Arrows a b → Set ℓ where
138 identityR {a} {a} {id a} = refl 138 prefl : {a b : Objs } → {f : Arrows a b } → f ≐ f
139 identityR {a} {⊤} {○ a} = refl 139 p⊤ : {a : Objs } → {f g : Arrows a ⊤ } → f ≐ g
140 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR 140 <p> : {a b c : Objs } → {f h : Arrows a b } {g i : Arrows a c } → f ≐ h → g ≐ i → < f , g > ≐ < h , i >
141 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR 141 piv : {a b c : Objs } → {f : Arrow b c } {g i : Arrows a b } → g ≐ i → iv f g ≐ iv f i
142 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f 142 aiv : { a : Objs } {b c : vertex G } → {f h : edge G b c } → {g i : Arrows a (atom b) } → _≅_ G f h → g ≐ i → iv (arrow f) g ≐ iv (arrow h) i
143 identityL = refl 143
144 associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → 144 psym : {a b : Objs } → { f g : Arrows a b} → f ≐ g → g ≐ f
145 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) 145 psym prefl = prefl
146 associative (id a) g h = refl 146 psym p⊤ = p⊤
147 associative (○ a) g h = refl 147 psym (<p> eq eq₁) = <p> (psym eq) (psym eq₁)
148 associative < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (associative f g h) (associative f₁ g h) 148 psym (piv eq) = piv (psym eq)
149 associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h ) 149 psym (aiv x eq) = aiv (IsEquivalence.sym (Graph.isEq G) x) (psym eq)
150
151 ptrans : {a b : Objs } → { f g h : Arrows a b} → f ≐ g → g ≐ h → f ≐ h
152 ptrans prefl g=h = g=h
153 ptrans p⊤ g=h = p⊤
154 ptrans (<p> f=g f=g₁) prefl = <p> f=g f=g₁
155 ptrans (<p> f=g f=g₁) (<p> g=h g=h₁) = <p> ( ptrans f=g g=h ) ( ptrans f=g₁ g=h₁ )
156 ptrans (piv f=g) prefl = piv f=g
157 ptrans (piv f=g) p⊤ = p⊤
158 ptrans (piv f=g) (piv g=h) = piv ( ptrans f=g g=h )
159 ptrans (piv f=g) (aiv x g=h) = aiv x (ptrans f=g g=h)
160 ptrans (aiv x f=g) prefl = aiv x f=g
161 ptrans (aiv x f=g) (piv g=h) = aiv x (ptrans f=g g=h)
162 ptrans (aiv x f=g) (aiv x₁ g=h) = aiv (IsEquivalence.trans (Graph.isEq G) x x₁) (ptrans f=g g=h)
163
164 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≐ f
165 identityL = prefl
166
167 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≐ f
168 identityR {a} {a} {id a} = prefl
169 identityR {a} {⊤} {○ a} = p⊤
170 identityR {a} {_} {< f , f₁ >} = <p> identityR identityR
171 identityR {a} {b} {iv f g} = piv identityR
172
173 assoc≐ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
174 (f ・ (g ・ h)) ≐ ((f ・ g) ・ h)
175 assoc≐ (id a) g h = prefl
176 assoc≐ (○ a) g h = p⊤
177 assoc≐ < f , f₁ > g h = <p> (assoc≐ f g h) (assoc≐ f₁ g h)
178 assoc≐ (iv f f1) g h = piv ( assoc≐ f1 g h )
150 179
151 -- positive intutionistic calculus 180 -- positive intutionistic calculus
152 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) 181 PL : Category c₁ (c₁ ⊔ c₂) ℓ
153 PL = record { 182 PL = record {
154 Obj = Objs; 183 Obj = Objs;
155 Hom = λ a b → Arrows a b ; 184 Hom = λ a b → Arrows a b ;
156 _o_ = λ{a} {b} {c} x y → x ・ y ; 185 _o_ = λ{a} {b} {c} x y → x ・ y ;
157 _≈_ = λ x y → x ≡ y ; 186 _≈_ = λ x y → x ≐ y ;
158 Id = λ{a} → id a ; 187 Id = λ{a} → id a ;
159 isCategory = record { 188 isCategory = record {
160 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; 189 isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym} ;
161 identityL = λ {a b f} → identityL {a} {b} {f} ; 190 identityL = λ {a b f} → identityL {a} {b} {f} ;
162 identityR = λ {a b f} → identityR {a} {b} {f} ; 191 identityR = λ {a b f} → identityR {a} {b} {f} ;
163 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; 192 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
164 associative = λ{a b c d f g h } → associative f g h 193 associative = λ{a b c d f g h } → assoc≐ f g h
165 } 194 }
166 } where 195 } where
167 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → 196 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
168 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) 197 f ≐ g → h ≐ i → (h ・ f) ≐ (i ・ g)
169 o-resp-≈ refl refl = refl 198 o-resp-≈ {_} {_} {⊤} {f} {g} {h} {i} f=g h=i = p⊤
199 o-resp-≈ {_} {_} {_} {f} {g} {id a} {id a} f=g h=i = ptrans (ptrans f=g (psym identityR) ) identityR
200 o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< h , h₁ >} f=g prefl = <p> (o-resp-≈ f=g prefl ) (o-resp-≈ f=g prefl )
201 o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< i , i₁ >} f=g (<p> h=i h=i₁) = <p> (o-resp-≈ f=g h=i ) (o-resp-≈ f=g h=i₁)
202 o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ h} f=g prefl = piv ( o-resp-≈ f=g prefl )
203 o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ i} f=g (piv h=i) = piv ( o-resp-≈ f=g h=i)
204 o-resp-≈ {_} {_} {_} {f} {g} {iv (arrow x) h} {iv (arrow y) i} f=g (aiv x=y h=i) = aiv x=y (o-resp-≈ f=g h=i)
170 205
171 -------- 206 --------
172 -- 207 --
173 -- Functor from Positive Logic to Sets 208 -- Functor from Positive Logic to Sets
174 -- 209 --
219 adistr : fmap (g + f) z ≡ fmap g (fmap f z) → 254 adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
220 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) 255 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z )
221 adistr eq x = cong ( λ k → amap x k ) eq 256 adistr eq x = cong ( λ k → amap x k ) eq
222 isf : IsFunctor PL Sets fobj fmap 257 isf : IsFunctor PL Sets fobj fmap
223 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) 258 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
224 IsFunctor.≈-cong isf refl = refl 259 IsFunctor.≈-cong isf = {!!}
225 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 260 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
226 261
227 open import subcat 262 open import subcat
228 263
229 CSC = FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) CS 264 CSC = FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) CS