Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 548:03b851adc4fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Apr 2017 22:04:38 +0900
parents c0078b03201c
children adef39d19884
comparison
equal deleted inserted replaced
547:c0078b03201c 548:03b851adc4fb
174 snmap : ( i : OC ) → sobj i 174 snmap : ( i : OC ) → sobj i
175 sncommute : { i j : OC } → ( f : I ) → smap f ( snmap i ) ≡ snmap j 175 sncommute : { i j : OC } → ( f : I ) → smap f ( snmap i ) ≡ snmap j
176 176
177 open snat 177 open snat
178 178
179 snat1 : { c₂ : Level } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I )→ sobj i → sobj j ) 179 snmeq : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j }
180 ( snm : ( i : OC ) → sobj i ) → (( snm1 : ( i : OC ) → sobj i ) ( i j : OC ) → (f : I ) → smap f ( snm1 i ) ≡ snm1 j ) → snat sobj smap 180 ( s t : snat SO SM ) → ( i : OC ) →
181 snat1 SO SM snm eq = record { snmap = λ i → snm i ; sncommute = λ {i} {j} f → eq snm i j f } 181 { snmapsi snmapti : SO i } → snmapsi ≡ snmapti → SO i
182 snmeq s t i {pi} {.pi} refl = pi
183
184 snmc : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j }
185 ( s t : snat SO SM ) → { i j : OC } → { f : I } →
186 { snmapsi snmapti : SO i } → (eqi : snmapsi ≡ snmapti ) →
187 { snmapsj snmaptj : SO j } → (eqj : snmapsj ≡ snmaptj )
188 → ( SM f ( snmapsi ) ≡ snmapsj )
189 → ( SM f ( snmapti ) ≡ snmaptj )
190 → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj)
191 snmc s t refl refl refl refl = refl
192
193 snmc1 : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j }
194 ( s t : snat SO SM ) → { i j : OC } → { f : I } →
195 { snmapsi snmapti : SO i } → (eqi : snmapsi ≡ snmapti ) →
196 { snmapsj snmaptj : SO j } → (eqj : snmapsj ≡ snmaptj )
197 → ( SM f ( snmapsi ) ≡ snmapsj )
198 → ( SM f ( snmapti ) ≡ snmaptj ) → ( snm : (i : OC ) → SO i ) →
199 SM f (snm i) ≡ snm j
200 snmc1 s t refl refl refl refl snm = {!!}
201
202 snat1 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j )
203 → ( s t : snat SO SM )
204 → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i )
205 → ( eq2 : ( i j : OC ) ( f : I ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j )
206 → ( eq3 : ( i j : OC ) ( f : I ) → SM {i} {j} f ( snmap t i ) ≡ snmap t j )
207 → snat SO SM
208 snat1 SO SM s t eq1 eq2 eq3 = record {
209 snmap = λ i → snmeq s t i (eq1 i ) ;
210 sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f )
211 }
182 212
183 ≡cong2 : { c : Level } { A B C : Set c } { a a' : A } { b b' : B } ( f : A → B → C ) 213 ≡cong2 : { c : Level } { A B C : Set c } { a a' : A } { b b' : B } ( f : A → B → C )
184 → a ≡ a' 214 → a ≡ a'
185 → b ≡ b' 215 → b ≡ b'
186 → f a b ≡ f a' b' 216 → f a b ≡ f a' b'
187 ≡cong2 _ refl refl = refl 217 ≡cong2 _ refl refl = refl
218
219 snmeqeqs : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j )
220 ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) →
221 snmeq s t i (eq1 i ) ≡ snmap s i
222 snmeqeqs SO SM s t i eq1 = lemma (eq1 i) refl where
223 lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapsi ≡ sm ) →
224 snmeq s t i eq1 ≡ sm
225 lemma refl refl = refl
226
227 snmeqeqt : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j )
228 ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) →
229 snmeq s t i (eq1 i ) ≡ snmap t i
230 snmeqeqt SO SM s t i eq1 = lemma (eq1 i) refl where
231 lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapti ≡ sm ) →
232 snmeq s t i eq1 ≡ sm
233 lemma refl refl = refl
234
235 -- irr2 : { c₂ : Level} {d : Set c₂ } { x1 x2 y1 y2 : d } ( eqx : x1 ≡ x2 )( eqy : y1 ≡ y2 )
236 -- ( eq1 : x1 ≡ y1 ) ( eq2 : x2 ≡ y2 ) → eq1 ≡ eq2
237 -- irr2 = ?
188 238
189 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j) 239 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j)
190 { s t : snat SObj SMap } 240 { s t : snat SObj SMap }
191 → (( i : OC ) → snmap s i ≡ snmap t i ) 241 → (( i : OC ) → snmap s i ≡ snmap t i )
192 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) 242 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j )
193 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) 243 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j )
194 → s ≡ t 244 → s ≡ t
195 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong2 ( λ x y → snat1 SO SM x y ) 245 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong2 ( λ x y →
196 ( extensionality Sets ( λ i → eq1 i ) ) 246 record { snmap = λ i → x i ; sncommute = y x } ) (extensionality Sets ( λ i → eq1 i )) {!!}
197 ( extensionality Sets ( λ snm →
198 ( extensionality Sets ( λ i →
199 ( extensionality Sets ( λ j →
200 ( extensionality Sets ( λ f → irr2 snm i j f ( eq2s i j f (eq1 i) snm (eq2 i j f ) ) {!!} ))))))))
201 where
202 eq2s1 : { i j : OC } { f : I } → {si : SO i} { sj : SO j }
203 ( snm : ( i : OC ) → SO i ) → ( si ≡ snm i ) → ( sj ≡ snm j ) → SM {i} {j} f si ≡ sj → SM f ( snm i) ≡ snm j
204 eq2s1 {i} {j} {f} {si} {sj} snm eq1 eq2 eq3 = begin
205 SM f ( snm i)
206 ≡⟨ ≡cong (λ x → SM f x ) (sym eq1) ⟩
207 SM f si
208 ≡⟨ eq3 ⟩
209 sj
210 ≡⟨ eq2 ⟩
211 snm j
212 ∎ where
213 open import Relation.Binary.PropositionalEquality
214 open ≡-Reasoning
215 eq2s : ( i j : OC ) ( f : I ) → ( snmap s i ≡ snmap t i ) →
216 ( snm : ( i : OC ) → SO i ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j → SM f ( snm i) ≡ snm j
217 eq2s i j f eq1 snm eq2 = eq2s1 snm {!!} {!!} eq2
218 irr3 : { i j : OC } { f : I } → {snmapsi : SO i } → {snmapsj : SO j } →
219 ( es et : SM f ( snmapsi ) ≡ snmapsj ) → es ≡ et
220 irr3 refl refl = refl
221 irr2 : ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I ) →
222 ( es et : SM f (snm i ) ≡ snm j ) → es ≡ et
223 irr2 snm i j f es et = irr3 es et
224 247
225 248
226 open import HomReasoning 249 open import HomReasoning
227 open NTrans 250 open NTrans
228 251
281 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] 304 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
282 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin 305 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
283 limit1 a t x 306 limit1 a t x
284 ≡⟨⟩ 307 ≡⟨⟩
285 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f } 308 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f }
286 ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) {!!} {!!} {!!} ⟩ 309 ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩
287 record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) } 310 record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) }
288 ≡⟨⟩ 311 ≡⟨⟩
289 f x 312 f x
290 ∎ ) where 313 ∎ ) where
291 open import Relation.Binary.PropositionalEquality 314 open import Relation.Binary.PropositionalEquality
292 open ≡-Reasoning 315 open ≡-Reasoning
293 316 eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
294 317 eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t )
295 318 eq2 : (x : a ) (i j : Obj C) (f : I) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
296 319 eq2 x i j f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
297 320 eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j
298 321 eq3 x i j k = sncommute (f x ) k
299 322
300 323
301 324
325
326
327
328
329
330
331